AND-based reversible adder with explicit fresh per-carry AND temporaries (Tier-X / L5-c prerequisite)

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate). Pure Boolean-DSL value-correctness; no amplitude bridge and no measurement (those are #31 / L5-d).

Why this file exists (the L5-c wall verdict)

The measurement-based AND-uncomputation gadget (Empirical/QM/MeasurementUncompute.lean, Gidney's measure-and-correct, the ~2× Toffoli saving) needs an attachment point: a fresh ancilla holding a logical AND of two data wires (andInput-shaped), uncomputed at an explicit sub-circuit. The corpus's two ripple adders do not provide one:

• ModAdd.rippleCirc computes carries into a carry chain C and leaves them dirty (never uncomputed) — no uncompute sub-block to replace.
• CuccaroAdd.cuccaroAdd restores the carries unitarily inside uma (in-place, carry-restoring), with no fresh AND temporary — again nothing for a measurement gadget to attach to.

This file supplies the missing primitive: an adder whose carries live in fresh |0⟩ ancillas, computed by an explicit AND (Toffoli) and uncomputed by an explicit reverse Toffoli. The uncompute-AND Toffolis are exactly the ones the measurement route would later eliminate.

What is built

Reusable circuit infrastructure (target-frame + agreement propagation):

• gateTarget / denote_apply_of_forall_not_mem_target — a wire that is never a target (it may be a control) is preserved. The control-permitting refinement of gateWires / denote_apply_of_forall_not_mem.
• denote_agree_on — two states agreeing on every wire a circuit's gates touch produce equal outputs on those wires. The locality lemma that makes the uncompute-pass cleanup provable.

The AND-uncompute cell (item 1, the must-have attachment point):

• andCarry a b g := [CCX a b g] — the fresh-AND compute: g ← g ⊕ (a ∧ b) (= a ∧ b for g = 0), a / b preserved (andCarry_correct). The andInput-shaped state g = a ∧ b.
• andUncompute a b g := [CCX a b g] — the explicit AND-uncompute (the Toffoli a measurement gadget replaces). andUncompute_restores: it undoes andCarry, returning g to its input value.
• andCell a b g out := andCarry ++ [CX g out] ++ andUncompute — compute-use-uncompute: out ← out ⊕ (a ∧ b), ancilla g restored (andCell_correct / andCell_ancilla_clean).

The full AND-based ripple adder (items 2/3): andAdd, on an AndAddLayout with addends A, B (both preserved), a separate sum register S, and a fresh per-carry ancilla chain G. Structure: andForward ++ andSumPass ++ inverse andForward — compute all carries into G (preserving A, B), write the sums into S, then uncompute every carry via the reverse pass.

• andAdd_correct: regValRange S (denote (andAdd L) s) n = (A + B) % 2 ^ n.
• andAdd_ancilla_clean: every fresh carry-AND ancilla G i returns to false.
• andAdd_toffoli: 6 * n Toffolis, of which the 3 * n uncompute half is the measurement-route saving target (andAdd_uncompute_toffoli).

Honest scope

Value-correct + ancilla-clean over regVal, Boolean DSL only. The compute / uncompute Toffolis here are unitary; replacing the uncompute half with the measurement gadget is L5-d, and the amplitude lift of the AND-uncompute block is #31. No measurement, no amplitudes, no ECDSA resource claim here. The carry cell uses a 3-Toffoli preserving majority MAJ(a,b,c) = (a∧b) ⊕ (a∧c) ⊕ (b∧c) (GF(2) identity, majority_eq_xor3) so the addend register B survives untouched — which is what makes the reverse pass an exact inverse and the cleanup provable.

Target-frame lemma (controls allowed, only the written wire matters)

def Reversible.gateTarget {n : ℕ} : Gate n → Finset (Fin n)

The set of wires a gate writes (its target), excluding control wires. A wire outside this set is preserved even if it is a control. The control-permitting refinement of gateWires.

Equations

• Reversible.gateTarget (Reversible.Gate.X i) = {i}
• Reversible.gateTarget (Reversible.Gate.CX c t) = {t}
• Reversible.gateTarget (Reversible.Gate.CCX c₁ c₂ t) = {t}
• Reversible.gateTarget (Reversible.Gate.swap i j) = {i, j}

theorem Reversible.denoteGate_apply_of_not_mem_target {n : ℕ} {g : Gate n} {s : State n} {i : Fin n} (hi : i ∉ gateTarget g) : denoteGate g s i = s i

Target-frame (single gate). A wire that is not the target of g is preserved by denoteGate g — even if it is a control.

theorem Reversible.denote_apply_of_forall_not_mem_target {n : ℕ} {i : Fin n} (c : Circuit n) : (∀ g ∈ c, i ∉ gateTarget g) → ∀ (s : State n), denote c s i = s i

Target-frame (circuit). A wire that is never a target of any gate of c is preserved by denote c (it may appear as a control).

Agreement propagation (the cleanup locality lemma)

theorem Reversible.denoteGate_agree {n : ℕ} {P : Fin n → Prop} {g : Gate n} (hg : ∀ w ∈ gateWires g, P w) {s s' : State n} (hss : ∀ (w : Fin n), P w → s w = s' w) (w : Fin n) (hw : P w) : denoteGate g s w = denoteGate g s' w

Agreement (single gate). If s and s' agree on every wire satisfying P, and every wire of g satisfies P, then denoteGate g s and denoteGate g s' agree on every P-wire.

theorem Reversible.denote_agree_on {n : ℕ} {P : Fin n → Prop} (c : Circuit n) : (∀ g ∈ c, ∀ w ∈ gateWires g, P w) → ∀ {s s' : State n}, (∀ (w : Fin n), P w → s w = s' w) → ∀ (w : Fin n), P w → denote c s w = denote c s' w

Agreement propagation (circuit). If every gate of c touches only P-wires, and s, s' agree on all P-wires, then denote c s and denote c s' agree on all P-wires. The locality lemma behind the carry-ancilla cleanup: the sum pass leaves the addend/carry wires untouched, so the reverse pass undoes the forward pass on them exactly.

The fresh-AND carry cell and its explicit uncompute (item 1, the attachment point)

def Reversible.andCarry {n : ℕ} (a b g : Fin n) : Circuit n

The fresh-AND compute. A single Toffoli folding the logical AND of data wires a, b into a fresh ancilla g: g ← g ⊕ (a ∧ b). For a |0⟩-initialised g this writes g = a ∧ b — the andInput-shaped state (a fresh ancilla holding a ∧ b, correlated with the data).

Equations

• Reversible.andCarry a b g = [Reversible.Gate.CCX a b g]

def Reversible.andUncompute {n : ℕ} (a b g : Fin n) : Circuit n

The explicit AND-uncompute (the Toffoli a measurement gadget replaces). Identical gate list to andCarry (a Toffoli is its own inverse): applied after andCarry it restores the ancilla. Named separately to mark the attachment point.

Equations

• Reversible.andUncompute a b g = [Reversible.Gate.CCX a b g]

theorem Reversible.andCarry_correct {n : ℕ} {a b g : Fin n} (hga : g ≠ a) (hgb : g ≠ b) (s : State n) : denote (andCarry a b g) s g = (s g ^^ s a && s b) ∧ denote (andCarry a b g) s a = s a ∧ denote (andCarry a b g) s b = s b

Fresh-AND-compute correctness. For a fresh ancilla distinct from the data, andCarry writes the AND into g (g ← g ⊕ (a ∧ b)) and leaves a, b untouched.

theorem Reversible.andCarry_writes_and {n : ℕ} {a b g : Fin n} (hga : g ≠ a) (hgb : g ≠ b) {s : State n} (hg0 : s g = false) : denote (andCarry a b g) s g = (s a && s b)

Ancilla-clean for a |0⟩ ancilla. andCarry on a fresh g = false writes exactly a ∧ b.

theorem Reversible.andUncompute_restores {n : ℕ} (a b g : Fin n) (s : State n) : denote (andUncompute a b g) (denote (andCarry a b g) s) = s

The AND-uncompute restores the ancilla. Running andUncompute after andCarry returns the whole state to its input — in particular the fresh ancilla g is restored. This is the explicit uncompute point: the second Toffoli (andUncompute) is the one a measurement-based gadget eliminates.

def Reversible.andCell {n : ℕ} (a b g out : Fin n) : Circuit n

The compute-use-uncompute cell. Fold the AND of a, b into out through a fresh ancilla: compute g = a ∧ b (andCarry), use it (CX g out, i.e. out ← out ⊕ g), then uncompute g (andUncompute). The cell is [CCX a b g, CX g out, CCX a b g]: an explicit fresh-AND temporary with an explicit AND-uncompute sub-block, value-correct and ancilla-clean.

Equations

• Reversible.andCell a b g out = Reversible.andCarry a b g ++ [Reversible.Gate.CX g out] ++ Reversible.andUncompute a b g

theorem Reversible.andCell_correct {n : ℕ} {a b g out : Fin n} (hga : g ≠ a) (hgb : g ≠ b) (hoa : out ≠ a) (hob : out ≠ b) (hog : out ≠ g) (s : State n) : denote (andCell a b g out) s out = (s out ^^ s g ^^ s a && s b) ∧ denote (andCell a b g out) s g = s g ∧ denote (andCell a b g out) s a = s a ∧ denote (andCell a b g out) s b = s b

Cell correctness (general). out ← out ⊕ g ⊕ (a ∧ b) (reading the fresh ancilla's input bit g), the ancilla g is restored to its input, and a, b are preserved. For a |0⟩ ancilla (hg0) the g term drops and out ← out ⊕ (a ∧ b) (andCell_correct_clean). The genuine fresh-AND temporary (g = g ⊕ a ∧ b between the compute and uncompute) is used and then cleaned up.

theorem Reversible.andCell_correct_clean {n : ℕ} {a b g out : Fin n} (hga : g ≠ a) (hgb : g ≠ b) (hoa : out ≠ a) (hob : out ≠ b) (hog : out ≠ g) {s : State n} (hg0 : s g = false) : denote (andCell a b g out) s out = (s out ^^ s a && s b) ∧ denote (andCell a b g out) s g = false

Cell correctness for a |0⟩ ancilla. With a fresh g = false, out ← out ⊕ (a ∧ b), g restored to false, a/b preserved.

theorem Reversible.andCell_ancilla_clean {n : ℕ} {a b g out : Fin n} (hga : g ≠ a) (hgb : g ≠ b) (hoa : out ≠ a) (hob : out ≠ b) (hog : out ≠ g) {s : State n} (hg0 : s g = false) : denote (andCell a b g out) s g = false

Cell ancilla-clean. A |0⟩-initialised cell ancilla returns to false.

Cell cost: one compute-AND + one uncompute-AND Toffoli

theorem Reversible.andCell_toffoli {n : ℕ} (a b g out : Fin n) : (circuitCost (andCell a b g out)).toffoli = 2

Cell Toffoli cost = 2. One compute-AND (andCarry) + one uncompute-AND (andUncompute); the CX g out is a CNOT.

theorem Reversible.andCell_uncompute_toffoli {n : ℕ} (a b g : Fin n) : (circuitCost (andUncompute a b g)).toffoli = 1

The uncompute-AND half is one Toffoli — the measurement-route saving target. The cell's two Toffolis split as one compute + one uncompute; the measurement gadget (#31/L5-d) eliminates this uncompute Toffoli (replacing it with H + measurement + a conditional Clifford).

The preserving-majority carry cell (3-Toffoli, addend-preserving)

The ripple's per-carry cell must compute the carry-out MAJ(a, b, c) into a fresh ancilla while leaving its inputs (in particular the addend register B) untouched — that is what makes the reverse pass an exact inverse and the ancilla cleanup provable. The GF(2) identity MAJ(a,b,c) = (a∧b) ⊕ (a∧c) ⊕ (b∧c) lets three Toffolis into a single fresh target do this.

theorem Reversible.majority_eq_xor3 (a b c : Bool) : majority a b c = (a && b ^^ a && c ^^ b && c)

Majority as a GF(2) sum of ANDs: MAJ(a,b,c) = (a∧b) ⊕ (a∧c) ⊕ (b∧c). The identity that makes the carry computable into a fresh ancilla by three Toffolis that all read (never overwrite) the inputs.

def Reversible.andCarryCell {n : ℕ} (a b c g : Fin n) : Circuit n

The preserving-majority carry cell. Three Toffolis folding the AND of each input pair into a fresh target g: [CCX a b g, CCX a c g, CCX b c g]. Each gate writes only g (the inputs are pure controls), so a, b, c are preserved and g ← g ⊕ MAJ(a,b,c). These are the explicit fresh-AND computes; the reverse pass (inverse) is the explicit AND-uncompute.

Equations

• Reversible.andCarryCell a b c g = [Reversible.Gate.CCX a b g, Reversible.Gate.CCX a c g, Reversible.Gate.CCX b c g]

theorem Reversible.andCarryCell_correct {n : ℕ} {a b c g : Fin n} (hga : g ≠ a) (hgb : g ≠ b) (hgc : g ≠ c) {s : State n} (hg0 : s g = false) : denote (andCarryCell a b c g) s g = majority (s a) (s b) (s c) ∧ denote (andCarryCell a b c g) s a = s a ∧ denote (andCarryCell a b c g) s b = s b ∧ denote (andCarryCell a b c g) s c = s c

Preserving-majority correctness. For a fresh ancilla g = false distinct from a, b, c, the cell writes g = MAJ(a, b, c) and preserves a, b, c.

theorem Reversible.andCarryCell_toffoli {n : ℕ} (a b c g : Fin n) : (circuitCost (andCarryCell a b c g)).toffoli = 3

Cell Toffoli cost = 3 (the three fresh-AND computes).

The AND-based ripple-adder layout

structure Reversible.AndAddLayout (m n : ℕ) : Type

The AND-based ripple-adder wire geometry for n-bit registers on m wires: addends A, B (both preserved), a separate sum register S (output), and a fresh per-carry ancilla chain G (G 0 the input carry, G (i+1) the carry out of bit i, all init false). The four images are pairwise disjoint and each injective on its used index range — the bounded-injectivity pattern of RippleLayout / CuccaroLayout, refined to a separate sum register so the reverse pass is an exact inverse.

• A : ℕ → Fin m

  First addend (preserved).

• B : ℕ → Fin m

  Second addend (preserved).

• S : ℕ → Fin m

  Sum output register ((A + B) mod 2 ^ n).

• G : ℕ → Fin m

  Fresh per-carry ancilla chain (G i = carry into bit i; init/returned false).

• hAB (i j : ℕ) : self.A i ≠ self.B j
• hAS (i j : ℕ) : self.A i ≠ self.S j
• hAG (i j : ℕ) : self.A i ≠ self.G j
• hBS (i j : ℕ) : self.B i ≠ self.S j
• hBG (i j : ℕ) : self.B i ≠ self.G j
• hSG (i j : ℕ) : self.S i ≠ self.G j
• hSinj (i j : ℕ) : i < n → j < n → self.S i = self.S j → i = j
• hGinj (i j : ℕ) : i < n + 1 → j < n + 1 → self.G i = self.G j → i = j

Carry / sum / forward / uncompute circuits

def Reversible.andForwardSlice {n m : ℕ} (L : AndAddLayout m n) (i : ℕ) : Circuit m

The carry compute for bit i: preserving-majority of (A i, B i, G i) into the fresh G (i+1).

Equations

• Reversible.andForwardSlice L i = Reversible.andCarryCell (L.A i) (L.B i) (L.G i) (L.G (i + 1))

def Reversible.andForwardPrefix {n m : ℕ} (L : AndAddLayout m n) (k : ℕ) : Circuit m

The forward carry pass over the first k bits.

Equations

• Reversible.andForwardPrefix L k = List.flatMap (Reversible.andForwardSlice L) (List.range k)

def Reversible.andForward {n m : ℕ} (L : AndAddLayout m n) : Circuit m

The full forward carry pass (all n bits): computes G (i+1) = carry, preserving A, B.

Equations

• Reversible.andForward L = Reversible.andForwardPrefix L n

def Reversible.andSumSlice {n m : ℕ} (L : AndAddLayout m n) (i : ℕ) : Circuit m

The sum-write for bit i: S i ← S i ⊕ A i ⊕ B i ⊕ G i (three CNOTs into S i).

Equations

• Reversible.andSumSlice L i = [Reversible.Gate.CX (L.A i) (L.S i), Reversible.Gate.CX (L.B i) (L.S i), Reversible.Gate.CX (L.G i) (L.S i)]

def Reversible.andSumPrefix {n m : ℕ} (L : AndAddLayout m n) (k : ℕ) : Circuit m

The sum pass over the first k bits.

Equations

• Reversible.andSumPrefix L k = List.flatMap (Reversible.andSumSlice L) (List.range k)

def Reversible.andSumPass {n m : ℕ} (L : AndAddLayout m n) : Circuit m

The full sum pass (all n bits).

Equations

• Reversible.andSumPass L = Reversible.andSumPrefix L n

theorem Reversible.andSumPass_def {n m : ℕ} (L : AndAddLayout m n) : andSumPass L = andSumPrefix L n

The sum pass is the full-length sum prefix (interface lemma, §9.1).

def Reversible.andAdd {n m : ℕ} (L : AndAddLayout m n) : Circuit m

The AND-based ripple adder. Compute all carries into the fresh ancilla chain G (andForward), write the sums into S (andSumPass), then uncompute every carry via the reverse pass inverse (andForward L). The uncompute pass is the explicit AND-uncompute sub-block — exactly the Toffolis a measurement-based gadget would eliminate.

Equations

• Reversible.andAdd L = Reversible.andForward L ++ Reversible.andSumPass L ++ Reversible.inverse (Reversible.andForward L)

Membership / wire / target characterisation of the forward & sum gates

theorem Reversible.mem_andForwardPrefix {n m : ℕ} {L : AndAddLayout m n} {k : ℕ} {g : Gate m} (hg : g ∈ andForwardPrefix L k) : ∃ j < k, g ∈ andForwardSlice L j

theorem Reversible.mem_andSumPrefix {n m : ℕ} {L : AndAddLayout m n} {k : ℕ} {g : Gate m} (hg : g ∈ andSumPrefix L k) : ∃ j < k, g ∈ andSumSlice L j

theorem Reversible.andForwardSlice_wires {n m : ℕ} {L : AndAddLayout m n} {j : ℕ} {g : Gate m} (hg : g ∈ andForwardSlice L j) {w : Fin m} (hw : w ∈ gateWires g) : w = L.A j ∨ w = L.B j ∨ w = L.G j ∨ w = L.G (j + 1)

theorem Reversible.andForwardSlice_target {n m : ℕ} {L : AndAddLayout m n} {j : ℕ} {g : Gate m} (hg : g ∈ andForwardSlice L j) {w : Fin m} (hw : w ∈ gateTarget g) : w = L.G (j + 1)

theorem Reversible.andSumSlice_target {n m : ℕ} {L : AndAddLayout m n} {j : ℕ} {g : Gate m} (hg : g ∈ andSumSlice L j) {w : Fin m} (hw : w ∈ gateTarget g) : w = L.S j

Preservation lemmas (target-frame)

theorem Reversible.andForwardPrefix_preserves_A {n m : ℕ} (L : AndAddLayout m n) (s : State m) (k i : ℕ) : denote (andForwardPrefix L k) s (L.A i) = s (L.A i)

theorem Reversible.andForwardPrefix_preserves_B {n m : ℕ} (L : AndAddLayout m n) (s : State m) (k i : ℕ) : denote (andForwardPrefix L k) s (L.B i) = s (L.B i)

theorem Reversible.andForwardPrefix_preserves_S {n m : ℕ} (L : AndAddLayout m n) (s : State m) (k i : ℕ) : denote (andForwardPrefix L k) s (L.S i) = s (L.S i)

theorem Reversible.andForwardSlice_preserves {n m : ℕ} (L : AndAddLayout m n) (s : State m) (k : ℕ) {w : Fin m} (hw : w ≠ L.G (k + 1)) : denote (andForwardSlice L k) s w = s w

The forward slice for bit k preserves any wire other than its single target G (k+1).

theorem Reversible.andSumPrefix_preserves_of_ne_S {n m : ℕ} (L : AndAddLayout m n) (t : State m) (k : ℕ) {w : Fin m} (hw : ∀ i < k, w ≠ L.S i) : denote (andSumPrefix L k) t w = t w

Arithmetic: the true carry and the adder sum identity

def Reversible.carryOf (a b : ℕ → Bool) : ℕ → Bool

The true ripple carry sequence: carryOf 0 = false, carryOf (i+1) = MAJ(aᵢ, bᵢ, carryOf i).

Equations

• Reversible.carryOf a b 0 = false
• Reversible.carryOf a b i.succ = Reversible.majority (a i) (b i) (Reversible.carryOf a b i)

theorem Reversible.adder_sum_identity (a b : ℕ → Bool) (k : ℕ) : ∑ i ∈ Finset.range k, (a i ^^ b i ^^ carryOf a b i).toNat * 2 ^ i + (carryOf a b k).toNat * 2 ^ k = ∑ i ∈ Finset.range k, (a i).toNat * 2 ^ i + ∑ i ∈ Finset.range k, (b i).toNat * 2 ^ i

The adder sum identity (ℕ). The low-k sum bits plus the carry into bit k, place-weighted, equal the low-k parts of the two addends. Induction on k via the bitwise fulladder_nat.

Forward carry invariant

theorem Reversible.andForward_carry {n m : ℕ} (L : AndAddLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (k : ℕ) : k ≤ n → (∀ i ≤ k, denote (andForwardPrefix L k) s (L.G i) = carryOf (fun (i : ℕ) => s (L.A i)) (fun (i : ℕ) => s (L.B i)) i) ∧ ∀ (i : ℕ), k < i → i ≤ n → denote (andForwardPrefix L k) s (L.G i) = false

The forward carry invariant. After the first k forward slices, every computed carry ancilla G i (i ≤ k) holds the true carry carryOf i, and the not-yet-computed ancillas (k < i ≤ n) are still false. By induction on k, each step a preserving-majority andCarryCell on fresh G (k+1).

Sum-pass value invariant

theorem Reversible.andSumSlice_preserves {n m : ℕ} (L : AndAddLayout m n) (u : State m) (k : ℕ) {w : Fin m} (hw : w ≠ L.S k) : denote (andSumSlice L k) u w = u w

The sum slice for bit k preserves any wire other than its single target S k.

theorem Reversible.andSumSlice_correct {n m : ℕ} (L : AndAddLayout m n) (u : State m) (k : ℕ) : denote (andSumSlice L k) u (L.S k) = (u (L.S k) ^^ u (L.A k) ^^ u (L.B k) ^^ u (L.G k))

Single sum slice. S i ← S i ⊕ A i ⊕ B i ⊕ G i (the inputs are pure controls).

theorem Reversible.andSum_value {n m : ℕ} (L : AndAddLayout m n) (t : State m) (k : ℕ) : k ≤ n → (∀ i < k, denote (andSumPrefix L k) t (L.S i) = (t (L.S i) ^^ t (L.A i) ^^ t (L.B i) ^^ t (L.G i))) ∧ ∀ (i : ℕ), k ≤ i → i < n → denote (andSumPrefix L k) t (L.S i) = t (L.S i)

Sum-pass value invariant. After the first k sum slices, the processed sum wires (i < k) carry S i ⊕ A i ⊕ B i ⊕ G i, and the unprocessed ones (k ≤ i < n) are unchanged. By induction on k, each step a single andSumSlice writing only S k.

Per-bit value of the full adder

theorem Reversible.andAdd_sum_bit {n m : ℕ} (L : AndAddLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (hS0 : ∀ (i : ℕ), s (L.S i) = false) (k : ℕ) (hk : k < n) : denote (andAdd L) s (L.S k) = (s (L.A k) ^^ s (L.B k) ^^ carryOf (fun (i : ℕ) => s (L.A i)) (fun (i : ℕ) => s (L.B i)) k)

Per-bit sum value. Bit k of the sum register holds A k ⊕ B k ⊕ carry k. The uncompute pass (inverse andForward) only touches G wires, so S k is the value written by andSumPass over the forward-completed carries.

Headline theorems

theorem Reversible.andAdd_correct {n m : ℕ} (L : AndAddLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (hS0 : ∀ (i : ℕ), s (L.S i) = false) : regValRange L.S (denote (andAdd L) s) n = (regValRange L.A s n + regValRange L.B s n) % 2 ^ n

AND-based ripple-adder correctness. For a disjoint-wire layout with all carry ancillas and the sum register initialised false, the sum register ends holding (A + B) mod 2 ^ n. The carries are computed into fresh ancillas (andForward), the sums written (andSumPass), and the carries uncomputed (inverse andForward); the value is read off the exhibited circuit, not postulated.

theorem Reversible.andAdd_ancilla_clean {n m : ℕ} (L : AndAddLayout m n) (s : State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (j : ℕ) : denote (andAdd L) s (L.G j) = false

Ancilla-clean: every fresh carry-AND ancilla returns to false. The reverse pass inverse (andForward L) uncomputes every carry: the sum pass leaves the addend / carry wires untouched (denote_agree_on), so the reverse pass undoes the forward pass on the G chain exactly (reversible_inverse_correct). This is the explicit AND-uncompute working — the property a measurement-based gadget must reproduce.

Derived cost: 6n Toffolis (3n compute + 3n uncompute)

theorem Reversible.andForwardPrefix_toffoli {n m : ℕ} (L : AndAddLayout m n) (k : ℕ) : (circuitCost (andForwardPrefix L k)).toffoli = 3 * k

theorem Reversible.andSumPrefix_toffoli {n m : ℕ} (L : AndAddLayout m n) (k : ℕ) : (circuitCost (andSumPrefix L k)).toffoli = 0

theorem Reversible.andAdd_uncompute_toffoli {n m : ℕ} (L : AndAddLayout m n) : (circuitCost (inverse (andForward L))).toffoli = 3 * n

The uncompute half is 3 * n Toffolis — the AND-uncompute cost a measurement-based gadget would eliminate (the ~2× saving target for L5-d). It equals the compute half (andForward, 3 * n) by cost_inverse_toffoli.

theorem Reversible.andAdd_toffoli {n m : ℕ} (L : AndAddLayout m n) : (circuitCost (andAdd L)).toffoli = 6 * n

Derived Toffoli cost: 6 * n. 3 * n compute-AND Toffolis (andForward) + 3 * n uncompute-AND Toffolis (inverse andForward); the sum pass is CNOT-only. The uncompute 3 * n (andAdd_uncompute_toffoli) is exactly what the measurement route saves.

Non-vacuity witness + #eval cross-check

A concrete 2-bit AND-based adder layout on Fin 9: A → {0,1}, B → {2,3}, S → {4,5}, carry chain G → {6,7,8}. The headlines apply, and the strict Array evaluator runArr (bridge regValRangeArr_eq) witnesses 2 + 3 = 5, the sum register reading 5 and every carry ancilla returning false.

def Reversible.andAddLayout2 : AndAddLayout 9 2

A concrete 2-bit AND-based adder layout on Fin 9.

Equations

• One or more equations did not get rendered due to their size.

def Reversible.andAddWitness2 : State 9

Witness: A = 2 (wires 0,1 = 0,1), B = 3 (wires 2,3 = 1,1), S/G init false.

Equations

• Reversible.andAddWitness2 = ![false, true, true, true, false, false, false, false, false]