The [[15, 1, 3]] code space and its transversal T

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

The logical states of the [[15, 1, 3]] quantum Reed–Muller code, in the coordinate-operator model of Pauli.lean/Magic.lean on QReg 15: |0̄⟩ = ∑_{x ∈ C} |x⟩ and |1̄⟩ = ∑_{x ∈ C} |x + 𝟙⟩, with C the [15, 4] simplex code spanned by the four rows of the parity-check matrix (ReedMuller15.col), unnormalised (‖·‖ = 4). The X-stabilisers X^{row i} permute the codewords and fix both logical states (pauliOp_row_logical0/1). Every codeword has weight 0 or 8 and every word of the coset C + 𝟙 has weight 7 or 15 (weight_codeword, weight_codeword_add_one, finite checks), so the transversal T, T^{⊗15}, whose coordinate action is |x⟩ ↦ e^{iπ|x|/4}|x⟩, fixes |0̄⟩ and multiplies |1̄⟩ by e^{−iπ/4}: it acts on the logical qubit as T†. Applied to the encoded |+̄⟩ = |0̄⟩ + |1̄⟩ it produces the encoded T†|+⟩, the magic state up to the Clifford S (S T† = T).

• row i, codeword a, codeword_injective; wt — the weight on Fin 15 → Fin 2;
• weight_codeword, weight_codeword_add_one — the weights 0/8 and 7/15 (the triorthogonality of the code, in the form the transversal gate needs);
• logical0, logical1, logicalPlus; pauliOp_basisState_zero, ★ pauliOp_row_logical0/1 — the X-stabilisers fix the logical states;
• tTrans — the transversal T as a coordinate operator, tTrans_eq_comp — it is the composite of the fifteen single-qubit T gates; tTrans_basisState;
• ★★ tTrans_logical0, tTrans_logical1 — T^{⊗15} is the logical T†; ★ tTrans_logicalPlus — the encoded magic state |0̄⟩ + e^{−iπ/4}|1̄⟩.

Honest scope

⚠️ The code space is presented by its two logical states, not as the range of the fourteen-generator stabiliser average of Stabilizer.lean; the Z-stabilisers and the action of Z-error patterns on the logical states are BACKLOG #77, the distillation bound #78.

References: S. Bravyi, A. Kitaev, PRA 71 (2005) 022316 §IV; E. Knill, R. Laflamme, W. Zurek, quant-ph/9610011; S. Bravyi, J. Haah, PRA 86 (2012) 052329 (triorthogonal codes); specs/magic-plan.md; specs/BACKLOG.md #76; specs/future-work.md.

The simplex code on Fin 2 labels

def QuantumInfo.ReedMuller15.row (i : Fin 4) : Fin 15 → Fin 2

Row i of the parity-check matrix, as a Fin 2 label.

Equations

• QuantumInfo.ReedMuller15.row i j = if (↑j + 1).testBit ↑i = true then 1 else 0

def QuantumInfo.ReedMuller15.codeword (a : Fin 4 → Fin 2) : Fin 15 → Fin 2

The codeword ∑ᵢ aᵢ · row i of the [15, 4] simplex code.

Equations

• QuantumInfo.ReedMuller15.codeword a j = ∑ i : Fin 4, a i * QuantumInfo.ReedMuller15.row i j

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

The weight of a Fin 2 label.

Equations

• QuantumInfo.ReedMuller15.wt x = {j : Fin 15 | x j = 1}.card

theorem QuantumInfo.ReedMuller15.codeword_injective : Function.Injective codeword

theorem QuantumInfo.ReedMuller15.weight_codeword (a : Fin 4 → Fin 2) : wt (codeword a) = 0 ∨ wt (codeword a) = 8

Every codeword has weight 0 or 8.

theorem QuantumInfo.ReedMuller15.weight_codeword_add_one (a : Fin 4 → Fin 2) : wt (codeword a + 1) = 7 ∨ wt (codeword a + 1) = 15

Every word of the coset C + 𝟙 has weight 7 or 15.

theorem QuantumInfo.ReedMuller15.codeword_add_row (a : Fin 4 → Fin 2) (i : Fin 4) : codeword a + row i = codeword (a + Pi.single i 1)

X^{row i} permutes the codewords: codeword a + row i = codeword (a + eᵢ).

The logical states and the X-stabilisers

noncomputable def QuantumInfo.ReedMuller15.logical0 : QReg 15

|0̄⟩ = ∑_{x ∈ C} |x⟩ (unnormalised).

Equations

• QuantumInfo.ReedMuller15.logical0 = ∑ a : Fin 4 → Fin 2, QuantumInfo.basisState (QuantumInfo.ReedMuller15.codeword a)

noncomputable def QuantumInfo.ReedMuller15.logical1 : QReg 15

|1̄⟩ = ∑_{x ∈ C} |x + 𝟙⟩ (unnormalised).

Equations

• QuantumInfo.ReedMuller15.logical1 = ∑ a : Fin 4 → Fin 2, QuantumInfo.basisState (QuantumInfo.ReedMuller15.codeword a + 1)

noncomputable def QuantumInfo.ReedMuller15.logicalPlus : QReg 15

The encoded |+̄⟩, unnormalised: |0̄⟩ + |1̄⟩.

Equations

• QuantumInfo.ReedMuller15.logicalPlus = QuantumInfo.ReedMuller15.logical0 + QuantumInfo.ReedMuller15.logical1

theorem QuantumInfo.ReedMuller15.fin2_add_add_self (x a : Fin 15 → Fin 2) : x + a + a = x

theorem QuantumInfo.ReedMuller15.pauliOp_basisState_zero (a x : Fin 15 → Fin 2) : pauliOp a 0 (basisState x) = basisState (x + a)

X^a moves a basis state: X^a |x⟩ = |x + a⟩.

theorem QuantumInfo.ReedMuller15.pauliOp_row_logical0 (i : Fin 4) : pauliOp (row i) 0 logical0 = logical0

★ The X-stabilisers fix |0̄⟩.

theorem QuantumInfo.ReedMuller15.pauliOp_row_logical1 (i : Fin 4) : pauliOp (row i) 0 logical1 = logical1

★ The X-stabilisers fix |1̄⟩.

The transversal T

noncomputable def QuantumInfo.ReedMuller15.tTrans (ψ : QReg 15) : QReg 15

The transversal T gate T^{⊗15}: |x⟩ ↦ e^{iπ|x|/4}|x⟩.

Equations

• QuantumInfo.ReedMuller15.tTrans ψ = (WithLp.equiv 2 ((Fin 15 → Fin 2) → ℂ)).symm fun (z : Fin 15 → Fin 2) => QuantumInfo.tPhase ^ QuantumInfo.ReedMuller15.wt z * ψ.ofLp z

@[simp]

theorem QuantumInfo.ReedMuller15.tTrans_apply (ψ : QReg 15) (z : Fin 15 → Fin 2) : (tTrans ψ).ofLp z = tPhase ^ wt z * ψ.ofLp z

theorem QuantumInfo.ReedMuller15.fin2_val_eq_ite (v : Fin 2) : ↑v = if v = 1 then 1 else 0

theorem QuantumInfo.ReedMuller15.wt_eq_sum (z : Fin 15 → Fin 2) : wt z = ∑ j : Fin 15, ↑(z j)

theorem QuantumInfo.ReedMuller15.finRange_fifteen : List.finRange 15 = [0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14]

theorem QuantumInfo.ReedMuller15.tTrans_eq_comp (ψ : QReg 15) : tTrans ψ = tGate 0 (tGate 1 (tGate 2 (tGate 3 (tGate 4 (tGate 5 (tGate 6 (tGate 7 (tGate 8 (tGate 9 (tGate 10 (tGate 11 (tGate 12 (tGate 13 (tGate 14 ψ))))))))))))))

Transversality: tTrans is the composite of the fifteen single-qubit T gates.

theorem QuantumInfo.ReedMuller15.tTrans_sum {κ : Type u_1} (s : Finset κ) (f : κ → QReg 15) : tTrans (∑ k ∈ s, f k) = ∑ k ∈ s, tTrans (f k)

theorem QuantumInfo.ReedMuller15.tTrans_add (ψ φ : QReg 15) : tTrans (ψ + φ) = tTrans ψ + tTrans φ

theorem QuantumInfo.ReedMuller15.tTrans_smul (c : ℂ) (ψ : QReg 15) : tTrans (c • ψ) = c • tTrans ψ

theorem QuantumInfo.ReedMuller15.tTrans_basisState (x : Fin 15 → Fin 2) : tTrans (basisState x) = tPhase ^ wt x • basisState x

theorem QuantumInfo.ReedMuller15.tPhase_pow_seven : tPhase ^ 7 = tPhaseInv

theorem QuantumInfo.ReedMuller15.tPhase_pow_fifteen : tPhase ^ 15 = tPhaseInv

theorem QuantumInfo.ReedMuller15.tTrans_logical0 : tTrans logical0 = logical0

★★ T^{⊗15} fixes |0̄⟩: every codeword has weight 0 or 8.

theorem QuantumInfo.ReedMuller15.tTrans_logical1 : tTrans logical1 = tPhaseInv • logical1

★★ T^{⊗15} multiplies |1̄⟩ by e^{−iπ/4}: every word of the coset has weight 7 or 15. Together with tTrans_logical0: the transversal T is the logical T†.

theorem QuantumInfo.ReedMuller15.tTrans_logicalPlus : tTrans logicalPlus = logical0 + tPhaseInv • logical1

★ The encoded magic state: T^{⊗15}|+̄⟩ = |0̄⟩ + e^{−iπ/4}|1̄⟩, the encoded T†|+⟩.