The combinatorics of the [[15, 1, 3]] quantum Reed–Muller code

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

The X-stabilisers of the [[15, 1, 3]] code are the four rows of the 4 × 15 matrix H whose columns are the nonzero vectors of 𝔽₂⁴ (col j = the binary digits of j + 1): the punctured simplex code [15, 4]. A Z-error pattern e ∈ 𝔽₂¹⁵ is undetected by the X-checks iff H e = 0, i.e. e lies in the dual, the [15, 11] Hamming code.

• col, col_ne_zero, col_injective — the columns are nonzero and distinct;
• syndrome e = H e, weight e, support e, ind S (the indicator of a set of qubits);
• syndrome_ne_zero_of_weight_one, syndrome_ne_zero_of_weight_two — no undetected pattern of weight 1 or 2 (columns nonzero and distinct);
• ★ card_undetected_weight_three — exactly 35 undetected patterns of weight 3 (the triples {a, b, a + b} of nonzero vectors: the lines of PG(3, 2)), through the bijection with 3-subsets and a finite check (card_undetectedTriples, decide);
• ★ dotp_add_one — an undetected pattern of odd weight acts as the logical Z̄: on the coset x + 𝟙 of a codeword x the pairing e · (x + 𝟙) is e · x + |e|, so a Z-pattern with e · x = 0 on the X-stabiliser code picks up the sign (−1)^{|e|} on the logical 1̄;
• ★ card_undetected — the Hamming code has 2¹¹ words: syndrome is surjective (syndrome_preimage), so its kernel has dimension 11.

Honest scope

⚠️ Classical combinatorics only: the quantum statements (transversal T on the code, the projection of fifteen magic states, the 35 p³ bound) are BACKLOG #76–#78 and consume these facts.

References: S. Bravyi, A. Kitaev, PRA 71 (2005) 022316 §IV; E. Knill, R. Laflamme, W. Zurek, quant-ph/9610011 (the [[15, 1, 3]] code); F. J. MacWilliams, N. J. A. Sloane, The Theory of Error-Correcting Codes, Ch. 1 §9 (the Hamming code) and Ch. 13 (Reed–Muller codes); specs/magic-plan.md; specs/BACKLOG.md #75; specs/future-work.md.

instance ReedMuller15.instFactPrimeTwo : Fact (Nat.Prime 2)

The parity-check matrix

def ReedMuller15.col (j : Fin 15) : Fin 4 → ZMod 2

Column j of the parity-check matrix: the binary digits of j + 1, the j-th nonzero vector of 𝔽₂⁴.

Equations

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

theorem ReedMuller15.col_ne_zero (j : Fin 15) : col j ≠ 0

theorem ReedMuller15.col_injective : Function.Injective col

def ReedMuller15.syndrome (e : Fin 15 → ZMod 2) : Fin 4 → ZMod 2

The syndrome H e of a pattern e.

Equations

• ReedMuller15.syndrome e i = ∑ j : Fin 15, e j * ReedMuller15.col j i

def ReedMuller15.support (e : Fin 15 → ZMod 2) : Finset (Fin 15)

The support of a pattern.

Equations

• ReedMuller15.support e = {j : Fin 15 | e j ≠ 0}

def ReedMuller15.weight (e : Fin 15 → ZMod 2) : ℕ

The weight of a pattern.

Equations

• ReedMuller15.weight e = (ReedMuller15.support e).card

def ReedMuller15.ind (S : Finset (Fin 15)) : Fin 15 → ZMod 2

The indicator pattern of a set of qubits.

Equations

• ReedMuller15.ind S j = if j ∈ S then 1 else 0

theorem ReedMuller15.zmod_two_eq_zero_or_one (a : ZMod 2) : a = 0 ∨ a = 1

theorem ReedMuller15.zmod_two_eq_of_add_eq_zero {a b : ZMod 2} (h : a + b = 0) : a = b

theorem ReedMuller15.ind_support (e : Fin 15 → ZMod 2) : ind (support e) = e

theorem ReedMuller15.support_ind (S : Finset (Fin 15)) : support (ind S) = S

theorem ReedMuller15.weight_ind (S : Finset (Fin 15)) : weight (ind S) = S.card

theorem ReedMuller15.syndrome_add (e f : Fin 15 → ZMod 2) : syndrome (e + f) = syndrome e + syndrome f

theorem ReedMuller15.syndrome_ind (S : Finset (Fin 15)) : syndrome (ind S) = ∑ j ∈ S, col j

Weights one and two are detected

theorem ReedMuller15.syndrome_ne_zero_of_weight_one (e : Fin 15 → ZMod 2) (h : weight e = 1) : syndrome e ≠ 0

No undetected pattern of weight one: the columns are nonzero.

theorem ReedMuller15.syndrome_ne_zero_of_weight_two (e : Fin 15 → ZMod 2) (h : weight e = 2) : syndrome e ≠ 0

No undetected pattern of weight two: the columns are distinct.

Exactly 35 undetected patterns of weight three

def ReedMuller15.undetectedTriples : Finset (Finset (Fin 15))

The 3-subsets of qubits whose columns sum to zero: the lines of PG(3, 2).

Equations

• ReedMuller15.undetectedTriples = {S ∈ Finset.powersetCard 3 Finset.univ | ∑ j ∈ S, ReedMuller15.col j = 0}

theorem ReedMuller15.card_undetectedTriples : undetectedTriples.card = 35

theorem ReedMuller15.card_undetected_weight_three : {e : Fin 15 → ZMod 2 | syndrome e = 0 ∧ weight e = 3}.card = 35

★ Exactly 35 undetected patterns of weight 3.

Odd weight is the logical Z̄

def ReedMuller15.dotp (e x : Fin 15 → ZMod 2) : ZMod 2

The pairing e · x = ∑ eⱼ xⱼ in 𝔽₂.

Equations

• ReedMuller15.dotp e x = ∑ j : Fin 15, e j * x j

theorem ReedMuller15.syndrome_apply_eq_dotp (e : Fin 15 → ZMod 2) (i : Fin 4) : syndrome e i = dotp e fun (j : Fin 15) => col j i

theorem ReedMuller15.weight_cast (e : Fin 15 → ZMod 2) : ↑(weight e) = ∑ j : Fin 15, e j

theorem ReedMuller15.dotp_add_one (e x : Fin 15 → ZMod 2) : dotp e (x + 1) = dotp e x + ↑(weight e)

★ The parity rule: e · (x + 𝟙) = e · x + |e|. An undetected Z-pattern (e · x = 0 on the X-stabiliser code) acts on the logical 1̄ = 0̄ + 𝟙 with the sign (−1)^{|e|}: it is the logical Z̄ exactly when its weight is odd.

The Hamming code has 2¹¹ words

def ReedMuller15.Hmat : Matrix (Fin 4) (Fin 15) (ZMod 2)

The parity-check matrix H, columns col j.

Equations

• ReedMuller15.Hmat i j = ReedMuller15.col j i

theorem ReedMuller15.mulVec_eq_syndrome (e : Fin 15 → ZMod 2) : Hmat.mulVec e = syndrome e

def ReedMuller15.preimage (s : Fin 4 → ZMod 2) : Fin 15 → ZMod 2

A preimage of a syndrome: the unit columns sit at j = 0, 1, 3, 7.

Equations

• ReedMuller15.preimage s j = if ↑j = 0 then s 0 else if ↑j = 1 then s 1 else if ↑j = 3 then s 2 else if ↑j = 7 then s 3 else 0

theorem ReedMuller15.syndrome_preimage (s : Fin 4 → ZMod 2) : syndrome (preimage s) = s

theorem ReedMuller15.syndrome_surjective : Function.Surjective syndrome

def ReedMuller15.syndromeₗ : (Fin 15 → ZMod 2) →ₗ[ZMod 2] Fin 4 → ZMod 2

The syndrome as a linear map.

Equations

• ReedMuller15.syndromeₗ = ReedMuller15.Hmat.mulVecLin

theorem ReedMuller15.syndromeₗ_apply (e : Fin 15 → ZMod 2) : syndromeₗ e = syndrome e

theorem ReedMuller15.finrank_ker_syndromeₗ : Module.finrank (ZMod 2) ↥syndromeₗ.ker = 11

theorem ReedMuller15.card_undetected : {e : Fin 15 → ZMod 2 | syndrome e = 0}.card = 2 ^ 11

★ The Hamming code has 2¹¹ words: the undetected patterns number 2048.