Z-error patterns on the encoded magic state: detection and the logical Z̄

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #77, part (c) of R-004 (specs/magic-plan.md, "The split").

The 15-to-1 protocol injects T (BACKLOG #66–#67) into each qubit of the encoded |+̄⟩; a noisy resource leaves a Z-error pattern e ∈ 𝔽₂¹⁵ on the encoded magic state |Ā'⟩ = T^{⊗15}|+̄⟩ = |0̄⟩ + e^{−iπ/4}|1̄⟩ (tTrans_logicalPlus), i.e. the state Z_e |Ā'⟩. The X-checks X^{row i} are then measured:

• Z_e commutes with X^{row i} up to the sign (−1)^{(syndrome e)ᵢ} (pauliOp_z_comm_row), so on any state fixed by the checks the measurement of check i is deterministic with outcome (syndrome e)ᵢ (★ measProj_row_z): a pattern with nonzero syndrome is rejected with certainty (exists_reject_of_syndrome_ne_zero), a pattern with zero syndrome passes every check;
• an undetected pattern acts on the code space as the logical Z̄ to the power of its parity: Z_e|0̄⟩ = |0̄⟩ and Z_e|1̄⟩ = (−1)^{|e|}|1̄⟩ (pauliOp_z_logical0/1, from bdot_codeword — a pattern orthogonal to the rows is orthogonal to the code — and bdot e 𝟙 = |e| mod 2, parity_val, parity_eq_one_iff_odd); ★★ pauliOp_z_encodedMagic: the accepted state is |0̄⟩ + (−1)^{|e|} e^{−iπ/4}|1̄⟩, the encoded T†|+⟩ for even |e| and its logical Z̄-flip for odd |e|;
• reading the logical coefficients as a qubit (outQubit e), the output is √2 · T†|+⟩ for even |e| and √2 · Z T†|+⟩ for odd |e| (outQubit_eq, magicConj), and S T†|+⟩ = |A⟩ (sGate_magicConj): the protocol distils the magic state up to the Clifford S.

syndromeF (on Fin 2 labels) agrees with ReedMuller15.syndrome (syndromeF_eq), so the counts of ReedMuller15.lean apply: no undetected pattern of weight 1 or 2, exactly 35 of weight 3, 2¹¹ in all.

Honest scope

⚠️ The output is read off the logical coefficients here; the explicit decoding circuit is QuantumInfo/ReedMuller15Decoder.lean (BACKLOG #79, 2026-09-27), sixteen CNOTs that put those coefficients on wire 0. The probabilities over the pattern under independent noise, and the 35 p³ bound, are BACKLOG #78.

References: S. Bravyi, A. Kitaev, PRA 71 (2005) 022316 §IV; specs/magic-plan.md; specs/BACKLOG.md #77; specs/future-work.md.

The syndrome on Fin 2 labels

def QuantumInfo.ReedMuller15.syndromeF (e : Fin 15 → Fin 2) : Fin 4 → Fin 2

The X-check syndrome of a Z-pattern: (syndrome e)ᵢ = e · row i.

Equations

• QuantumInfo.ReedMuller15.syndromeF e i = QuantumInfo.bdot e (QuantumInfo.ReedMuller15.row i)

def QuantumInfo.ReedMuller15.parity (e : Fin 15 → Fin 2) : Fin 2

The parity e · 𝟙 = |e| mod 2 of a pattern.

Equations

• QuantumInfo.ReedMuller15.parity e = QuantumInfo.bdot e 1

theorem QuantumInfo.ReedMuller15.col_eq_row (j : Fin 15) (i : Fin 4) : ReedMuller15.col j i = row i j

The rows are the columns of ReedMuller15.lean (ZMod 2 is Fin 2).

theorem QuantumInfo.ReedMuller15.syndromeF_eq (e : Fin 15 → Fin 2) : syndromeF e = ReedMuller15.syndrome e

The Fin 2 syndrome is the ZMod 2 syndrome of ReedMuller15.lean, definitionally.

theorem QuantumInfo.ReedMuller15.parity_cast (e : Fin 15 → Fin 2) : parity e = ↑(wt e)

theorem QuantumInfo.ReedMuller15.parity_val (e : Fin 15 → Fin 2) : ↑(parity e) = wt e % 2

e · 𝟙 is the weight mod 2.

theorem QuantumInfo.ReedMuller15.parity_eq_one_iff_odd (e : Fin 15 → Fin 2) : parity e = 1 ↔ Odd (wt e)

The parity is 1 exactly for odd weight.

Z_e against the X-checks

theorem QuantumInfo.ReedMuller15.pauliOp_basisState_z (e x : Fin 15 → Fin 2) : pauliOp 0 e (basisState x) = pauliSign e x • basisState x

Z_e |x⟩ = (−1)^{e · x} |x⟩.

theorem QuantumInfo.ReedMuller15.pauliOp_z_comm_row (e : Fin 15 → Fin 2) (i : Fin 4) (ψ : QReg 15) : pauliOp (row i) 0 (pauliOp 0 e ψ) = signChar (syndromeF e i) • pauliOp 0 e (pauliOp (row i) 0 ψ)

Z_e X^{row i} = (−1)^{(syndrome e)ᵢ} X^{row i} Z_e.

theorem QuantumInfo.ReedMuller15.measProj_row_z (e : Fin 15 → Fin 2) (i : Fin 4) {ψ : QReg 15} (hfix : pauliOp (row i) 0 ψ = ψ) : measProj (row i) 0 (syndromeF e i) (pauliOp 0 e ψ) = pauliOp 0 e ψ ∧ measProj (row i) 0 (syndromeF e i + 1) (pauliOp 0 e ψ) = 0

★ The X-check i on Z_e ψ̄ is deterministic with outcome (syndrome e)ᵢ, for any ψ̄ fixed by X^{row i}.

theorem QuantumInfo.ReedMuller15.fin2_add_one_eq_zero_of_ne_zero {v : Fin 2} (h : v ≠ 0) : v + 1 = 0

theorem QuantumInfo.ReedMuller15.exists_reject_of_syndrome_ne_zero {e : Fin 15 → Fin 2} (he : syndromeF e ≠ 0) {ψ : QReg 15} (hfix : ∀ (i : Fin 4), pauliOp (row i) 0 ψ = ψ) : ∃ (i : Fin 4), measProj (row i) 0 0 (pauliOp 0 e ψ) = 0

A detected pattern is rejected with certainty: some X-check has zero amplitude for the +1 outcome.

theorem QuantumInfo.ReedMuller15.measProj_row_z_zero {e : Fin 15 → Fin 2} (he : syndromeF e = 0) (i : Fin 4) {ψ : QReg 15} (hfix : pauliOp (row i) 0 ψ = ψ) : measProj (row i) 0 0 (pauliOp 0 e ψ) = pauliOp 0 e ψ

An undetected pattern passes every X-check with certainty.

Undetected patterns act as the logical Z̄^{parity}

theorem QuantumInfo.ReedMuller15.bdot_codeword (e : Fin 15 → Fin 2) (a : Fin 4 → Fin 2) : bdot e (codeword a) = ∑ i : Fin 4, a i * bdot e (row i)

theorem QuantumInfo.ReedMuller15.bdot_codeword_eq_zero {e : Fin 15 → Fin 2} (he : syndromeF e = 0) (a : Fin 4 → Fin 2) : bdot e (codeword a) = 0

A pattern orthogonal to the rows is orthogonal to the code.

theorem QuantumInfo.ReedMuller15.pauliOp_z_logical0 {e : Fin 15 → Fin 2} (he : syndromeF e = 0) : pauliOp 0 e logical0 = logical0

★ An undetected Z-pattern fixes |0̄⟩.

theorem QuantumInfo.ReedMuller15.pauliOp_z_logical1 {e : Fin 15 → Fin 2} (he : syndromeF e = 0) : pauliOp 0 e logical1 = signChar (parity e) • logical1

★ An undetected Z-pattern multiplies |1̄⟩ by (−1)^{|e|}.

theorem QuantumInfo.ReedMuller15.pauliOp_row_tTrans_logicalPlus (i : Fin 4) : pauliOp (row i) 0 (tTrans logicalPlus) = tTrans logicalPlus

The encoded magic state is fixed by every X-check.

theorem QuantumInfo.ReedMuller15.pauliOp_z_encodedMagic {e : Fin 15 → Fin 2} (he : syndromeF e = 0) : pauliOp 0 e (tTrans logicalPlus) = logical0 + (signChar (parity e) * tPhaseInv) • logical1

★★ The accepted state: an undetected pattern e turns the encoded magic state into |0̄⟩ + (−1)^{|e|} e^{−iπ/4}|1̄⟩ — the encoded T†|+⟩ for even |e|, its logical Z̄-flip for odd.

The decoded output

noncomputable def QuantumInfo.ReedMuller15.magicConj : QReg 1

The conjugate magic state T†|+⟩ = T† H |0⟩.

Equations

• QuantumInfo.ReedMuller15.magicConj = QuantumInfo.tGateInv 0 (QuantumInfo.hGate 0 (QuantumInfo.basisState fun (x : Fin 1) => 0))

theorem QuantumInfo.ReedMuller15.sGate_magicConj : sGate 0 magicConj = magicState

S T†|+⟩ = |A⟩: the distilled state is the magic state up to the Clifford S.

theorem QuantumInfo.ReedMuller15.magicConj_apply (z : Fin 1 → Fin 2) : magicConj.ofLp z = (↑√2)⁻¹ * tPhaseInv ^ ↑(z 0)

noncomputable def QuantumInfo.ReedMuller15.outQubit (e : Fin 15 → Fin 2) : QReg 1

The logical coefficients of the accepted state, read as one qubit: |0⟩ + (−1)^{|e|} e^{−iπ/4}|1⟩.

Equations

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

noncomputable def QuantumInfo.ReedMuller15.zPow (s : Fin 2) (ψ : QReg 1) : QReg 1

Z^s on one qubit.

Equations

• QuantumInfo.ReedMuller15.zPow s ψ = if s = 0 then ψ else QuantumInfo.pauliOp 0 (QuantumInfo.unitV 0) ψ

theorem QuantumInfo.ReedMuller15.outQubit_eq (e : Fin 15 → Fin 2) : outQubit e = ↑√2 • zPow (parity e) magicConj

★ The output is √2 · Z^{|e|} T†|+⟩: the conjugate magic state for even |e|, its Z-flip for odd |e|.