Function discharge_journaled_injective 

pub fn discharge_journaled_injective(
    name: &str,
    in_bits: u32,
    augmented: &[usize],
) -> Result<JournaledInjectivity, String>

Prove a Journaled op is INJECTIVE once augmented with its Bennett ancilla. augmented[x] is the packed (F(x), J(x)) output for input x (all 2^in_bits inputs present). Injective iff every packed output is distinct — an EXHAUSTIVE bit-blast, the same rigor as certify_gate, so the core needs no SMT solver. Fails loud on a collision: two inputs share an augmented output, so the ancilla did NOT capture the erased bits — a genuine (un-reversible) Landauer erasure.