The decoder of the [[15, 1, 3]] protocol as an explicit CNOT circuit

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #79, the last part of R-004's protocol (specs/magic-plan.md, "The split"): #77 read the output off the logical coefficients of the accepted state, and this file decodes it with a circuit.

The [15, 4] simplex code has a linear logical-Z readout. Columns 1, 2, 3 of the parity-check matrix sum to zero, so f(x) = x₀ + x₁ + x₂ vanishes on every codeword (logicalBit_codeword) and is 1 on the all-ones shift codeword a + 𝟙 (logicalBit_add_one). The decoder therefore needs no Hadamard: sixteen CNOTs suffice.

The CNOT layer (general m, namespace Controlled)

cnotAct a b is the label action of CNOT, an involution once a ≠ b (cnotAct_cnotAct), and ★ cnotGate'_apply identifies #83's matrix as its permutation matrix — the bridge from the entry algebra of ControlledGate.lean to a map on bitstrings, in the same shape as xGate_apply. On amplitudes a CNOT is a pullback, ★ cnotGate'_mulVec_apply: (C v)(k) = v (cnotAct a b k), and ★★ cnotListMat_mulVec_apply iterates that over a list of CNOTs (cnotListMat, the product with the first gate of the list rightmost, unitary by cnotListMat_mem_unitaryGroup): the amplitude map is the reversed composition cnotListPull.

The decoder (m = 15)

• decoderList is the circuit: CNOT(1 → 0) and CNOT(2 → 0) compute the logical bit onto wire 0, then CNOT(0 → j) for j = 1, …, 14 clear the all-ones component from the other wires — sixteen gates (decoderList_length), and decoderCircuit is their product;
• ★ cnotListPull_decoderList: the circuit pulls labels back by decodeLabelInv, so ★★ decoderCircuit_mulVec_apply and toEuclideanLin_decoderCircuit_apply give every decoded amplitude as (D ψ)(z) = ψ (decodeLabelInv z). decodeLabelInv is inverse to decodeLabel (decodeLabel_decodeLabelInv, decodeLabelInv_decodeLabel), which is the forward reading: ★ decoderCircuit_mulVec_basisState, D|x⟩ = |decodeLabel x⟩, the logical bit on wire 0 and the all-ones component cleared;
• ★★ decoderCircuit_logical_update: wire 0 carries the logical qubit. For every label k of the other fourteen wires the decoded amplitude at k[0 ↦ 1] is λ times the one at k[0 ↦ 0], where λ is the logical coefficient of the input |0̄⟩ + λ|1̄⟩. The ratio is the same whatever the fourteen residual wires carry, which is why measuring them does not disturb wire 0. The pair is not vacuous: decoderCircuit_logical_apply_zero gives amplitude 1 at the zero label;
• ★★★ decoderCircuit_encodedMagic and decoderCircuit_encodedMagic_apply: the decoded output is #77's outQubit e. For an undetected pattern e the amplitudes on wire 0 are those of outQubit e = |0⟩ + (−1)^{|e|} e^{−iπ/4}|1⟩, which is √2 · Z^{|e|} T†|+⟩ (outQubit_eq) and the magic state up to the Clifford S (sGate_magicConj).

The mechanism in one line is decodeLabelInv_update_one: decodeLabelInv (k[0 ↦ 1]) = decodeLabelInv (k[0 ↦ 0]) + 𝟙. The 1-sector of wire 0 pulls back to the coset C + 𝟙, which is exactly where |1̄⟩ lives, and the 0-sector pulls back into the kernel of the readout, where |1̄⟩ has no amplitude at all (logical1_apply_of_logicalBit_zero).

Honest scope

⚠️ The fourteen residual wires are not exhibited as a tensor factor: what is proved is the amplitude ratio at every residual label, the same statement in coordinates. A factorised form would need the relabelling (Fin 15 → Fin 2) ≃ Fin 2 × (Fin 14 → Fin 2). ⚠️ No measurement of the residual wires is modelled here; the row's "measures the fourteen syndrome qubits" is covered only in the sense above, that the ratio does not depend on their label. ⚠️ The circuit is a product of CNOTs, hence Clifford, but the corpus has no IsClifford predicate: the claim is carried by the explicit list decoderList and by unitarity (decoderCircuit_mem_unitaryGroup). BACKLOG #79 priced a CNOT/H circuit; the Hadamard turned out to be unnecessary for this code. ⚠️ Nothing here normalises anything: logical0, logical1 and outQubit are the unnormalised states of #76 and #77.

Source

S. Bravyi, A. Kitaev, PRA 71 (2005) 022316 §IV; QuantumInfo/ReedMuller15Code.lean (#76), QuantumInfo/ReedMuller15Errors.lean (#77), QuantumInfo/ControlledGate.lean (#83); specs/magic-plan.md; specs/BACKLOG.md #79; specs/future-work.md.

CNOT as a permutation of the computational basis

def QuantumInfo.Controlled.cnotAct {m : ℕ} (a b : Fin m) (x : Fin m → Fin 2) : Fin m → Fin 2

The label action of CNOT with control a and target b: the target gains the control.

Equations

• QuantumInfo.Controlled.cnotAct a b x = Function.update x b (x b + x a)

@[simp]

theorem QuantumInfo.Controlled.cnotAct_apply_self {m : ℕ} (a b : Fin m) (x : Fin m → Fin 2) : cnotAct a b x b = x b + x a

theorem QuantumInfo.Controlled.cnotAct_apply_of_ne {m : ℕ} {a b i : Fin m} (hi : i ≠ b) (x : Fin m → Fin 2) : cnotAct a b x i = x i

@[simp]

theorem QuantumInfo.Controlled.cnotAct_cnotAct {m : ℕ} {a b : Fin m} (hab : a ≠ b) (x : Fin m → Fin 2) : cnotAct a b (cnotAct a b x) = x

CNOT is an involution on labels.

theorem QuantumInfo.Controlled.cnotAct_eq_iff {m : ℕ} {a b : Fin m} (hab : a ≠ b) {k x : Fin m → Fin 2} : cnotAct a b k = x ↔ k = cnotAct a b x

theorem QuantumInfo.Controlled.blockEntry_flip (p q : Fin 2) : MultiControlled.blockEntry p q 0 1 1 0 = if q = p + 1 then 1 else 0

The 2 × 2 block of CNOT is the bit flip, read as a condition on the two labels.

theorem QuantumInfo.Controlled.cnotGate'_apply {m : ℕ} {a b : Fin m} (hab : a ≠ b) (k l : Fin m → Fin 2) : cnotGate' a b k l = if l = cnotAct a b k then 1 else 0

★ CNOT is the permutation matrix of cnotAct — the same shape as xGate_apply.

theorem QuantumInfo.Controlled.cnotGate'_mulVec_apply {m : ℕ} {a b : Fin m} (hab : a ≠ b) (v : (Fin m → Fin 2) → ℂ) (k : Fin m → Fin 2) : (cnotGate' a b).mulVec v k = v (cnotAct a b k)

★ CNOT on amplitudes is the pullback along cnotAct.

A list of CNOTs

noncomputable def QuantumInfo.Controlled.cnotListMat {m : ℕ} (l : List (Fin m × Fin m)) : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ

The matrix of a list of CNOTs: the first gate of the list acts first, so it is rightmost in the product.

Equations

• QuantumInfo.Controlled.cnotListMat l = List.foldr (fun (p : Fin m × Fin m) (M : Matrix (Fin m → Fin 2) (Fin m → Fin 2) ℂ) => M * QuantumInfo.Controlled.cnotGate' p.1 p.2) 1 l

@[simp]

theorem QuantumInfo.Controlled.cnotListMat_nil {m : ℕ} : cnotListMat [] = 1

@[simp]

theorem QuantumInfo.Controlled.cnotListMat_cons {m : ℕ} (p : Fin m × Fin m) (l : List (Fin m × Fin m)) : cnotListMat (p :: l) = cnotListMat l * cnotGate' p.1 p.2

def QuantumInfo.Controlled.cnotListPull {m : ℕ} (l : List (Fin m × Fin m)) (k : Fin m → Fin 2) : Fin m → Fin 2

The label map a list of CNOTs pulls amplitudes back along: the reversed composition, so the last gate of the list is applied first.

Equations

• QuantumInfo.Controlled.cnotListPull l k = List.foldr (fun (p : Fin m × Fin m) (y : Fin m → Fin 2) => QuantumInfo.Controlled.cnotAct p.1 p.2 y) k l

@[simp]

theorem QuantumInfo.Controlled.cnotListPull_nil {m : ℕ} (k : Fin m → Fin 2) : cnotListPull [] k = k

@[simp]

theorem QuantumInfo.Controlled.cnotListPull_cons {m : ℕ} (p : Fin m × Fin m) (l : List (Fin m × Fin m)) (k : Fin m → Fin 2) : cnotListPull (p :: l) k = cnotAct p.1 p.2 (cnotListPull l k)

theorem QuantumInfo.Controlled.cnotListMat_mulVec_apply {m : ℕ} (l : List (Fin m × Fin m)) : (∀ p ∈ l, p.1 ≠ p.2) → ∀ (v : (Fin m → Fin 2) → ℂ) (k : Fin m → Fin 2), (cnotListMat l).mulVec v k = v (cnotListPull l k)

★★ A CNOT circuit acts on amplitudes as one label pullback.

theorem QuantumInfo.Controlled.cnotListMat_mem_unitaryGroup {m : ℕ} (l : List (Fin m × Fin m)) : (∀ p ∈ l, p.1 ≠ p.2) → cnotListMat l ∈ Matrix.unitaryGroup (Fin m → Fin 2) ℂ

The logical readout of the simplex code

def QuantumInfo.ReedMuller15.logicalBit (x : Fin 15 → Fin 2) : Fin 2

The logical Z readout f(x) = x₀ + x₁ + x₂: zero on the code, one on its all-ones shift.

Equations

• QuantumInfo.ReedMuller15.logicalBit x = x 0 + x 1 + x 2

theorem QuantumInfo.ReedMuller15.logicalBit_add_one (x : Fin 15 → Fin 2) : logicalBit (x + 1) = logicalBit x + 1

theorem QuantumInfo.ReedMuller15.logicalBit_codeword (a : Fin 4 → Fin 2) : logicalBit (codeword a) = 0

The readout vanishes on the code: columns 1, 2, 3 of the parity-check matrix sum to zero.

theorem QuantumInfo.ReedMuller15.logicalBit_update_zero (k : Fin 15 → Fin 2) (v : Fin 2) : logicalBit (Function.update k 0 v) = v + k 1 + k 2

The label map of the decoder and its inverse

def QuantumInfo.ReedMuller15.decodeLabel (x : Fin 15 → Fin 2) (j : Fin 15) : Fin 2

What the decoder does to a label: the readout onto wire 0, cleared from the others.

Equations

• QuantumInfo.ReedMuller15.decodeLabel x j = if j = 0 then QuantumInfo.ReedMuller15.logicalBit x else x j + QuantumInfo.ReedMuller15.logicalBit x

theorem QuantumInfo.ReedMuller15.decodeLabel_zero (x : Fin 15 → Fin 2) : decodeLabel x 0 = logicalBit x

theorem QuantumInfo.ReedMuller15.decodeLabel_of_ne {j : Fin 15} (hj : j ≠ 0) (x : Fin 15 → Fin 2) : decodeLabel x j = x j + logicalBit x

def QuantumInfo.ReedMuller15.decodeLabelInv (y : Fin 15 → Fin 2) (j : Fin 15) : Fin 2

The inverse label map: wire 0 is added back to the others, and the readout of the result lands on wire 0.

Equations

• QuantumInfo.ReedMuller15.decodeLabelInv y j = if j = 0 then QuantumInfo.ReedMuller15.logicalBit y else y j + y 0

theorem QuantumInfo.ReedMuller15.decodeLabelInv_zero (y : Fin 15 → Fin 2) : decodeLabelInv y 0 = logicalBit y

theorem QuantumInfo.ReedMuller15.decodeLabelInv_of_ne {j : Fin 15} (hj : j ≠ 0) (y : Fin 15 → Fin 2) : decodeLabelInv y j = y j + y 0

theorem QuantumInfo.ReedMuller15.logicalBit_decodeLabel (x : Fin 15 → Fin 2) : logicalBit (decodeLabel x) = x 0

theorem QuantumInfo.ReedMuller15.logicalBit_decodeLabelInv (y : Fin 15 → Fin 2) : logicalBit (decodeLabelInv y) = y 0

theorem QuantumInfo.ReedMuller15.decodeLabel_decodeLabelInv (y : Fin 15 → Fin 2) : decodeLabel (decodeLabelInv y) = y

theorem QuantumInfo.ReedMuller15.decodeLabelInv_decodeLabel (x : Fin 15 → Fin 2) : decodeLabelInv (decodeLabel x) = x

The circuit

def QuantumInfo.ReedMuller15.cleanTargets : List (Fin 15)

The targets of the clearing layer: every wire but 0.

Equations

• QuantumInfo.ReedMuller15.cleanTargets = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14]

theorem QuantumInfo.ReedMuller15.mem_cleanTargets {j : Fin 15} (hj : j ≠ 0) : j ∈ cleanTargets

def QuantumInfo.ReedMuller15.decoderList : List (Fin 15 × Fin 15)

The decoder: CNOT(1 → 0) and CNOT(2 → 0) compute the logical bit onto wire 0, then CNOT(0 → j) clears it from every other wire. Sixteen gates, no Hadamard.

Equations

• QuantumInfo.ReedMuller15.decoderList = (1, 0) :: (2, 0) :: List.map (fun (t : Fin 15) => (0, t)) QuantumInfo.ReedMuller15.cleanTargets

theorem QuantumInfo.ReedMuller15.decoderList_length : decoderList.length = 16

theorem QuantumInfo.ReedMuller15.ne_zero_of_mem_cleanTargets {t : Fin 15} (ht : t ∈ cleanTargets) : t ≠ 0

theorem QuantumInfo.ReedMuller15.decoderList_ne (p : Fin 15 × Fin 15) : p ∈ decoderList → p.1 ≠ p.2

noncomputable def QuantumInfo.ReedMuller15.decoderCircuit : Matrix (Fin 15 → Fin 2) (Fin 15 → Fin 2) ℂ

The decoder circuit, as the product of its sixteen CNOT matrices.

Equations

• QuantumInfo.ReedMuller15.decoderCircuit = QuantumInfo.Controlled.cnotListMat QuantumInfo.ReedMuller15.decoderList

theorem QuantumInfo.ReedMuller15.decoderCircuit_mem_unitaryGroup : decoderCircuit ∈ Matrix.unitaryGroup (Fin 15 → Fin 2) ℂ

theorem QuantumInfo.ReedMuller15.cnotListPull_clean (l : List (Fin 15)) : 0 ∉ l → l.Nodup → ∀ (y : Fin 15 → Fin 2) (j : Fin 15), Controlled.cnotListPull (List.map (fun (t : Fin 15) => (0, t)) l) y j = if j ∈ l then y j + y 0 else y j

The clearing layer adds wire 0 to each of its targets.

theorem QuantumInfo.ReedMuller15.cnotListPull_decoderList (y : Fin 15 → Fin 2) : Controlled.cnotListPull decoderList y = decodeLabelInv y

★ The circuit pulls labels back by decodeLabelInv.

theorem QuantumInfo.ReedMuller15.decoderCircuit_mulVec_apply (v : (Fin 15 → Fin 2) → ℂ) (z : Fin 15 → Fin 2) : decoderCircuit.mulVec v z = v (decodeLabelInv z)

★★ Every decoded amplitude.

theorem QuantumInfo.ReedMuller15.toEuclideanLin_decoderCircuit_apply (ψ : QReg 15) (z : Fin 15 → Fin 2) : ((Matrix.toEuclideanLin decoderCircuit) ψ).ofLp z = ψ.ofLp (decodeLabelInv z)

The same, on register states.

theorem QuantumInfo.ReedMuller15.decoderCircuit_mulVec_basisState (x : Fin 15 → Fin 2) : decoderCircuit.mulVec (basisState x).ofLp = (basisState (decodeLabel x)).ofLp

★ The forward reading: the circuit sends the basis label x to decodeLabel x, the logical bit on wire 0 and the all-ones component cleared from the rest.

The logical states under the decoder

theorem QuantumInfo.ReedMuller15.logical0_apply (x : Fin 15 → Fin 2) : logical0.ofLp x = ∑ a : Fin 4 → Fin 2, if x = codeword a then 1 else 0

theorem QuantumInfo.ReedMuller15.logical1_apply (x : Fin 15 → Fin 2) : logical1.ofLp x = ∑ a : Fin 4 → Fin 2, if x = codeword a + 1 then 1 else 0

theorem QuantumInfo.ReedMuller15.logical1_apply_of_logicalBit_zero {x : Fin 15 → Fin 2} (hx : logicalBit x = 0) : logical1.ofLp x = 0

|1̄⟩ has no amplitude where the readout vanishes: its labels are the coset C + 𝟙.

theorem QuantumInfo.ReedMuller15.logical0_apply_add_one (x : Fin 15 → Fin 2) : logical0.ofLp (x + 1) = logical1.ofLp x

theorem QuantumInfo.ReedMuller15.logical1_apply_add_one (x : Fin 15 → Fin 2) : logical1.ofLp (x + 1) = logical0.ofLp x

theorem QuantumInfo.ReedMuller15.logical0_apply_zero : logical0.ofLp 0 = 1

Wire 0 carries the logical qubit

theorem QuantumInfo.ReedMuller15.decodeLabelInv_update_one (k : Fin 15 → Fin 2) : decodeLabelInv (Function.update k 0 1) = decodeLabelInv (Function.update k 0 0) + 1

The mechanism. The 1-sector of wire 0 pulls back to the all-ones shift of the 0-sector — the coset C + 𝟙, which is where |1̄⟩ lives.

theorem QuantumInfo.ReedMuller15.decodeLabelInv_zero_label : decodeLabelInv 0 = 0

theorem QuantumInfo.ReedMuller15.decoderCircuit_logical_update (lam : ℂ) (k : Fin 15 → Fin 2) : ((Matrix.toEuclideanLin decoderCircuit) (logical0 + lam • logical1)).ofLp (Function.update k 0 1) = lam * ((Matrix.toEuclideanLin decoderCircuit) (logical0 + lam • logical1)).ofLp (Function.update k 0 0)

★★ The decoded state carries the logical qubit on wire 0. Whatever the other fourteen wires do, the amplitude in the 1-sector of wire 0 is λ times the amplitude in the 0-sector: the decoded state is |0⟩ + λ|1⟩ on wire 0, uniformly in the residual label.

theorem QuantumInfo.ReedMuller15.decoderCircuit_logical_apply_zero (lam : ℂ) : ((Matrix.toEuclideanLin decoderCircuit) (logical0 + lam • logical1)).ofLp 0 = 1

The pair above is not vacuous: the 0-sector carries amplitude 1 at the zero label.

The decoded output of the protocol

theorem QuantumInfo.ReedMuller15.outQubit_apply_zero (e : Fin 15 → Fin 2) : ((outQubit e).ofLp fun (x : Fin 1) => 0) = 1

theorem QuantumInfo.ReedMuller15.outQubit_apply_one (e : Fin 15 → Fin 2) : ((outQubit e).ofLp fun (x : Fin 1) => 1) = signChar (parity e) * tPhaseInv

theorem QuantumInfo.ReedMuller15.decoderCircuit_encodedMagic {e : Fin 15 → Fin 2} (he : syndromeF e = 0) (k : Fin 15 → Fin 2) (v : Fin 2) : ((Matrix.toEuclideanLin decoderCircuit) (pauliOp 0 e (tTrans logicalPlus))).ofLp (Function.update k 0 v) = ((outQubit e).ofLp fun (x : Fin 1) => v) * ((Matrix.toEuclideanLin decoderCircuit) (pauliOp 0 e (tTrans logicalPlus))).ofLp (Function.update k 0 0)

★★★ The decoder outputs outQubit e on wire 0. For an undetected pattern e, the decoded amplitudes of the accepted state on wire 0 are exactly those of #77's outQubit e = |0⟩ + (−1)^{|e|} e^{−iπ/4}|1⟩, at every label of the other fourteen wires.

theorem QuantumInfo.ReedMuller15.decoderCircuit_encodedMagic_apply {e : Fin 15 → Fin 2} (he : syndromeF e = 0) (v : Fin 2) : ((Matrix.toEuclideanLin decoderCircuit) (pauliOp 0 e (tTrans logicalPlus))).ofLp (Function.update 0 0 v) = (outQubit e).ofLp fun (x : Fin 1) => v

★★★ The output qubit, with its amplitudes. At the zero label of the other fourteen wires the decoded amplitudes are those of outQubit e: the protocol's output is √2 · Z^{|e|} T†|+⟩ (outQubit_eq), the magic state up to the Clifford S (sGate_magicConj).