Measurement-based AND-uncomputation (Gidney's measure-and-correct gadget)

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

This is the amplitude-model proof-of-concept for measurement-based uncomputation (specs Tier-X measurement-adder fork, stage L5-a). An AND-ancilla holding x ∧ y (computed earlier with a Toffoli, here entangled with the data) is uncomputed without a second Toffoli by Gidney's gadget:

1. Apply Hadamard H to the ancilla and measure it in the computational basis (= an X-basis measurement of the original ancilla), obtaining outcome m ∈ {0,1} (each prob 1/2). The post-measurement data picks up a phase (-1)^{m·(x∧y)}.
2. Correction: if m = 1, apply CZ to the data qubits (x,y), multiplying by (-1)^{x∧y}, which cancels the phase.

Net (BOTH outcomes): the data returns to Σ c_{xy}|x,y⟩ and the ancilla is reset to |m⟩ — the AND is uncomputed using only Cliffords (H, CZ) + a measurement, zero Toffoli. That is the ~2× saving versus the unitary AND-uncompute, which costs one Toffoli.

What is proved

• measureUncompute_uncomputes (THE headline): for every outcome m and every data superposition c, the corrected, projected state equals the uncomputed data with the ancilla reset to |m⟩, scaled by the outcome amplitude (√2)⁻¹. The phase cancellation ((-1)^{x∧y})² = 1 (the m = 1 branch) is genuine, not asserted.
• andInput_nontrivial: the AND-entangled INPUT genuinely carries a = x ∧ y (non-vacuity: the uncompute is real work, not a trivial product).
• gadgetGateList_zero_toffoli: the gadget's gate list contains no Toffoli, whereas the unitary AND-uncompute contains one.
• gadgetGateList_denotes_measureUncompute (L5-b, the operator↔list link): folding the interpretation GadgetGate.denote of gadgetGateList (hGate ↦ hadA, measGate ↦ projA m, czGate ↦ correctionMat m) reproduces the measureUncompute m operator exactly. The equality is definitional (rfl): measureUncompute m is by definition the composition correctionMat m ∘ projA m ∘ hadA, so the cost-bearing gate list is a genuine decomposition of the operator, not a free-standing list.
• measureUncompute_cost (L5-b, the 0-vs-1 Toffoli saving as an operator property): the decomposition gadgetGateList of the measureUncompute operator has Toffoli count 0 (plus 1 measurement and 1 CNOT-equivalent for the conditional CZ, all single-qubit Cliffords free), whereas the unitary AND-uncompute's decomposition has Toffoli count 1. The Toffoli-free property is now a property of the operator (via the link), not of a hand-written list.

Representation choice

We use the per-outcome partial-isometry form (not a full CPTP Channel): on the explicit 3-qubit space QReg 3 = EuclideanSpace ℂ (Fin 3 → Fin 2) (qubit 0 = x, 1 = y, 2 = a), each step is a Matrix.toEuclideanLin application — Hadamard on the ancilla (hadA, entries the corpus hadEntry = qmH), the computational projector (projA m), and the conditional CZ on the data (correctionMat m, = qmCZ-phase). This is the cleanest faithful form the amplitude machinery supports; the X-basis phases are why this lives in the amplitude model and NOT the Boolean reversible DSL.

Scope (honest)

L5-a settled that measurement-based uncomputation is verifiable in Lean in the amplitude model. L5-b (this file) closes the operator↔list gap: gadgetGateList is now proven (definitionally) to be the decomposition of measureUncompute, so the 0-Toffoli cost is a property of the operator, not a hand-written list, and the ~2× saving is stated in the corpus Reversible.Cost model (0 Toffoli + 1 measurement + Cliffords, vs 1 Toffoli for the unitary uncompute). This is a per-AND-uncompute gate-cost statement only. Deferred: L5-c (the Boolean-arithmetic ↔ amplitude bridge — applying this to actual adders, the trusted-base increase, the wall), L5-d (the measurement-based adder + circuit re-cost). No ECDSA resource claim is made here.

@[reducible, inline]

abbrev CSD.Empirical.QM.B3 : Type

The 3-qubit computational index type (x, y, ancilla a).

Equations

• CSD.Empirical.QM.B3 = (Fin 3 → Fin 2)

Coordinate primitives for Matrix.toEuclideanLin on QReg 3

theorem CSD.Empirical.QM.toEuclideanLin_diagonal_apply (d : B3 → ℂ) (v : QuantumInfo.QReg 3) (z : B3) : ((Matrix.toEuclideanLin (Matrix.diagonal d)) v).ofLp z = d z * v.ofLp z

A diagonal register operator acts pointwise on amplitudes.

theorem CSD.Empirical.QM.toEuclideanLin_basisState (A : Matrix B3 B3 ℂ) (w z : B3) : ((Matrix.toEuclideanLin A) (QuantumInfo.basisState w)).ofLp z = A z w

A register operator applied to a computational basis state reads off the w-th column.

theorem CSD.Empirical.QM.smul_coord (c : ℂ) (v : QuantumInfo.QReg 3) (z : B3) : (c • v).ofLp z = c * v.ofLp z

Coordinatewise scalar multiplication on QReg 3.

theorem CSD.Empirical.QM.b3_eq_iff (z : B3) (x y m : Fin 2) : z = ![x, y, m] ↔ z 0 = x ∧ z 1 = y ∧ z 2 = m

Pointwise characterisation of a 3-qubit bitstring equality.

The gadget components (gates on the 3-qubit register)

def CSD.Empirical.QM.czPhase (x y : Fin 2) : ℂ

The CZ phase on the data qubits: (-1)^{x∧y} (x∧y = x·y on Fin 2).

Equations

• CSD.Empirical.QM.czPhase x y = (-1) ^ (↑x * ↑y)

noncomputable def CSD.Empirical.QM.hadA : Matrix B3 B3 ℂ

Hadamard on the ancilla (qubit 2), identity on the data qubits (0,1). Its qubit-2 block entries are the corpus single-qubit Hadamard entries (hadEntry = qmH).

Equations

• CSD.Empirical.QM.hadA = Matrix.of fun (z w : CSD.Empirical.QM.B3) => if z 0 = w 0 ∧ z 1 = w 1 then QuantumInfo.hadEntry (z 2) (w 2) else 0

theorem CSD.Empirical.QM.hadA_apply (z w : B3) : hadA z w = if z 0 = w 0 ∧ z 1 = w 1 then QuantumInfo.hadEntry (z 2) (w 2) else 0

noncomputable def CSD.Empirical.QM.projA (m : Fin 2) : Matrix B3 B3 ℂ

Computational projector onto ancilla outcome m (the X-basis measurement after the Hadamard).

Equations

• CSD.Empirical.QM.projA m = Matrix.diagonal fun (z : CSD.Empirical.QM.B3) => if z 2 = m then 1 else 0

noncomputable def CSD.Empirical.QM.czXY : Matrix B3 B3 ℂ

The CZ on the data qubits as a diagonal register operator: phase (-1)^{x∧y}.

Equations

• CSD.Empirical.QM.czXY = Matrix.diagonal fun (z : CSD.Empirical.QM.B3) => CSD.Empirical.QM.czPhase (z 0) (z 1)

noncomputable def CSD.Empirical.QM.correctionMat (m : Fin 2) : Matrix B3 B3 ℂ

The conditional correction: CZ on the data when m = 1, identity when m = 0.

Equations

• CSD.Empirical.QM.correctionMat m = Matrix.diagonal fun (z : CSD.Empirical.QM.B3) => if m = 1 then CSD.Empirical.QM.czPhase (z 0) (z 1) else 1

theorem CSD.Empirical.QM.correctionMat_one : correctionMat 1 = czXY

The correction at outcome 1 is exactly the data CZ.

theorem CSD.Empirical.QM.correctionMat_zero : correctionMat 0 = 1

The correction at outcome 0 is the identity (no Toffoli, no Clifford applied).

def CSD.Empirical.QM.andIdx (x y : Fin 2) : B3

The AND-entangled index ![x, y, x∧y]: data (x,y) with the ancilla carrying the AND.

Equations

• CSD.Empirical.QM.andIdx x y = ![x, y, x * y]

@[simp]

theorem CSD.Empirical.QM.andIdx_zero (x y : Fin 2) : andIdx x y 0 = x

@[simp]

theorem CSD.Empirical.QM.andIdx_one (x y : Fin 2) : andIdx x y 1 = y

@[simp]

theorem CSD.Empirical.QM.andIdx_two (x y : Fin 2) : andIdx x y 2 = x * y

The gadget and the input/output states

noncomputable def CSD.Empirical.QM.measureUncompute (m : Fin 2) (ψ : QuantumInfo.QReg 3) : QuantumInfo.QReg 3

The measure-and-correct gadget, per outcome m: Hadamard the ancilla, project onto ancilla = m (the X-basis measurement), then apply the m-conditional CZ correction.

Equations

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

noncomputable def CSD.Empirical.QM.andInput (c : Fin 2 → Fin 2 → ℂ) : QuantumInfo.QReg 3

The AND-entangled input state Σ_{x,y} c_{xy} |x, y, x∧y⟩: a data superposition with the ancilla holding x ∧ y for each branch.

Equations

• CSD.Empirical.QM.andInput c = ∑ x : Fin 2, ∑ y : Fin 2, c x y • QuantumInfo.basisState (CSD.Empirical.QM.andIdx x y)

noncomputable def CSD.Empirical.QM.uncomputedData (c : Fin 2 → Fin 2 → ℂ) (m : Fin 2) : QuantumInfo.QReg 3

The uncomputed data, ancilla reset to |m⟩: Σ_{x,y} c_{xy} |x, y, m⟩.

Equations

• CSD.Empirical.QM.uncomputedData c m = ∑ x : Fin 2, ∑ y : Fin 2, c x y • QuantumInfo.basisState ![x, y, m]

Reuse / honesty bridges to the corpus Clifford gates

theorem CSD.Empirical.QM.hadEntry_eq_qmH (a b : Fin 2) : QuantumInfo.hadEntry a b = Gates.qmH a b

The ancilla-Hadamard block entries are the corpus single-qubit Hadamard qmH.

theorem CSD.Empirical.QM.czPhase_eq_qmCZ_diag : czPhase 0 0 = Gates.qmCZ 0 0 ∧ czPhase 0 1 = Gates.qmCZ 1 1 ∧ czPhase 1 0 = Gates.qmCZ 2 2 ∧ czPhase 1 1 = Gates.qmCZ 3 3

The data-CZ phase matches the corpus controlled-Z qmCZ on its diagonal (phase flip on |11⟩): the four computational diagonal values agree.

Per-component apply lemmas

theorem CSD.Empirical.QM.corr_apply (m : Fin 2) (v : QuantumInfo.QReg 3) (z : B3) : ((Matrix.toEuclideanLin (correctionMat m)) v).ofLp z = (if m = 1 then czPhase (z 0) (z 1) else 1) * v.ofLp z

theorem CSD.Empirical.QM.proj_apply (m : Fin 2) (v : QuantumInfo.QReg 3) (z : B3) : ((Matrix.toEuclideanLin (projA m)) v).ofLp z = (if z 2 = m then 1 else 0) * v.ofLp z

theorem CSD.Empirical.QM.hadEntry_zero_left (c : Fin 2) : QuantumInfo.hadEntry 0 c = (↑√2)⁻¹

The m = 0 numeric branch: the Hadamard projects the ancilla onto |0⟩ with amplitude (√2)⁻¹, independent of the data.

theorem CSD.Empirical.QM.czPhase_mul_hadEntry (x y : Fin 2) : czPhase x y * QuantumInfo.hadEntry 1 (x * y) = (↑√2)⁻¹

The genuine phase cancellation (the m = 1 branch): the (-1)^{x∧y} phase picked up by the |1⟩ projection is exactly cancelled by the data CZ, leaving amplitude (√2)⁻¹ for every data branch (x,y). This is ((-1)^{x∧y})² = 1.

theorem CSD.Empirical.QM.corr_had_eq (m x y : Fin 2) : (if m = 1 then czPhase x y else 1) * QuantumInfo.hadEntry m (x * y) = (↑√2)⁻¹

The combined correction × Hadamard-projection amplitude, both outcomes: (√2)⁻¹ for every m and every data branch (x,y). The m = 0 branch is the clean projection (hadEntry_zero_left); the m = 1 branch is the genuine phase cancellation (czPhase_mul_hadEntry).

The headline: per-basis correctness (genuine phase cancellation)

theorem CSD.Empirical.QM.measureUncompute_basisState (m x y : Fin 2) : measureUncompute m (QuantumInfo.basisState (andIdx x y)) = (↑√2)⁻¹ • QuantumInfo.basisState ![x, y, m]

Per-basis-state uncompute. For every outcome m and every data basis branch (x,y), the gadget maps the AND-entangled basis state |x, y, x∧y⟩ to (√2)⁻¹ |x, y, m⟩ — data unchanged, ancilla reset, outcome-independent after the m = 1 CZ correction. The m = 1 case is the genuine phase cancellation czPhase x y · hadEntry 1 (x∧y) = (√2)⁻¹.

Linearity wrappers

theorem CSD.Empirical.QM.measureUncompute_smul (m : Fin 2) (a : ℂ) (v : QuantumInfo.QReg 3) : measureUncompute m (a • v) = a • measureUncompute m v

theorem CSD.Empirical.QM.measureUncompute_sum {ι : Type u_1} (s : Finset ι) (f : ι → QuantumInfo.QReg 3) (m : Fin 2) : measureUncompute m (∑ i ∈ s, f i) = ∑ i ∈ s, measureUncompute m (f i)

THE headline theorem

theorem CSD.Empirical.QM.measureUncompute_uncomputes (m : Fin 2) (c : Fin 2 → Fin 2 → ℂ) : measureUncompute m (andInput c) = (↑√2)⁻¹ • uncomputedData c m

measureUncompute_uncomputes (the deliverable). For every measurement outcome m and every data superposition c, the measure-and-correct gadget maps the AND-entangled state Σ c_{xy}|x,y⟩|x∧y⟩ to the uncomputed data with the ancilla reset to |m⟩, Σ c_{xy}|x,y⟩|m⟩, scaled by the outcome amplitude (√2)⁻¹. The result is outcome-independent (the m = 1 CZ correction cancels the (-1)^{x∧y} phase): this is the net "identity-on-data ⊗ ancilla-reset".

Non-vacuity: the AND ancilla is genuinely set

theorem CSD.Empirical.QM.andInput_nontrivial : andIdx 1 1 2 = 1 ∧ QuantumInfo.basisState (andIdx 1 1) ≠ QuantumInfo.basisState ![1, 1, 0]

Non-vacuity. The AND-entangled input genuinely carries a = x ∧ y: on the |1,1⟩ data branch the ancilla is |1⟩ (the AND is set), so the entangled basis state is distinct from the ancilla-reset state — the uncompute is real work, not a trivial product.

Cost: zero Toffoli (the ~2× saving)

inductive CSD.Empirical.QM.GadgetGate : Type

An abstract gadget gate label, used only to state the Toffoli-count cost point.

• hGate : GadgetGate
• czGate : GadgetGate
• measGate : GadgetGate
• toffoli : GadgetGate

@[instance_reducible]

instance CSD.Empirical.QM.instDecidableEqGadgetGate : DecidableEq GadgetGate

Equations

• CSD.Empirical.QM.instDecidableEqGadgetGate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def CSD.Empirical.QM.GadgetGate.isToffoli : GadgetGate → Bool

Whether a gate is a Toffoli.

Equations

• CSD.Empirical.QM.GadgetGate.toffoli.isToffoli = true
• x✝.isToffoli = false

def CSD.Empirical.QM.gadgetGateList : List GadgetGate

The measure-and-correct gadget's gate list: Hadamard, measurement, conditional CZ — all Cliffords + a measurement, no Toffoli.

Equations

• CSD.Empirical.QM.gadgetGateList = [CSD.Empirical.QM.GadgetGate.hGate, CSD.Empirical.QM.GadgetGate.measGate, CSD.Empirical.QM.GadgetGate.czGate]

def CSD.Empirical.QM.unitaryUncomputeGateList : List GadgetGate

The unitary AND-uncompute's gate list: one Toffoli.

Equations

• CSD.Empirical.QM.unitaryUncomputeGateList = [CSD.Empirical.QM.GadgetGate.toffoli]

theorem CSD.Empirical.QM.gadgetGateList_zero_toffoli : List.countP GadgetGate.isToffoli gadgetGateList = 0 ∧ List.countP GadgetGate.isToffoli unitaryUncomputeGateList = 1

The cost point (list form). The measure-and-correct gadget's gate LIST ([H, Meas, CZ]) contains no Toffoli, whereas the unitary AND-uncompute's list contains exactly one — the ~2× (one-Toffoli) saving. This is a count over the gate lists; L5-b (measureUncompute_cost below) upgrades it to a property of the measureUncompute OPERATOR via the link gadgetGateList_denotes_measureUncompute.

L5-b: the operator↔list link and the cost as an operator property

noncomputable def CSD.Empirical.QM.GadgetGate.denote (g : GadgetGate) (m : Fin 2) : QuantumInfo.QReg 3 → QuantumInfo.QReg 3

Interpretation of a gadget gate as a register operator on QReg 3, parameterised by the measurement outcome m: hGate ↦ hadA, measGate ↦ projA m, czGate ↦ correctionMat m (the three Matrix.toEuclideanLin blocks that define measureUncompute). The toffoli label maps to id — it is not part of this gadget's decomposition (it is the unitary route's gate), so it plays no role in gadgetGateList; it is given a denotation only for totality.

Equations

• CSD.Empirical.QM.GadgetGate.hGate.denote m = fun (ψ : QuantumInfo.QReg 3) => (Matrix.toEuclideanLin CSD.Empirical.QM.hadA) ψ
• CSD.Empirical.QM.GadgetGate.measGate.denote m = fun (ψ : QuantumInfo.QReg 3) => (Matrix.toEuclideanLin (CSD.Empirical.QM.projA m)) ψ
• CSD.Empirical.QM.GadgetGate.czGate.denote m = fun (ψ : QuantumInfo.QReg 3) => (Matrix.toEuclideanLin (CSD.Empirical.QM.correctionMat m)) ψ
• CSD.Empirical.QM.GadgetGate.toffoli.denote m = id

noncomputable def CSD.Empirical.QM.denoteGadgetList (m : Fin 2) : List GadgetGate → QuantumInfo.QReg 3 → QuantumInfo.QReg 3

Fold a gadget gate list into an operator, applying gates left-to-right (head first).

Equations

• CSD.Empirical.QM.denoteGadgetList m [] x✝ = x✝
• CSD.Empirical.QM.denoteGadgetList m (g :: gs) x✝ = CSD.Empirical.QM.denoteGadgetList m gs (g.denote m x✝)

theorem CSD.Empirical.QM.gadgetGateList_denotes_measureUncompute (m : Fin 2) (ψ : QuantumInfo.QReg 3) : denoteGadgetList m gadgetGateList ψ = measureUncompute m ψ

The operator↔list link (L5-b, the honesty fix). Folding the interpretation of the cost-bearing gate list gadgetGateList = [hGate, measGate, czGate] reproduces the measureUncompute m operator exactly, for every input ψ.

This equality is definitional (rfl): measureUncompute m ψ is by definition the composition correctionMat m ∘ projA m ∘ hadA applied to ψ, and denoteGadgetList m gadgetGateList ψ unfolds to that same composition. The point is not a deep proof but to tie the Toffoli-count statement (gadgetGateList_zero_toffoli) to the operator: gadgetGateList is a genuine decomposition of measureUncompute, not a free-standing list.

def CSD.Empirical.QM.gadgetGateCost : GadgetGate → Reversible.Cost

Per-gate fault-tolerant cost in the corpus Reversible.Cost model. Following the corpus convention (Reversible.gateCost: single-qubit Clifford X is free, two-qubit Clifford CX costs one CNOT, CCX costs one Toffoli — the FT-expensive resource), the amplitude gadget gates are billed: hGate (single-qubit Clifford) free; czGate (two-qubit Clifford CZ ≃ CNOT up to single-qubit Cliffords) one CNOT; measGate one measurement; toffoli one Toffoli. No gate here incurs a T-count beyond the Toffoli's own (kept in the toffoli field, Pass-1 model).

Equations

• CSD.Empirical.QM.gadgetGateCost CSD.Empirical.QM.GadgetGate.hGate = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 0, tCount := 0, meas := 0 }
• CSD.Empirical.QM.gadgetGateCost CSD.Empirical.QM.GadgetGate.czGate = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 1, tCount := 0, meas := 0 }
• CSD.Empirical.QM.gadgetGateCost CSD.Empirical.QM.GadgetGate.measGate = { qubits := 0, ancilla := 0, toffoli := 0, toffoliDepth := 0, cnot := 0, tCount := 0, meas := 1 }
• CSD.Empirical.QM.gadgetGateCost CSD.Empirical.QM.GadgetGate.toffoli = { qubits := 0, ancilla := 0, toffoli := 1, toffoliDepth := 1, cnot := 0, tCount := 0, meas := 0 }

theorem CSD.Empirical.QM.measureUncompute_cost : (List.map (fun (g : GadgetGate) => (gadgetGateCost g).toffoli) gadgetGateList).sum = 0 ∧ (List.map (fun (g : GadgetGate) => (gadgetGateCost g).meas) gadgetGateList).sum = 1 ∧ (List.map (fun (g : GadgetGate) => (gadgetGateCost g).cnot) gadgetGateList).sum = 1 ∧ (List.map (fun (g : GadgetGate) => (gadgetGateCost g).toffoli) unitaryUncomputeGateList).sum = 1

The cost as an operator property (L5-b, the ~2× saving). Via the link gadgetGateList_denotes_measureUncompute, the decomposition gadgetGateList of the measureUncompute operator costs, in the corpus Reversible.Cost model:

• Toffoli 0 (the FT-expensive resource) — gadgetGateList is Toffoli-free as an operator;
• measurement 1 — the single X-basis ancilla measurement;
• CNOT 1 — the conditional CZ correction (a two-qubit Clifford, counted but cheap);

whereas the unitary AND-uncompute's decomposition unitaryUncomputeGateList costs Toffoli 1. So the measurement-based route saves the Toffoli (0 vs 1) at the cost of one measurement plus Cliffords — the ~2× per-AND-uncompute saving, with the measurement and Cliffords accounted as real but cheap resources and the Toffoli as the FT-expensive one.

Honest scope: this is a per-AND-uncompute gate-cost statement. It is not an adder- or circuit-level re-cost (that is L5-d), and it does not yet apply the gadget to Boolean arithmetic (that is L5-c, the amplitude↔Boolean bridge wall).

theorem CSD.Empirical.QM.measureUncompute_toffoli_eq_zero (m : Fin 2) : (∀ (ψ : QuantumInfo.QReg 3), denoteGadgetList m gadgetGateList ψ = measureUncompute m ψ) ∧ (List.map (fun (g : GadgetGate) => (gadgetGateCost g).toffoli) gadgetGateList).sum = 0

The Toffoli-free property of the operator (L5-b headline). There is a decomposition of the measureUncompute m operator (namely gadgetGateList, by gadgetGateList_denotes_measureUncompute) whose Reversible.Cost Toffoli count is 0. The 0-Toffoli is thus a property of the operator, not of a free-standing gate list.