Faulty gates: a transversal gadget on the Steane code, with one bad location

Category: 3-Local (Empirical, QM twin). BACKLOG #62 (a) and (b): the noise sits on the gates now, not on resting qubits, and the transversal gadgets are the code's logical gates.

Glossary: https://glossary.constraintsurfacedynamics.com/transversal-gate/ Plain-language, CSD-role and formal statements of transversal gates, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Code capacity (#51, #86) puts the errors on the seven qubits of a block and keeps every gate perfect. The circuit-level model of Aharonov–Ben-Or puts a fault at every location of the circuit — each gate of each gadget. This module does the first case of that: a transversal gadget, one single-qubit gate per qubit of the block, with one of its seven locations faulty.

• ★★ faultyTransversal_eq — error propagation: a fault at location i, acting after the ideal single-qubit gate there, makes the gadget gateOf i E * blockKron A — the ideal gadget followed by a weight-one error (blockKron_replace_eq_gateOf_mul). This is why transversal gadgets are fault-tolerant: a single fault cannot spread inside a block;
• ★★★ steane_faultyTransversal_recovery — one channel returns the ideal output of the faulty gadget, up to the scalar of #61, whenever the ideal output is a code state; ★★★ steane_faultyTransversal_recovery_unitary — exactly, for a unitary fault;
• blockKron_pX_eq_pauliMat, blockKron_pZ_eq_pauliMat — the transversal X and Z are the all-ones Paulis, the code's logical X̄ and Z̄ (a Pauli string factorises over the qubits, pauliMat_eq_blockKron, and X = onePauli 1 0, Z = onePauli 0 1), with ★ logicalX_density and ★ logicalZ_density — they flip and sign the encoded qubit;
• ★★★ steane_faultyLogicalX_recovery and ★★★ steane_faultyLogicalZ_recovery — the concrete statements: a faulty transversal logical X̄ (or Z̄) on an encoded qubit, one location bad and the fault an arbitrary unitary, is corrected — the recovery returns the ideal output;
• the transversal Hadamard, #62 (b): swapHalves exchanges the halves of a stabiliser label, so steaneA_swapHalves/steaneB_swapHalves turn the label swap of hadTransversal_conj_pauliMat into a bijection of the family; with the CSS condition bdot_steaneA_steaneB killing the sign that gives ★★ hadTransversal_conj_steaneProj — the transversal Hadamard preserves the code projector — hence ★ hadTransversal_code_state, and ★★ hadTransversal_conj_logicalX / _logicalZ: it exchanges X̄ and Z̄, the logical Hadamard in the Heisenberg picture. ★★★ steane_faultyHadamard_recovery is then (a)'s theorem for the Hadamard gadget;
• ★★ steane_circuit_threshold — the accounting: a circuit of N such gadgets, faults independent at rate p < 1/21, reaches every accuracy at some concatenation level (exists_level_circuitMeasure_lt with C(7, 2) = 21).

Honest scope

⚠️ Faulty gates, ideal recovery. The recovery channel here is the perfect one of #14(b): faults inside the recovery gadget — hence extended rectangles, and with them the simulation theorem that makes the levels compose — are not treated. That is what BACKLOG #62 (c) and (d) hold.

⚠️ One fault per gadget, level one. The quantum statement is for a single faulty location of a single transversal gadget on one block. The recursion over levels is the probabilistic one (circuitMeasure_circuitBad_le): what a level-k gadget does when its pattern is good is #86's theorem at code capacity, not a statement about faulty gates.

⚠️ A transversal gadget is not a universal gate set: blockKron A for arbitrary A need not preserve the code space, which is why the general theorem carries that as a hypothesis — discharged here for X̄, Z̄ and the Hadamard. The two-block transversal CNOT is not here because it needs a faulty-gadget theorem across two blocks, a different statement from (a)'s; that is SteaneTransversalCNOT.lean (#62 (f), landed 2026-09-28).

⚠️ The Hadamard's logical action is proved in the Heisenberg picture (where X̄ and Z̄ go) and through the projector, which is what fault tolerance needs. That H^{⊗ 7}|0̄⟩ = (|0̄⟩ + |1̄⟩)/√2 in the Schrödinger picture — the MacWilliams/coset computation — is not proved here.

References: D. Aharonov, M. Ben-Or, SIAM J. Comput. 38 (2008); P. Aliferis, D. Gottesman, J. Preskill, Quantum Inf. Comput. 6 (2006); A. Steane, PRL 77 (1996); Empirical/QM/QEC/SteaneArbitrary.lean (#61), Mathlib/Probability/CircuitThreshold.lean (#62); specs/BACKLOG.md #62; specs/steane-plan.md.

Error propagation through a transversal gadget

theorem CSD.Empirical.QM.QEC.Steane.faultyTransversal_eq (A : Fin 7 → Matrix (Fin 2) (Fin 2) ℂ) (i : Fin 7) (E : Matrix (Fin 2) (Fin 2) ℂ) : (QuantumInfo.blockKron fun (b : Fin 7) => if b = i then E * A i else A b) = QuantumInfo.Controlled.gateOf i E * QuantumInfo.blockKron A

★★ A fault at one location of a transversal gadget is a weight-one error. The gadget whose factor at i is E * A i — the ideal gate there, followed by the fault — is the ideal gadget followed by the single-qubit error E.

theorem CSD.Empirical.QM.QEC.Steane.conj_vecMulVec {n : Type u_1} [Fintype n] (M : Matrix n n ℂ) (v : n → ℂ) : M * Matrix.vecMulVec v (star v) * M.conjTranspose = Matrix.vecMulVec (M.mulVec v) (star (M.mulVec v))

Conjugating a rank-one density operator by a matrix acts on the vector.

One faulty location is corrected

theorem CSD.Empirical.QM.QEC.Steane.steane_faultyTransversal_recovery : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (A : Fin 7 → Matrix (Fin 2) (Fin 2) ℂ) (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), QuantumInfo.blockKron A * ρ * (QuantumInfo.blockKron A).conjTranspose = steaneProj * (QuantumInfo.blockKron A * ρ * (QuantumInfo.blockKron A).conjTranspose) * steaneProj → ∀ (i : Fin 7) (E : Matrix (Fin 2) (Fin 2) ℂ), R.apply ((QuantumInfo.blockKron fun (b : Fin 7) => if b = i then E * A i else A b) * ρ * (QuantumInfo.blockKron fun (b : Fin 7) => if b = i then E * A i else A b).conjTranspose) = ((star (E 0 0) * E 0 0 + star (E 0 1) * E 0 1 + star (E 1 0) * E 1 0 + star (E 1 1) * E 1 1) / 2) • (QuantumInfo.blockKron A * ρ * (QuantumInfo.blockKron A).conjTranspose)

★★★ A transversal gadget with one faulty location is corrected. For every transversal gadget whose ideal output on ρ is a code state, and every fault E at one of the seven locations, one channel returns that ideal output — up to the scalar tr(EᴴE)/2 of #61, since a non-unitary fault is trace-decreasing.

theorem CSD.Empirical.QM.QEC.Steane.steane_faultyTransversal_recovery_unitary : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (A : Fin 7 → Matrix (Fin 2) (Fin 2) ℂ) (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), QuantumInfo.blockKron A * ρ * (QuantumInfo.blockKron A).conjTranspose = steaneProj * (QuantumInfo.blockKron A * ρ * (QuantumInfo.blockKron A).conjTranspose) * steaneProj → ∀ (i : Fin 7), ∀ E ∈ Matrix.unitaryGroup (Fin 2) ℂ, R.apply ((QuantumInfo.blockKron fun (b : Fin 7) => if b = i then E * A i else A b) * ρ * (QuantumInfo.blockKron fun (b : Fin 7) => if b = i then E * A i else A b).conjTranspose) = QuantumInfo.blockKron A * ρ * (QuantumInfo.blockKron A).conjTranspose

★★★ A unitary fault at one location is undone exactly: the scalar is 1.

The transversal X and Z are the logical X̄ and Z̄

theorem CSD.Empirical.QM.QEC.Steane.onePauli_one_zero : QuantumInfo.onePauli 1 0 = pX

theorem CSD.Empirical.QM.QEC.Steane.onePauli_zero_one : QuantumInfo.onePauli 0 1 = pZ

theorem CSD.Empirical.QM.QEC.Steane.blockKron_pX_eq_pauliMat : (QuantumInfo.blockKron fun (x : Fin 7) => pX) = QuantumInfo.pauliMat allOnes 0

The transversal X on the seven qubits is the all-ones Pauli, the code's logical X̄: a Pauli string factorises over the qubits (pauliMat_eq_blockKron) and X = onePauli 1 0.

theorem CSD.Empirical.QM.QEC.Steane.blockKron_pZ_eq_pauliMat : (QuantumInfo.blockKron fun (x : Fin 7) => pZ) = QuantumInfo.pauliMat 0 allOnes

The transversal Z is the other all-ones Pauli, the code's logical Z̄.

theorem CSD.Empirical.QM.QEC.Steane.pauliMat_allOnes_mulVec_logicalVec (a b : ℂ) : (QuantumInfo.pauliMat allOnes 0).mulVec (logicalVec a b) = logicalVec b a

The all-ones Pauli flips the encoded qubit: a|0̄⟩ + b|1̄⟩ ↦ b|0̄⟩ + a|1̄⟩.

theorem CSD.Empirical.QM.QEC.Steane.logicalX_density (a b : ℂ) : (QuantumInfo.blockKron fun (x : Fin 7) => pX) * Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) * (QuantumInfo.blockKron fun (x : Fin 7) => pX).conjTranspose = Matrix.vecMulVec (logicalVec b a) (star (logicalVec b a))

★ The transversal X flips the encoded qubit's density operator.

theorem CSD.Empirical.QM.QEC.Steane.steane_faultyLogicalX_recovery : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (a b : ℂ) (i : Fin 7), ∀ E ∈ Matrix.unitaryGroup (Fin 2) ℂ, R.apply ((QuantumInfo.blockKron fun (q : Fin 7) => if q = i then E * pX else pX) * Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) * (QuantumInfo.blockKron fun (q : Fin 7) => if q = i then E * pX else pX).conjTranspose) = Matrix.vecMulVec (logicalVec b a) (star (logicalVec b a))

★★★ A faulty transversal logical X̄ is corrected. The gadget is the transversal X on the seven qubits — the code's logical X̄ — with an arbitrary unitary fault at one of its seven locations. One channel returns the ideal output: the encoded qubit with its amplitudes exchanged.

theorem CSD.Empirical.QM.QEC.Steane.pauliMat_zero_allOnes_mulVec_logicalVec (a b : ℂ) : (QuantumInfo.pauliMat 0 allOnes).mulVec (logicalVec a b) = logicalVec a (-b)

The all-ones Z Pauli signs the encoded qubit's second amplitude: Z̄ on a|0̄⟩ + b|1̄⟩.

theorem CSD.Empirical.QM.QEC.Steane.logicalZ_density (a b : ℂ) : (QuantumInfo.blockKron fun (x : Fin 7) => pZ) * Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) * (QuantumInfo.blockKron fun (x : Fin 7) => pZ).conjTranspose = Matrix.vecMulVec (logicalVec a (-b)) (star (logicalVec a (-b)))

★ The transversal Z signs the encoded qubit's density operator.

theorem CSD.Empirical.QM.QEC.Steane.steane_faultyLogicalZ_recovery : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (a b : ℂ) (i : Fin 7), ∀ E ∈ Matrix.unitaryGroup (Fin 2) ℂ, R.apply ((QuantumInfo.blockKron fun (q : Fin 7) => if q = i then E * pZ else pZ) * Matrix.vecMulVec (logicalVec a b) (star (logicalVec a b)) * (QuantumInfo.blockKron fun (q : Fin 7) => if q = i then E * pZ else pZ).conjTranspose) = Matrix.vecMulVec (logicalVec a (-b)) (star (logicalVec a (-b)))

★★★ A faulty transversal logical Z̄ is corrected, with the ideal output the signed encoded qubit.

The transversal Hadamard preserves the code space

def CSD.Empirical.QM.QEC.Steane.swapHalves (x : Fin 6 → Fin 2) : Fin 6 → Fin 2

Swapping the two halves of a stabiliser label: in Fin 6 that is k ↦ k + 3.

Equations

• CSD.Empirical.QM.QEC.Steane.swapHalves x k = x (k + 3)

theorem CSD.Empirical.QM.QEC.Steane.swapHalves_involutive : Function.Involutive swapHalves

theorem CSD.Empirical.QM.QEC.Steane.steaneA_swapHalves (x : Fin 6 → Fin 2) : steaneA (swapHalves x) = steaneB x

The swap exchanges the X-labels for the Z-labels of the stabiliser family.

theorem CSD.Empirical.QM.QEC.Steane.steaneB_swapHalves (x : Fin 6 → Fin 2) : steaneB (swapHalves x) = steaneA x

theorem CSD.Empirical.QM.QEC.Steane.bdot_steaneA_steaneB (x : Fin 6 → Fin 2) : QuantumInfo.bdot (steaneA x) (steaneB x) = 0

The CSS condition on the family's labels: every X-label is orthogonal to every Z-label, so the transversal Hadamard's sign is 1.

theorem CSD.Empirical.QM.QEC.Steane.hadTransversal_conj_steaneProj : QuantumInfo.hadTransversal 7 * steaneProj * QuantumInfo.hadTransversal 7 = steaneProj

★★ The transversal Hadamard preserves the Steane code projector. The Hadamard exchanges the X- and Z-labels of every group element (hadTransversal_conj_pauliMat), the CSS condition kills the sign, and swapping the halves of the label is a bijection of the family — so the group average comes back to itself.

theorem CSD.Empirical.QM.QEC.Steane.steaneProj_mul_hadTransversal : steaneProj * QuantumInfo.hadTransversal 7 = QuantumInfo.hadTransversal 7 * steaneProj

theorem CSD.Empirical.QM.QEC.Steane.hadTransversal_code_state {ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ} (hρ : ρ = steaneProj * ρ * steaneProj) : QuantumInfo.hadTransversal 7 * ρ * (QuantumInfo.hadTransversal 7).conjTranspose = steaneProj * (QuantumInfo.hadTransversal 7 * ρ * (QuantumInfo.hadTransversal 7).conjTranspose) * steaneProj

★ The transversal Hadamard maps code states to code states, which is what the faulty-gadget theorem needs of the ideal gadget.

theorem CSD.Empirical.QM.QEC.Steane.hadTransversal_conj_logicalX : QuantumInfo.hadTransversal 7 * QuantumInfo.pauliMat allOnes 0 * QuantumInfo.hadTransversal 7 = QuantumInfo.pauliMat 0 allOnes

★★ The transversal Hadamard exchanges the logical X̄ and Z̄ — the logical Hadamard in the Heisenberg picture.

theorem CSD.Empirical.QM.QEC.Steane.hadTransversal_conj_logicalZ : QuantumInfo.hadTransversal 7 * QuantumInfo.pauliMat 0 allOnes * QuantumInfo.hadTransversal 7 = QuantumInfo.pauliMat allOnes 0

theorem CSD.Empirical.QM.QEC.Steane.steane_faultyHadamard_recovery : ∃ (R : QuantumInfo.Channel (Fin 7 → Fin 2) (Fin 7 → Fin 2) (Option SingleErr)), ∀ (ρ : Matrix (Fin 7 → Fin 2) (Fin 7 → Fin 2) ℂ), ρ = steaneProj * ρ * steaneProj → ∀ (i : Fin 7), ∀ E ∈ Matrix.unitaryGroup (Fin 2) ℂ, R.apply ((QuantumInfo.blockKron fun (q : Fin 7) => if q = i then E * QuantumInfo.CliffordT.hGateM else QuantumInfo.CliffordT.hGateM) * ρ * (QuantumInfo.blockKron fun (q : Fin 7) => if q = i then E * QuantumInfo.CliffordT.hGateM else QuantumInfo.CliffordT.hGateM).conjTranspose) = QuantumInfo.hadTransversal 7 * ρ * (QuantumInfo.hadTransversal 7).conjTranspose

★★★ A faulty transversal Hadamard is corrected. The gadget is the Hadamard on all seven qubits — a logical Hadamard, by hadTransversal_conj_logicalX/_logicalZ — with an arbitrary unitary fault at one of its seven locations; one channel returns the ideal output.

The circuit-level accounting

theorem CSD.Empirical.QM.QEC.Steane.steane_circuit_threshold (N : ℕ) (ν : MeasureTheory.Measure Bool) [MeasureTheory.IsProbabilityMeasure ν] {p ε : ℝ} (hp : 0 ≤ p) (hν : ν {c : Bool | c = true} ≤ ENNReal.ofReal p) (hthr : p < 1 / 21) (hε : 0 < ε) : ∃ (k : ℕ), (circuitMeasure N 7 ν k) (circuitBad N 7 k) < ENNReal.ofReal ε

★★ The threshold for a circuit of transversal gadgets. Each of the N gadgets of the circuit has seven locations, faults are independent with rate at most p, and a gadget is bad when two or more of its locations are (which is the case steane_faultyTransversal_recovery excludes). Below p < 1/21 every accuracy is reached at some concatenation level.