Hybrid circuits: reversible gates and measure-and-correct gadgets on the full register

Category: 1-Mathlib (CSD-free; staged as a Mathlib-upstream candidate).

Lift.lean embeds one CCX into QReg m as a permutation matrix and notes that a mid-circuit measurement gadget is not a permutation, so the basis-state induction that lifts a permutation circuit "breaks at the replaced block". This module closes that gap without the tensor factorisation the note anticipated: the gadget, per outcome, is a monomial operator — it sends every computational basis state to a scalar multiple of a basis state — so the induction goes through with a scalar carried along.

• gateMat g — the general lift of a reversible gate: the permutation matrix of its Boolean action denoteGate g, recast through stateOfReg/regOfState; gateMat_basisState is the basis-state rule, and gateMat_CCX checks it against the hand-built CCX unitary ccxAtMat.
• measureCorrectMat pairs g mo — the measure-and-correct gadget on the ancilla g, per outcome mo: Hadamard on g, projection of g onto mo, then a CZ on each pair of pairs when mo = 1. On a basis state it is (phase · ⟨mo|H|w g⟩) • |update w g mo⟩ (measureCorrectMat_basisState); when the ancilla holds the parity of ANDs the corrections cancel, w g = andParity pairs w, the scalar is (√2)⁻¹ for both outcomes (measureCorrect_scalar) — the genuine phase cancellation ((−1)^{p})² = 1; when it does not, the mo = 1 branch carries the sign −(√2)⁻¹ (measureCorrect_scalar_of_ne) — the reason a gadget must be matched to what its ancilla holds.
• HybridGate, hybridLin, shadow, WellFormed, gadgetCount — a hybrid gate list, its register semantics (a linear map, first gate first), its Boolean shadow (a reversible gate acts by denoteGate, a gadget writes its outcome into the ancilla), and the well-formedness of a run on a basis input (every gadget meets an ancilla holding the parity its corrections cancel, on wires its corrections avoid).
• ★ hybridLin_basisState — the hybrid amplitude equality: on a well-formed basis input the hybrid circuit produces (√2)⁻¹^{#gadgets} • |shadow⟩; hybridLin_sum extends it by linearity to superpositions of well-formed inputs.

The consumer is the AND-adder with its Toffoli-free uncompute pass (Empirical/QM/MeasurementAdderHybrid.lean), where the gadgets are matched to the majority ancillas of the carry cells.

Honest scope

The gadget is represented per outcome (a partial isometry), as in the measurement-gadget modules it generalises; the two outcomes have probability 1/2 each, which the scalar (√2)⁻¹ records. Nothing here is about noise or about gate decompositions: gateMat is the permutation a reversible gate is on the computational basis, and a hybrid list is costed by its consumers.

The recasts round-trip

@[simp]

theorem Reversible.stateOfReg_regOfState {m : ℕ} (s : State m) : stateOfReg (regOfState s) = s

@[simp]

theorem Reversible.regOfState_stateOfReg {m : ℕ} (w : Fin m → Fin 2) : regOfState (stateOfReg w) = w

The general lift of a reversible gate

noncomputable def Reversible.gateMat {m : ℕ} (g : Gate m) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The permutation matrix of a reversible gate on QReg m: the basis state w goes to the basis state of the gate's Boolean action on w.

Equations

• Reversible.gateMat g = Matrix.of fun (z w : Fin m → Fin 2) => if z = Reversible.regOfState (Reversible.denoteGate g (Reversible.stateOfReg w)) then 1 else 0

theorem Reversible.gateMat_apply {m : ℕ} (g : Gate m) (z w : Fin m → Fin 2) : gateMat g z w = if z = regOfState (denoteGate g (stateOfReg w)) then 1 else 0

theorem Reversible.gateMat_basisState {m : ℕ} (g : Gate m) (w : Fin m → Fin 2) : (Matrix.toEuclideanLin (gateMat g)) (QuantumInfo.basisState w) = QuantumInfo.basisState (regOfState (denoteGate g (stateOfReg w)))

The lifted gate permutes basis states by the gate's Boolean action.

theorem Reversible.gateMat_CCX {m : ℕ} (wa wb wg : Fin m) (hga : wg ≠ wa) (hgb : wg ≠ wb) : gateMat (Gate.CCX wa wb wg) = ccxAtMat wa wb wg

The general lift agrees with the hand-built CCX unitary of Lift.lean.

The measure-and-correct gadget at arbitrary wires

def Reversible.andParity {m : ℕ} (pairs : List (Fin m × Fin m)) (w : Fin m → Fin 2) : Fin 2

The parity of ANDs a correction list reads: ⊕_{(x,y) ∈ pairs} w x ∧ w y, as a Fin 2.

Equations

• Reversible.andParity pairs w = (List.map (fun (p : Fin m × Fin m) => w p.1 * w p.2) pairs).sum

def Reversible.correctionPhase {m : ℕ} (pairs : List (Fin m × Fin m)) (mo : Fin 2) (w : Fin m → Fin 2) : ℂ

The correction phase at outcome mo: (−1)^{mo · ⊕ ANDs} — a CZ on each pair when mo = 1, nothing when mo = 0.

Equations

• Reversible.correctionPhase pairs mo w = (-1) ^ (↑mo * ↑(Reversible.andParity pairs w))

theorem Reversible.neg_one_pow_fin_add (a b : Fin 2) : (-1) ^ ↑(a + b) = (-1) ^ ↑a * (-1) ^ ↑b

theorem Reversible.neg_one_pow_fin_mul (a b : Fin 2) : (-1) ^ ↑(a * b) = (-1) ^ (↑a * ↑b)

theorem Reversible.correctionPhase_one_eq_prod {m : ℕ} (pairs : List (Fin m × Fin m)) (w : Fin m → Fin 2) : correctionPhase pairs 1 w = (List.map (fun (p : Fin m × Fin m) => (-1) ^ (↑(w p.1) * ↑(w p.2))) pairs).prod

The correction at outcome 1 is the product of the per-pair CZ phases.

noncomputable def Reversible.measureCorrectMat {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (mo : Fin 2) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The measure-and-correct gadget on the ancilla wire g of QReg m, per outcome mo: Hadamard on g, projection of g onto mo, then a CZ on each pair of pairs if mo = 1. Entry (z, w): nonzero only for z = update w g mo, where it is the correction phase at z times the Hadamard entry ⟨mo|H|w g⟩.

Equations

• Reversible.measureCorrectMat pairs g mo = Matrix.of fun (z w : Fin m → Fin 2) => if z = Function.update w g mo then Reversible.correctionPhase pairs mo z * QuantumInfo.hadEntry mo (w g) else 0

theorem Reversible.measureCorrectMat_apply {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (mo : Fin 2) (z w : Fin m → Fin 2) : measureCorrectMat pairs g mo z w = if z = Function.update w g mo then correctionPhase pairs mo z * QuantumInfo.hadEntry mo (w g) else 0

theorem Reversible.measureCorrectMat_basisState {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (mo : Fin 2) (w : Fin m → Fin 2) : (Matrix.toEuclideanLin (measureCorrectMat pairs g mo)) (QuantumInfo.basisState w) = (correctionPhase pairs mo (Function.update w g mo) * QuantumInfo.hadEntry mo (w g)) • QuantumInfo.basisState (Function.update w g mo)

The gadget is monomial: a basis state goes to a scalar multiple of a basis state.

theorem Reversible.andParity_update_of_forall_ne {m : ℕ} (pairs : List (Fin m × Fin m)) {g : Fin m} (hg : ∀ p ∈ pairs, p.1 ≠ g ∧ p.2 ≠ g) (w : Fin m → Fin 2) (mo : Fin 2) : andParity pairs (Function.update w g mo) = andParity pairs w

Corrections that avoid the ancilla read the same parity before and after the reset.

theorem Reversible.measureCorrect_scalar {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (mo : Fin 2) (w : Fin m → Fin 2) (hg : ∀ p ∈ pairs, p.1 ≠ g ∧ p.2 ≠ g) (hw : w g = andParity pairs w) : correctionPhase pairs mo (Function.update w g mo) * QuantumInfo.hadEntry mo (w g) = (↑√2)⁻¹

The gadget scalar on a well-formed input. If the ancilla holds the parity its corrections cancel, the scalar is (√2)⁻¹ for both outcomes: the projection phase (−1)^{mo · w g} and the correction phase (−1)^{mo · parity} cancel.

theorem Reversible.measureCorrect_scalar_of_ne {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (w : Fin m → Fin 2) (hg : ∀ p ∈ pairs, p.1 ≠ g ∧ p.2 ≠ g) (hw : w g ≠ andParity pairs w) : correctionPhase pairs 1 (Function.update w g 1) * QuantumInfo.hadEntry 1 (w g) = -(↑√2)⁻¹

The sign flip on an ill-formed input. If the ancilla does not hold the parity the corrections cancel, the mo = 1 branch carries −(√2)⁻¹: a data-dependent relative phase.

Hybrid gate lists

inductive Reversible.HybridGate (m : ℕ) : Type

A hybrid gate: a reversible gate, or a measure-and-correct gadget with its outcome.

• gate {m : ℕ} (g : Gate m) : HybridGate m

  A reversible gate, lifted as a permutation.

• measure {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (mo : Fin 2) : HybridGate m

  The measure-and-correct gadget on ancilla g with corrections pairs, at outcome mo.

noncomputable def Reversible.HybridGate.mat {m : ℕ} : HybridGate m → Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The register operator of a hybrid gate.

Equations

• (Reversible.HybridGate.gate g).mat = Reversible.gateMat g
• (Reversible.HybridGate.measure pairs g mo).mat = Reversible.measureCorrectMat pairs g mo

def Reversible.HybridGate.shadow {m : ℕ} : HybridGate m → (Fin m → Fin 2) → Fin m → Fin 2

The Boolean shadow of a hybrid gate on register indices: a reversible gate acts by its denoteGate, a gadget writes its outcome into the ancilla.

Equations

• (Reversible.HybridGate.gate g).shadow x✝ = Reversible.regOfState (Reversible.denoteGate g (Reversible.stateOfReg x✝))
• (Reversible.HybridGate.measure pairs g mo).shadow x✝ = Function.update x✝ g mo

noncomputable def Reversible.hybridLin {m : ℕ} : List (HybridGate m) → QuantumInfo.QReg m →ₗ[ℂ] QuantumInfo.QReg m

The register semantics of a hybrid gate list, first gate first.

Equations

• Reversible.hybridLin [] = LinearMap.id
• Reversible.hybridLin (h :: rest) = Reversible.hybridLin rest ∘ₗ Matrix.toEuclideanLin h.mat

theorem Reversible.hybridLin_nil {m : ℕ} (ψ : QuantumInfo.QReg m) : (hybridLin []) ψ = ψ

theorem Reversible.hybridLin_cons {m : ℕ} (h : HybridGate m) (rest : List (HybridGate m)) (ψ : QuantumInfo.QReg m) : (hybridLin (h :: rest)) ψ = (hybridLin rest) ((Matrix.toEuclideanLin h.mat) ψ)

theorem Reversible.hybridLin_append {m : ℕ} (l₁ l₂ : List (HybridGate m)) (ψ : QuantumInfo.QReg m) : (hybridLin (l₁ ++ l₂)) ψ = (hybridLin l₂) ((hybridLin l₁) ψ)

theorem Reversible.stateOfReg_shadow_gate {m : ℕ} (g : Gate m) (w : Fin m → Fin 2) : stateOfReg ((HybridGate.gate g).shadow w) = denoteGate g (stateOfReg w)

The Boolean reading of a reversible gate's shadow is its denoteGate.

theorem Reversible.stateOfReg_update {m : ℕ} (w : Fin m → Fin 2) (g : Fin m) (mo : Fin 2) : stateOfReg (Function.update w g mo) = Function.update (stateOfReg w) g (decide (mo = 1))

The Boolean reading of a gadget's shadow is the ancilla reset to the outcome.

theorem Reversible.shadow_gate_apply_of_not_mem_target {m : ℕ} (g : Gate m) (w : Fin m → Fin 2) {i : Fin m} (hi : i ∉ gateTarget g) : (HybridGate.gate g).shadow w i = w i

A reversible gate's shadow preserves every wire it does not target.

theorem Reversible.val_eq_of_stateOfReg_eq {m : ℕ} {u : Fin m → Fin 2} {T : State m} {i : Fin m} (h : stateOfReg u i = T i) : u i = if T i = true then 1 else 0

A register value from its Boolean reading.

def Reversible.shadow {m : ℕ} (l : List (HybridGate m)) (w : Fin m → Fin 2) : Fin m → Fin 2

The Boolean shadow of a hybrid gate list.

Equations

• Reversible.shadow l w = List.foldl (fun (w : Fin m → Fin 2) (h : Reversible.HybridGate m) => h.shadow w) w l

theorem Reversible.shadow_nil {m : ℕ} (w : Fin m → Fin 2) : shadow [] w = w

theorem Reversible.shadow_cons {m : ℕ} (h : HybridGate m) (rest : List (HybridGate m)) (w : Fin m → Fin 2) : shadow (h :: rest) w = shadow rest (h.shadow w)

theorem Reversible.shadow_append {m : ℕ} (l₁ l₂ : List (HybridGate m)) (w : Fin m → Fin 2) : shadow (l₁ ++ l₂) w = shadow l₂ (shadow l₁ w)

def Reversible.gadgetCount {m : ℕ} : List (HybridGate m) → ℕ

The number of gadgets in a hybrid gate list.

Equations

• Reversible.gadgetCount [] = 0
• Reversible.gadgetCount (Reversible.HybridGate.gate g :: rest) = Reversible.gadgetCount rest
• Reversible.gadgetCount (Reversible.HybridGate.measure pairs g mo :: rest) = Reversible.gadgetCount rest + 1

def Reversible.WellFormed {m : ℕ} : List (HybridGate m) → (Fin m → Fin 2) → Prop

Well-formed run on a basis input: every gadget meets an ancilla holding the parity its corrections cancel, on wires its corrections avoid.

Equations

• One or more equations did not get rendered due to their size.
• Reversible.WellFormed [] x✝ = True
• Reversible.WellFormed (Reversible.HybridGate.gate g :: rest) x✝ = Reversible.WellFormed rest (Reversible.regOfState (Reversible.denoteGate g (Reversible.stateOfReg x✝)))

theorem Reversible.wellFormed_nil {m : ℕ} (w : Fin m → Fin 2) : WellFormed [] w

theorem Reversible.wellFormed_gate_cons {m : ℕ} (g : Gate m) (rest : List (HybridGate m)) (w : Fin m → Fin 2) : WellFormed (HybridGate.gate g :: rest) w ↔ WellFormed rest (regOfState (denoteGate g (stateOfReg w)))

theorem Reversible.wellFormed_measure_cons {m : ℕ} (pairs : List (Fin m × Fin m)) (g : Fin m) (mo : Fin 2) (rest : List (HybridGate m)) (w : Fin m → Fin 2) : WellFormed (HybridGate.measure pairs g mo :: rest) w ↔ (∀ p ∈ pairs, p.1 ≠ g ∧ p.2 ≠ g) ∧ w g = andParity pairs w ∧ WellFormed rest (Function.update w g mo)

★ The hybrid amplitude equality

theorem Reversible.hybridLin_basisState {m : ℕ} (l : List (HybridGate m)) (w : Fin m → Fin 2) : WellFormed l w → (hybridLin l) (QuantumInfo.basisState w) = (↑√2)⁻¹ ^ gadgetCount l • QuantumInfo.basisState (shadow l w)

★ The hybrid amplitude equality on a well-formed basis input. The hybrid circuit sends the basis state w to (√2)⁻¹^{#gadgets} • |shadow⟩: each reversible gate permutes the basis state, each gadget resets its ancilla to the outcome and contributes the scalar (√2)⁻¹.

theorem Reversible.hybridLin_sum {m : ℕ} {ι : Type u_1} (l : List (HybridGate m)) (S : Finset ι) (c : ι → ℂ) (w : ι → Fin m → Fin 2) (h : ∀ i ∈ S, WellFormed l (w i)) : (hybridLin l) (∑ i ∈ S, c i • QuantumInfo.basisState (w i)) = (↑√2)⁻¹ ^ gadgetCount l • ∑ i ∈ S, c i • QuantumInfo.basisState (shadow l (w i))

The hybrid amplitude equality on a superposition of well-formed basis inputs.

Reversible prefixes

theorem Reversible.shadow_gate_list {m : ℕ} (c : Circuit m) (w : Fin m → Fin 2) : shadow (List.map HybridGate.gate c) w = regOfState (denote c (stateOfReg w))

The shadow of a reversible gate list is its Boolean semantics, recast.

theorem Reversible.wellFormed_gate_list_append {m : ℕ} (c : Circuit m) (rest : List (HybridGate m)) (w : Fin m → Fin 2) : WellFormed (List.map HybridGate.gate c ++ rest) w ↔ WellFormed rest (regOfState (denote c (stateOfReg w)))

A reversible prefix only moves the basis input; well-formedness is decided after it.

theorem Reversible.gadgetCount_gate_list_append {m : ℕ} (c : Circuit m) (rest : List (HybridGate m)) : gadgetCount (List.map HybridGate.gate c ++ rest) = gadgetCount rest