The measurement-based AND-adder on the full register: the n-fold hybrid amplitude equality

Category: 3-Local (QM-validity content; no CSD ontology).

MeasurementAdder.lean (#21) re-costs the AND-adder by replacing its 3n reverse-pass Toffolis with measurement gadgets and proves the Toffoli count; what it left open was the amplitude-level statement that the hybrid adder, run on the full register, produces the same data as the unitary adder. This module proves it, with one correction to the picture #21 drew.

The correction. The reverse pass of a carry cell is three Toffolis with the same target, [CCX a b g, CCX a c g, CCX b c g] reversed, and the ancilla g holds the majority ab ⊕ ac ⊕ bc — not an AND — when the pass begins. Gidney's single-CZ gadget is correct only on an AND-shaped ancilla, so replacing each of the three Toffolis by it is not amplitude-exact: the first replacement, at ancilla maj with corrections for bc, leaves the data-dependent phase (−1)^{m(ab ⊕ ac)} on the m = 1 branch (naive_cell_gadget_sign_flip exhibits the sign). The amplitude-exact hybrid replaces the cell's whole reverse block by one measure-and-correct gadget with a CZ on each of the three input pairs (cellGadget): the majority ancilla is exactly the parity those corrections cancel. This saves the same 3n Toffolis with n measurements instead of 3n.

• hybridAdd L mo — the forward and sum passes as unitaries, then the measurement-based uncompute pass hybridUncompute L mo n (cells n−1, …, 0, one gadget each, outcomes mo).
• wellFormed_hybridUncompute — the run is well-formed: when cell i's gadget fires, its ancilla G (i+1) holds the majority of A i, B i, G i (the forward carry invariant, carried through the sum pass and the later cells, which never touch these wires).
• ★★ hybridAdd_amplitude — the n-fold hybrid amplitude equality: on every basis input with clean ancillas the hybrid adder produces (√2)⁻¹^n • |out⟩, where out agrees with the unitary adder's output on every wire except the n carry ancillas (hybridAdd_shadow_data), which hold the outcomes (hybridAdd_shadow_outcome); in particular the sum register holds (A + B) mod 2ⁿ (hybridAdd_sum). By linearity the same holds for any superposition of clean-ancilla inputs (hybridLin_sum).
• measureUncompute_eq_measureCorrect — the general-wire gadget of HybridLift.lean, at wires (0,1,2) of QReg 3 with the single correction (0,1), is the operator measureUncompute of MeasurementUncompute.lean (#31): the same Hadamard, projector and CZ, entry for entry.

Honest scope

The gadget is represented per outcome; the branch amplitude (√2)⁻¹^n says each of the 2ⁿ outcome strings has probability 2⁻ⁿ, and every branch carries the right data. The Toffoli count of the hybrid uncompute pass is 0 as before (each gadget is Hadamard, measurement and Cliffords); its measurement count is n, not the 3n that #21's per-Toffoli bookkeeping implied. No ECDSA resource-score change is claimed.

The general-wire gadget is #31's gadget

theorem CSD.Empirical.QM.update_two_eq (w : B3) (mo : Fin 2) : Function.update w 2 mo = ![w 0, w 1, mo]

update w 2 mo on three wires is the literal triple.

theorem CSD.Empirical.QM.correctionPhase_single (mo : Fin 2) (z : B3) : Reversible.correctionPhase [(0, 1)] mo z = if mo = 1 then czPhase (z 0) (z 1) else 1

The single-pair correction phase is the data CZ phase at outcome 1, and 1 at outcome 0.

theorem CSD.Empirical.QM.measureCorrect_entry (mo : Fin 2) (z w : B3) : Reversible.measureCorrectMat [(0, 1)] 2 mo z w = (if mo = 1 then czPhase (z 0) (z 1) else 1) * ((if z 2 = mo then 1 else 0) * hadA z w)

The entry identity behind the bridge: the general-wire gadget entry is the product of #31's correction, projector and Hadamard entries.

theorem CSD.Empirical.QM.measureUncompute_eq_measureCorrect (mo : Fin 2) (ψ : QuantumInfo.QReg 3) : measureUncompute mo ψ = (Matrix.toEuclideanLin (Reversible.measureCorrectMat [(0, 1)] 2 mo)) ψ

★ The general-wire gadget is #31's gadget. On QReg 3, the measure-and-correct gadget on ancilla 2 with the single correction (0, 1) is the operator measureUncompute of MeasurementUncompute.lean, entry for entry.

Why one gadget per cell: the naive replacement's sign

theorem CSD.Empirical.QM.naive_cell_gadget_sign_flip : (Matrix.toEuclideanLin (Reversible.measureCorrectMat [(1, 2)] 3 1)) (QuantumInfo.basisState ![1, 1, 0, 1]) = -(↑√2)⁻¹ • QuantumInfo.basisState ![1, 1, 0, 1]

The naive replacement is not amplitude-exact. On the four wires a, b, c, g with a = b = 1, c = 0 and the ancilla g = 1 = maj(a, b, c), the single-CZ gadget for the block CCX b c g (corrections for b ∧ c = 0 only) flips the sign of the m = 1 branch: the data survive, but with the relative phase (−1)^{ab ⊕ ac} = −1 against the branches where it does not fire.

The hybrid adder

def CSD.Empirical.QM.cellGadget {m n : ℕ} (L : Reversible.AndAddLayout m n) (i : ℕ) (mo : Fin 2) : Reversible.HybridGate m

The cell gadget: measure the majority ancilla G (i+1) of cell i and correct with a CZ on each input pair (A i, B i), (A i, G i), (B i, G i).

Equations

• CSD.Empirical.QM.cellGadget L i mo = Reversible.HybridGate.measure [(L.A i, L.B i), (L.A i, L.G i), (L.B i, L.G i)] (L.G (i + 1)) mo

def CSD.Empirical.QM.hybridUncompute {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) : ℕ → List (Reversible.HybridGate m)

The measurement-based uncompute pass over cells k−1, …, 0 (cell k−1 first, as in the reverse pass), one gadget per cell with outcomes mo.

Equations

• CSD.Empirical.QM.hybridUncompute L mo 0 = []
• CSD.Empirical.QM.hybridUncompute L mo k.succ = CSD.Empirical.QM.cellGadget L k (mo k) :: CSD.Empirical.QM.hybridUncompute L mo k

def CSD.Empirical.QM.hybridAdd {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) : List (Reversible.HybridGate m)

The hybrid adder: the forward and sum passes as unitaries, then the measurement-based uncompute pass over all n cells.

Equations

• CSD.Empirical.QM.hybridAdd L mo = List.map Reversible.HybridGate.gate (Reversible.andForward L ++ Reversible.andSumPass L) ++ CSD.Empirical.QM.hybridUncompute L mo n

theorem CSD.Empirical.QM.gadgetCount_hybridUncompute {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (k : ℕ) : Reversible.gadgetCount (hybridUncompute L mo k) = k

theorem CSD.Empirical.QM.gadgetCount_hybridAdd {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) : Reversible.gadgetCount (hybridAdd L mo) = n

theorem CSD.Empirical.QM.shadow_hybridUncompute_of_ne {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (k : ℕ) (u : Fin m → Fin 2) (i : Fin m) : (∀ j < k, i ≠ L.G (j + 1)) → Reversible.shadow (hybridUncompute L mo k) u i = u i

The uncompute pass writes only the carry ancillas of its cells.

theorem CSD.Empirical.QM.shadow_hybridUncompute_anc {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (k : ℕ) : k ≤ n → ∀ (u : Fin m → Fin 2), ∀ j < k, Reversible.shadow (hybridUncompute L mo k) u (L.G (j + 1)) = mo j

The uncompute pass writes each cell's outcome into its carry ancilla.

theorem CSD.Empirical.QM.regOfState_majority (a b c : Bool) : (if Reversible.majority a b c = true then 1 else 0) = ((if a = true then 1 else 0) * if b = true then 1 else 0) + (((if a = true then 1 else 0) * if c = true then 1 else 0) + (((if b = true then 1 else 0) * if c = true then 1 else 0) + 0))

majority as a Fin 2 parity of pairwise ANDs, in the recast.

theorem CSD.Empirical.QM.wellFormed_hybridUncompute {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (t : Reversible.State m) (hmaj : ∀ j < n, t (L.G (j + 1)) = Reversible.majority (t (L.A j)) (t (L.B j)) (t (L.G j))) (k : ℕ) : k ≤ n → ∀ (u : Fin m → Fin 2), (∀ j < k, u (L.A j) = Reversible.regOfState t (L.A j) ∧ u (L.B j) = Reversible.regOfState t (L.B j) ∧ u (L.G j) = Reversible.regOfState t (L.G j) ∧ u (L.G (j + 1)) = Reversible.regOfState t (L.G (j + 1))) → Reversible.WellFormed (hybridUncompute L mo k) u

The run is well-formed. If t satisfies the carry invariant (each G (i+1) holds the majority of A i, B i, G i), then on any register state agreeing with t on the wires of the cells still to come, the uncompute pass over k ≤ n cells is well-formed: every gadget meets its majority ancilla, and its corrections avoid it.

The carry invariant after the forward and sum passes

theorem CSD.Empirical.QM.unitaryPrefix_majority {m n : ℕ} (L : Reversible.AndAddLayout m n) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (j : ℕ) (hj : j < n) : Reversible.denote (Reversible.andForward L ++ Reversible.andSumPass L) s (L.G (j + 1)) = Reversible.majority (Reversible.denote (Reversible.andForward L ++ Reversible.andSumPass L) s (L.A j)) (Reversible.denote (Reversible.andForward L ++ Reversible.andSumPass L) s (L.B j)) (Reversible.denote (Reversible.andForward L ++ Reversible.andSumPass L) s (L.G j))

After the forward and sum passes, each carry ancilla holds the majority of its cell's inputs: the forward carry invariant, untouched by the sum pass.

★★ The n-fold hybrid amplitude equality

theorem CSD.Empirical.QM.wellFormed_hybridAdd {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) : Reversible.WellFormed (hybridAdd L mo) (Reversible.regOfState s)

The hybrid run is well-formed on every clean-ancilla basis input.

theorem CSD.Empirical.QM.hybridAdd_amplitude {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) : (Reversible.hybridLin (hybridAdd L mo)) (QuantumInfo.basisState (Reversible.regOfState s)) = (↑√2)⁻¹ ^ n • QuantumInfo.basisState (Reversible.shadow (hybridAdd L mo) (Reversible.regOfState s))

★★ The n-fold hybrid amplitude equality. On every basis input with clean carry ancillas, the hybrid adder — forward and sum passes, then one measure-and-correct gadget per carry cell with outcomes mo — produces (√2)⁻¹^n • |out⟩, out the run's shadow.

theorem CSD.Empirical.QM.hybridAdd_shadow_data {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (i : Fin m) (hi : ∀ j < n, i ≠ L.G (j + 1)) : Reversible.shadow (hybridAdd L mo) (Reversible.regOfState s) i = Reversible.regOfState (Reversible.denote (Reversible.andAdd L) s) i

The data agree with the unitary adder. On every wire other than the n carry ancillas G 1, …, G n, the hybrid output is the unitary adder's output: the uncompute pass — unitary or measured — writes nothing else.

theorem CSD.Empirical.QM.hybridAdd_shadow_outcome {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (j : ℕ) (hj : j < n) : Reversible.shadow (hybridAdd L mo) (Reversible.regOfState s) (L.G (j + 1)) = mo j

The ancillas hold the outcomes.

theorem CSD.Empirical.QM.hybridAdd_sum {m n : ℕ} (L : Reversible.AndAddLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (hS0 : ∀ (i : ℕ), s (L.S i) = false) : Reversible.regValRange L.S (Reversible.stateOfReg (Reversible.shadow (hybridAdd L mo) (Reversible.regOfState s))) n = (Reversible.regValRange L.A s n + Reversible.regValRange L.B s n) % 2 ^ n

The sum is right on every branch. The sum register of the hybrid output holds (A + B) mod 2ⁿ, exactly as for the unitary adder (andAdd_correct).