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

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

MeasurementGidneyAdder.lean re-costs the Gidney adder — n Toffoli forward, 0 on the measured reverse pass — and MeasurementAdderHybrid.lean proved the amplitude-level statement for the AND-adder. This module is the same statement for the Gidney adder, on the general hybrid semantics of HybridLift.lean. Here the per-Toffoli picture is right: the reverse block of a Gidney cell is [CX cin cout, CCX a b cout, CX cin b, CX cin a], and when its Toffoli fires the ancilla cout holds exactly the fresh AND (a ⊕ cin) ∧ (b ⊕ cin) of the (still shifted) addend wires — an AND-shaped block, so Gidney's single-CZ gadget is exact there, one per cell, with the two un-shifting CNOTs kept as unitaries around it (gidneyHybridCell).

• gidneyHybridAdd L mo — the forward and sum passes as unitaries, then the hybrid reverse pass gidneyHybridUncompute L mo n (cells n−1, …, 0; the Toffoli of each replaced by the gadget with outcome mo k).
• gidneyHybrid_invariant — the run compared with the unitary reverse pass, cell by cell: off the outcome ancillas the two agree (the agreement propagation denoteGate_agree, gate by gate), the ancillas hold the outcomes, and every gadget meets its AND (MAJ(a,b,c) ⊕ c = (a ⊕ c) ∧ (b ⊕ c), majority_xor_carry, on the forward carry invariant).
• ★★ gidneyHybridAdd_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 (gidneyHybridAdd_shadow_data) — so the sum register holds (A + B) mod 2ⁿ (gidneyHybridAdd_sum) and the addends are restored (gidneyHybridAdd_shadow_A, _B) — and the ancillas hold the outcomes (gidneyHybridAdd_shadow_outcome). By linearity the same holds for any superposition of clean-ancilla inputs (hybridLin_sum).

With MeasurementAdderHybrid.lean this closes link 11's measurement-gadget strand: both measurement-based adders of the corpus are amplitude-exact on the full register, at the Toffoli counts their re-costs state (n here, 3n there).

Honest scope

Per-outcome representation: each of the 2ⁿ outcome strings has probability 2⁻ⁿ and every branch carries the right data. The Toffoli count of the reverse pass is 0 as gidneyMeasAddToffoli_eq states; the measurement count is n. No ECDSA resource claim.

Boolean facts

theorem CSD.Empirical.QM.majority_xor_carry (a b c : Bool) : (Reversible.majority a b c ^^ c) = ((a ^^ c) && (b ^^ c))

MAJ(a,b,c) ⊕ c = (a ⊕ c) ∧ (b ⊕ c): the Gidney cell's fresh AND is the carry-out minus the carry-in.

theorem CSD.Empirical.QM.regOfState_and (x y : Bool) : (if (x && y) = true then 1 else 0) = ((if x = true then 1 else 0) * if y = true then 1 else 0) + 0

A Boolean AND in the Fin 2 recast: the product, as the one-pair parity.

The hybrid reverse pass

def CSD.Empirical.QM.gidneyHybridCell {m n : ℕ} (L : Reversible.GidneyLayout m n) (k : ℕ) (mo : Fin 2) : List (Reversible.HybridGate m)

The hybrid reverse block of cell k: the reversed Gidney cell with its Toffoli replaced by the single-correction gadget on the fresh AND (A k ⊕ G k) ∧ (B k ⊕ G k), the un-shifting CNOTs kept as unitaries.

Equations

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

theorem CSD.Empirical.QM.inverse_gidneyForwardSlice {m n : ℕ} (L : Reversible.GidneyLayout m n) (k : ℕ) : Reversible.inverse (Reversible.gidneyForwardSlice L k) = [Reversible.Gate.CX (L.G k) (L.G (k + 1)), Reversible.Gate.CCX (L.A k) (L.B k) (L.G (k + 1)), Reversible.Gate.CX (L.G k) (L.B k), Reversible.Gate.CX (L.G k) (L.A k)]

The unitary reverse block of cell k: the same gates with the Toffoli in place.

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

The hybrid reverse pass over cells k−1, …, 0 (cell k−1 first, as in the reverse pass).

Equations

• CSD.Empirical.QM.gidneyHybridUncompute L mo 0 = []
• CSD.Empirical.QM.gidneyHybridUncompute L mo k.succ = CSD.Empirical.QM.gidneyHybridCell L k (mo k) ++ CSD.Empirical.QM.gidneyHybridUncompute L mo k

def CSD.Empirical.QM.gidneyUnitaryUncompute {m n : ℕ} (L : Reversible.GidneyLayout m n) : ℕ → Reversible.Circuit m

The unitary reverse pass over cells k−1, …, 0, in the same shape.

Equations

• CSD.Empirical.QM.gidneyUnitaryUncompute L 0 = []
• CSD.Empirical.QM.gidneyUnitaryUncompute L k.succ = Reversible.inverse (Reversible.gidneyForwardSlice L k) ++ CSD.Empirical.QM.gidneyUnitaryUncompute L k

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

The hybrid Gidney adder: the forward and sum passes as unitaries, then the hybrid reverse pass over all n cells.

Equations

• CSD.Empirical.QM.gidneyHybridAdd L mo = List.map Reversible.HybridGate.gate (Reversible.gidneyForward L ++ Reversible.andSumPass L.toAnd) ++ CSD.Empirical.QM.gidneyHybridUncompute L mo n

theorem CSD.Empirical.QM.gidneyForwardPrefix_succ {m n : ℕ} (L : Reversible.GidneyLayout m n) (k : ℕ) : Reversible.gidneyForwardPrefix L (k + 1) = Reversible.gidneyForwardPrefix L k ++ Reversible.gidneyForwardSlice L k

theorem CSD.Empirical.QM.gidneyUnitaryUncompute_eq {m n : ℕ} (L : Reversible.GidneyLayout m n) (k : ℕ) : gidneyUnitaryUncompute L k = Reversible.inverse (Reversible.gidneyForwardPrefix L k)

The shaped unitary reverse pass is the reverse pass.

theorem CSD.Empirical.QM.gadgetCount_gidneyHybridUncompute {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (k : ℕ) : Reversible.gadgetCount (gidneyHybridUncompute L mo k) = k

theorem CSD.Empirical.QM.gadgetCount_gidneyHybridAdd {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) : Reversible.gadgetCount (gidneyHybridAdd L mo) = n

The invariant

def CSD.Empirical.QM.AgreeOff {m n : ℕ} (L : Reversible.GidneyLayout m n) (k : ℕ) (u : Fin m → Fin 2) (T : Reversible.State m) : Prop

Off the outcome ancillas of cells k, …, n−1, the register state u read as Booleans agrees with the Boolean state T.

Equations

• CSD.Empirical.QM.AgreeOff L k u T = ∀ (i : Fin m), (∀ (j : ℕ), k ≤ j → j < n → i ≠ L.G (j + 1)) → Reversible.stateOfReg u i = T i

def CSD.Empirical.QM.HoldsOutcomes {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (k : ℕ) (u : Fin m → Fin 2) : Prop

The outcome ancillas of cells k, …, n−1 hold their outcomes.

Equations

• CSD.Empirical.QM.HoldsOutcomes L mo k u = ∀ (j : ℕ), k ≤ j → j < n → u (L.G (j + 1)) = mo j

def CSD.Empirical.QM.CellsFresh {m n : ℕ} (L : Reversible.GidneyLayout m n) (t T : Reversible.State m) (k : ℕ) : Prop

The wires of cells 0, …, k−1 still hold their post-forward values.

Equations

• CSD.Empirical.QM.CellsFresh L t T k = ∀ j < k, T (L.A j) = t (L.A j) ∧ T (L.B j) = t (L.B j) ∧ T (L.G j) = t (L.G j) ∧ T (L.G (j + 1)) = t (L.G (j + 1))

theorem CSD.Empirical.QM.gidneyHybrid_invariant {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (t : Reversible.State m) (hcell : ∀ j < n, (t (L.G (j + 1)) ^^ t (L.G j)) = (t (L.A j) && t (L.B j))) (k : ℕ) : k ≤ n → ∀ (u : Fin m → Fin 2) (T : Reversible.State m), AgreeOff L k u T → HoldsOutcomes L mo k u → CellsFresh L t T k → Reversible.WellFormed (gidneyHybridUncompute L mo k) u ∧ AgreeOff L 0 (Reversible.shadow (gidneyHybridUncompute L mo k) u) (Reversible.denote (gidneyUnitaryUncompute L k) T) ∧ HoldsOutcomes L mo 0 (Reversible.shadow (gidneyHybridUncompute L mo k) u)

The hybrid reverse pass against the unitary one, cell by cell. If, before the cells k−1, …, 0, the register state agrees with the Boolean state off the outcome ancillas of the cells already processed, those hold their outcomes, and the cells to come are still fresh, then the hybrid pass is well-formed, its shadow agrees with the unitary pass off all outcome ancillas, and every outcome ancilla holds its outcome.

The carry invariant after the forward and sum passes

theorem CSD.Empirical.QM.gidneyPrefix_cell {m n : ℕ} (L : Reversible.GidneyLayout m n) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (j : ℕ) (hj : j < n) : (Reversible.denote (Reversible.gidneyForward L ++ Reversible.andSumPass L.toAnd) s (L.G (j + 1)) ^^ Reversible.denote (Reversible.gidneyForward L ++ Reversible.andSumPass L.toAnd) s (L.G j)) = (Reversible.denote (Reversible.gidneyForward L ++ Reversible.andSumPass L.toAnd) s (L.A j) && Reversible.denote (Reversible.gidneyForward L ++ Reversible.andSumPass L.toAnd) s (L.B j))

After the forward and sum passes, each cell's fresh AND is its carry-out minus its carry-in: G (j+1) ⊕ G j = A j ∧ B j on the (shifted) addend wires.

★★ The n-fold hybrid amplitude equality

theorem CSD.Empirical.QM.gidneyHybridAdd_invariant {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) : Reversible.WellFormed (gidneyHybridAdd L mo) (Reversible.regOfState s) ∧ AgreeOff L 0 (Reversible.shadow (gidneyHybridAdd L mo) (Reversible.regOfState s)) (Reversible.denote (Reversible.gidneyAdd L) s) ∧ HoldsOutcomes L mo 0 (Reversible.shadow (gidneyHybridAdd L mo) (Reversible.regOfState s))

The hybrid run is well-formed on every clean-ancilla basis input, and its shadow is the unitary adder's output off the outcome ancillas, which hold the outcomes.

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

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

theorem CSD.Empirical.QM.gidneyHybridAdd_shadow_data {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (i : Fin m) (hi : ∀ j < n, i ≠ L.G (j + 1)) : Reversible.shadow (gidneyHybridAdd L mo) (Reversible.regOfState s) i = Reversible.regOfState (Reversible.denote (Reversible.gidneyAdd L) s) i

The data agree with the unitary adder on every wire other than the n carry ancillas G 1, …, G n.

theorem CSD.Empirical.QM.gidneyHybridAdd_shadow_outcome {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (j : ℕ) (hj : j < n) : Reversible.shadow (gidneyHybridAdd L mo) (Reversible.regOfState s) (L.G (j + 1)) = mo j

The ancillas hold the outcomes.

theorem CSD.Empirical.QM.gidneyHybridAdd_sum {m n : ℕ} (L : Reversible.GidneyLayout 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 (gidneyHybridAdd 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 holds (A + B) mod 2ⁿ, exactly as for the unitary adder (gidneyAdd_correct).

theorem CSD.Empirical.QM.gidneyHybridAdd_shadow_A {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (k : ℕ) : Reversible.shadow (gidneyHybridAdd L mo) (Reversible.regOfState s) (L.A k) = Reversible.regOfState s (L.A k)

The addends are restored on every branch (the un-shifting CNOTs run as unitaries).

theorem CSD.Empirical.QM.gidneyHybridAdd_shadow_B {m n : ℕ} (L : Reversible.GidneyLayout m n) (mo : ℕ → Fin 2) (s : Reversible.State m) (hG0 : ∀ (j : ℕ), s (L.G j) = false) (k : ℕ) : Reversible.shadow (gidneyHybridAdd L mo) (Reversible.regOfState s) (L.B k) = Reversible.regOfState s (L.B k)