The Shor 9-qubit code, by concatenation (§Q Q5, E1)

Category: 5-Empirical-QM. The last iconic empirical item (specs/BACKLOG.md E1 / §Q Q5): the 9-qubit code that corrects an arbitrary single-qubit Pauli error, built as the concatenation of the two landed 3-qubit halves — the phase-flip code (PhaseFlip.lean) outside, the bit-flip code (ThreeQubit.lean) inside.

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

The combinator, and why 512 dimensions never appear entry-wise

The E1 row recorded the obstacle as dimensional: entry-wise tactics do not survive 2⁹ = 512. The route chosen here is the row's code-concatenation combinator option. One structural lemma does all the lifting:

• kron_mulVec / tel9_bkron_vkron — the block Kronecker action factorises, (A ⊗ B ⊗ C)(u ⊗ v ⊗ w) = (Au) ⊗ (Bv) ⊗ (Cw).

Every 9-qubit statement then reduces to the 8-dimensional block facts (where fin_cases is viable and mostly already proven): the inner code's stabiliser fixing and syndromes are ThreeQubit's lemmas applied to the block states B± = |000⟩ ± |111⟩ = logical 1 (±1), and the outer code's action rides two new 8-dim computations (tel_Xall_logical, tel_Zin_logical). Nothing above 8 dimensions is ever proved entry-wise.

The code and its statements

shorLogical a b = a·(B₊⊗B₊⊗B₊) + b·(B₋⊗B₋⊗B₋) (unnormalised coefficients, as in the 3-qubit modules — every statement is linear).

• Codespace: all eight stabilisers fix shorLogical — innerStab_fixes_shorLogical (the six Z_iZ_j pairs, via the bit-flip code's fixing lemmas) and outerStab_fixes_shorLogical (the two X^{⊗6} operators, via B± being ±1-eigenstates of X^{⊗3}).
• Syndromes: ★ innerStab_syndrome_X — a bit flip at inner position j of block s trips block s's stabiliser pair with exactly the 3-qubit sign pattern (xSyndromeSign, injective: xSyndromeSign_injective), while every other-block inner stabiliser (innerStab_fixes_X_other) and both outer stabilisers (outerStab_fixes_X) read +1. ★ outerStab_syndrome_Z — a phase flip anywhere in block s trips the outer pair with the block pattern (zSyndromeSign, injective: zSyndromeSign_injective), independent of which qubit inside was hit, while every inner stabiliser reads +1 (innerStab_fixes_Z). X errors trip only inner stabilisers and Z errors only outer ones, so the classes are separated by construction.
• Corrections (★★ the headline set): for every block s : Fin 3 and inner position j : Fin 3,
  • shor_corrects_X — re-applying the identified bit flip restores the state;
  • shor_corrects_Z_degenerate — applying Z to the first qubit of the identified block restores the state whichever qubit inside was hit: the code is degenerate, and the recovery needs only the block-level syndrome;
  • shor_corrects_XZ — the composite error X_j Z_j (Y up to phase) is corrected by composing the two recoveries. With pauli_decomposition (ErrorDiscretization.lean: every 2×2 error is a combination of I, X, Z, XZ), this is the discretised form of "corrects an arbitrary single-qubit error".

Honest scope

Correctable set: single-qubit errors (one position, one block). No claim about two-error patterns, measurement dynamics (the syndrome extraction is the eigenvalue reading, as in the 3-qubit modules — the collapse half at 9 qubits is not restated), or fault tolerance. The syndrome lemmas give the eigenvalue table and the two injectivity facts; the full 28-row distinctness tabulation is their mechanical product and is not separately enumerated.

Cross-references: specs/future-work.md, specs/BACKLOG.md §Q (Q5) and the E1 assessment row; three_qubit_corrects_single_bitflip, syndromePF_Z1 (the phase-flip half), pauli_decomposition, syndrome_collapse (SyndromeCollapse.lean, the 3-qubit collapse half).

Source

Shor 1995; Nielsen–Chuang §10.2 (the 9-qubit code as concatenation).

The 9-qubit space and the block Kronecker combinator

@[reducible, inline]

abbrev CSD.Empirical.QM.QEC.I3 : Type

The inner-block index: one 3-qubit register.

Equations

• CSD.Empirical.QM.QEC.I3 = (Fin 2 × Fin 2 × Fin 2)

@[reducible, inline]

abbrev CSD.Empirical.QM.QEC.H9 : Type

The 9-qubit Hilbert space, blocked as three 3-qubit registers.

Equations

• CSD.Empirical.QM.QEC.H9 = EuclideanSpace ℂ (CSD.Empirical.QM.QEC.I3 × CSD.Empirical.QM.QEC.I3 × CSD.Empirical.QM.QEC.I3)

def CSD.Empirical.QM.QEC.bkron (A B C : Matrix I3 I3 ℂ) : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ

Three-fold block Kronecker product of 8×8 block operators.

Equations

• CSD.Empirical.QM.QEC.bkron A B C = Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B C)

noncomputable def CSD.Empirical.QM.QEC.vkron (u v w : H3) : H9

Three-fold block tensor of block vectors: vkron u v w = u ⊗ v ⊗ w entry-wise on the blocked index.

Equations

• CSD.Empirical.QM.QEC.vkron u v w = ∑ p : CSD.Empirical.QM.QEC.I3 × CSD.Empirical.QM.QEC.I3 × CSD.Empirical.QM.QEC.I3, EuclideanSpace.single p (u.ofLp p.1 * v.ofLp p.2.1 * w.ofLp p.2.2)

@[simp]

theorem CSD.Empirical.QM.QEC.vkron_apply (u v w : H3) (p : I3 × I3 × I3) : (vkron u v w).ofLp p = u.ofLp p.1 * v.ofLp p.2.1 * w.ofLp p.2.2

theorem CSD.Empirical.QM.QEC.bkron_mul (A B C A' B' C' : Matrix I3 I3 ℂ) : bkron A B C * bkron A' B' C' = bkron (A * A') (B * B') (C * C')

Mixed product for block Kroneckers.

@[simp]

theorem CSD.Empirical.QM.QEC.bkron_one : bkron 1 1 1 = 1

theorem CSD.Empirical.QM.QEC.bkron_neg_left (A B C : Matrix I3 I3 ℂ) : bkron (-A) B C = -bkron A B C

theorem CSD.Empirical.QM.QEC.bkron_neg_mid (A B C : Matrix I3 I3 ℂ) : bkron A (-B) C = -bkron A B C

theorem CSD.Empirical.QM.QEC.bkron_neg_right (A B C : Matrix I3 I3 ℂ) : bkron A B (-C) = -bkron A B C

@[reducible, inline]

noncomputable abbrev CSD.Empirical.QM.QEC.tel9 (M : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ) (ψ : H9) : H9

Abbreviation for the 9-qubit matrix action.

Equations

• CSD.Empirical.QM.QEC.tel9 M ψ = (Matrix.toEuclideanLin M) ψ

theorem CSD.Empirical.QM.QEC.tel9_mul (M N : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ) (ψ : H9) : tel9 (M * N) ψ = tel9 M (tel9 N ψ)

theorem CSD.Empirical.QM.QEC.tel9_smul (c : ℂ) (M : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ) (ψ : H9) : tel9 (c • M) ψ = c • tel9 M ψ

theorem CSD.Empirical.QM.QEC.tel9_one (ψ : H9) : tel9 1 ψ = ψ

theorem CSD.Empirical.QM.QEC.kron_mulVec {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) (f : ι → ℂ) (g : κ → ℂ) : ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A B).mulVec fun (q : ι × κ) => f q.1 * g q.2) = fun (q : ι × κ) => A.mulVec f q.1 * B.mulVec g q.2

The generic two-factor combinator: a Kronecker product acts on a product vector factor-wise (function level, arbitrary finite index types).

theorem CSD.Empirical.QM.QEC.kron3_mulVec {ι : Type u_1} {κ : Type u_2} {ν : Type u_3} [Fintype ι] [Fintype κ] [Fintype ν] (A : Matrix ι ι ℂ) (B : Matrix κ κ ℂ) (C : Matrix ν ν ℂ) (f : ι → ℂ) (g : κ → ℂ) (h : ν → ℂ) : ((Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) A (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) B C)).mulVec fun (q : ι × κ × ν) => f q.1 * (g q.2.1 * h q.2.2)) = fun (q : ι × κ × ν) => A.mulVec f q.1 * (B.mulVec g q.2.1 * C.mulVec h q.2.2)

The three-factor version, by iterating kron_mulVec.

theorem CSD.Empirical.QM.QEC.tel9_bkron_vkron (A B C : Matrix I3 I3 ℂ) (u v w : H3) : tel9 (bkron A B C) (vkron u v w) = vkron ((Matrix.toEuclideanLin A) u) ((Matrix.toEuclideanLin B) v) ((Matrix.toEuclideanLin C) w)

★ The combinator: the block Kronecker action factorises through the block tensor — (A ⊗ B ⊗ C)(u ⊗ v ⊗ w) = (Au) ⊗ (Bv) ⊗ (Cw). The one lemma that reduces every 512-dimensional statement to 8-dimensional block facts.

theorem CSD.Empirical.QM.QEC.vkron_neg_left (u v w : H3) : vkron (-u) v w = -vkron u v w

theorem CSD.Empirical.QM.QEC.vkron_neg_mid (u v w : H3) : vkron u (-v) w = -vkron u v w

theorem CSD.Empirical.QM.QEC.vkron_neg_right (u v w : H3) : vkron u v (-w) = -vkron u v w

The block-level facts (8-dimensional, fin_cases-viable)

noncomputable def CSD.Empirical.QM.QEC.Bp : H3

The block states B± = |000⟩ ± |111⟩: the bit-flip code's encodings of |±⟩. Bp = logical 1 1.

Equations

• CSD.Empirical.QM.QEC.Bp = CSD.Empirical.QM.QEC.logical 1 1

noncomputable def CSD.Empirical.QM.QEC.Bm : H3

Bm = logical 1 (−1).

Equations

• CSD.Empirical.QM.QEC.Bm = CSD.Empirical.QM.QEC.logical 1 (-1)

def CSD.Empirical.QM.QEC.Xall : Matrix I3 I3 ℂ

The all-block bit flip X^{⊗3} = X₁X₂X₃ — the outer code's stabiliser factor on one block.

Equations

• CSD.Empirical.QM.QEC.Xall = CSD.Empirical.QM.QEC.kron3 CSD.Empirical.QM.QEC.pX CSD.Empirical.QM.QEC.pX CSD.Empirical.QM.QEC.pX

@[simp]

theorem CSD.Empirical.QM.QEC.Xall_mul_Xall : Xall * Xall = 1

theorem CSD.Empirical.QM.QEC.tel_Xall_logical (a b : ℂ) : (Matrix.toEuclideanLin Xall) (logical a b) = logical b a

X^{⊗3} swaps |000⟩ ↔ |111⟩: on the logical block it exchanges the coefficients.

theorem CSD.Empirical.QM.QEC.tel_Xall_Bp : (Matrix.toEuclideanLin Xall) Bp = Bp

B₊ is a +1 eigenstate of X^{⊗3}.

theorem CSD.Empirical.QM.QEC.tel_Xall_Bm : (Matrix.toEuclideanLin Xall) Bm = -Bm

B₋ is a −1 eigenstate of X^{⊗3}.

def CSD.Empirical.QM.QEC.Zin : Fin 3 → Matrix I3 I3 ℂ

The inner-position phase flips (PhaseFlip.lean's Z₁, Z₂, Z₃), as a Fin 3-indexed family.

Equations

• CSD.Empirical.QM.QEC.Zin 0 = CSD.Empirical.QM.QEC.Z1
• CSD.Empirical.QM.QEC.Zin 1 = CSD.Empirical.QM.QEC.Z2
• CSD.Empirical.QM.QEC.Zin 2 = CSD.Empirical.QM.QEC.Z3

def CSD.Empirical.QM.QEC.Xin : Fin 3 → Matrix I3 I3 ℂ

The inner-position bit flips (ThreeQubit.lean's X₁, X₂, X₃), as a Fin 3-indexed family.

Equations

• CSD.Empirical.QM.QEC.Xin 0 = CSD.Empirical.QM.QEC.X1
• CSD.Empirical.QM.QEC.Xin 1 = CSD.Empirical.QM.QEC.X2
• CSD.Empirical.QM.QEC.Xin 2 = CSD.Empirical.QM.QEC.X3

@[simp]

theorem CSD.Empirical.QM.QEC.Xin_mul_self (j : Fin 3) : Xin j * Xin j = 1

theorem CSD.Empirical.QM.QEC.tel_Zin_logical (j : Fin 3) (a b : ℂ) : (Matrix.toEuclideanLin (Zin j)) (logical a b) = logical a (-b)

The block phase-flip action: every single Z inside a block flips the sign of the |111⟩ component — Z_j (a|000⟩ + b|111⟩) = a|000⟩ − b|111⟩, the same action for all three positions j. The germ of the code's degeneracy.

theorem CSD.Empirical.QM.QEC.tel_Z1_Zin_logical (j : Fin 3) (a b : ℂ) : (Matrix.toEuclideanLin Z1) ((Matrix.toEuclideanLin (Zin j)) (logical a b)) = logical a b

Block-level degeneracy: Z₁ Z_j fixes the logical block for every j — the two sign flips cancel, so recovering with Z₁ corrects a Z error at any inner position.

The 9-qubit operators: placement and the code space

def CSD.Empirical.QM.QEC.place : Fin 3 → Matrix I3 I3 ℂ → Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ

Place a block operator in slot s (identity on the other blocks).

Equations

• CSD.Empirical.QM.QEC.place 0 x✝ = CSD.Empirical.QM.QEC.bkron x✝ 1 1
• CSD.Empirical.QM.QEC.place 1 x✝ = CSD.Empirical.QM.QEC.bkron 1 x✝ 1
• CSD.Empirical.QM.QEC.place 2 x✝ = CSD.Empirical.QM.QEC.bkron 1 1 x✝

theorem CSD.Empirical.QM.QEC.place_mul (s : Fin 3) (M N : Matrix I3 I3 ℂ) : place s M * place s N = place s (M * N)

@[simp]

theorem CSD.Empirical.QM.QEC.place_one (s : Fin 3) : place s 1 = 1

theorem CSD.Empirical.QM.QEC.place_smul (s : Fin 3) (c : ℂ) (M : Matrix I3 I3 ℂ) : place s (c • M) = c • place s M

noncomputable def CSD.Empirical.QM.QEC.shorLogical (a b : ℂ) : H9

The Shor logical state a·(B₊ ⊗ B₊ ⊗ B₊) + b·(B₋ ⊗ B₋ ⊗ B₋) (unnormalised coefficients).

Equations

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

def CSD.Empirical.QM.QEC.innerStabBlock : Fin 2 → Matrix I3 I3 ℂ

Block s's stabiliser pair member: Z₁Z₂ (t = 0) or Z₂Z₃ (t = 1).

Equations

• CSD.Empirical.QM.QEC.innerStabBlock 0 = CSD.Empirical.QM.QEC.Z1Z2
• CSD.Empirical.QM.QEC.innerStabBlock 1 = CSD.Empirical.QM.QEC.Z2Z3

def CSD.Empirical.QM.QEC.innerStab (s : Fin 3) (t : Fin 2) : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ

The six inner stabilisers: block s's pair, chosen by t.

Equations

• CSD.Empirical.QM.QEC.innerStab s t = CSD.Empirical.QM.QEC.place s (CSD.Empirical.QM.QEC.innerStabBlock t)

def CSD.Empirical.QM.QEC.outerStab : Fin 2 → Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ

The two outer stabilisers: X^{⊗6} on blocks 1–2 (t = 0) and 2–3 (t = 1).

Equations

• CSD.Empirical.QM.QEC.outerStab 0 = CSD.Empirical.QM.QEC.bkron CSD.Empirical.QM.QEC.Xall CSD.Empirical.QM.QEC.Xall 1
• CSD.Empirical.QM.QEC.outerStab 1 = CSD.Empirical.QM.QEC.bkron 1 CSD.Empirical.QM.QEC.Xall CSD.Empirical.QM.QEC.Xall

def CSD.Empirical.QM.QEC.errX (s j : Fin 3) : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ

The single-qubit bit-flip error at inner position j of block s.

Equations

• CSD.Empirical.QM.QEC.errX s j = CSD.Empirical.QM.QEC.place s (CSD.Empirical.QM.QEC.Xin j)

def CSD.Empirical.QM.QEC.errZ (s j : Fin 3) : Matrix (I3 × I3 × I3) (I3 × I3 × I3) ℂ

The single-qubit phase-flip error at inner position j of block s.

Equations

• CSD.Empirical.QM.QEC.errZ s j = CSD.Empirical.QM.QEC.place s (CSD.Empirical.QM.QEC.Zin j)

The codespace: all eight stabilisers fix the logical state

theorem CSD.Empirical.QM.QEC.innerStab_fixes_shorLogical (s : Fin 3) (t : Fin 2) (a b : ℂ) : tel9 (innerStab s t) (shorLogical a b) = shorLogical a b

The six inner stabilisers fix shorLogical: within each block the bit-flip code's stabilisers fix both B₊ and B₋ (they are logical instances).

theorem CSD.Empirical.QM.QEC.outerStab_fixes_shorLogical (t : Fin 2) (a b : ℂ) : tel9 (outerStab t) (shorLogical a b) = shorLogical a b

The two outer stabilisers fix shorLogical: B₊ is a +1 eigenstate of X^{⊗3} and B₋ a −1 eigenstate, and each outer stabiliser touches exactly two blocks, so the signs cancel.

Syndromes: the eigenvalue table

def CSD.Empirical.QM.QEC.xSyndromeSign : Fin 3 → Fin 2 → ℂ

The bit-flip syndrome signs: position j against the stabiliser pair, exactly the 3-qubit code's table (−,+), (−,−), (+,−).

Equations

• CSD.Empirical.QM.QEC.xSyndromeSign 0 0 = -1
• CSD.Empirical.QM.QEC.xSyndromeSign 0 1 = 1
• CSD.Empirical.QM.QEC.xSyndromeSign 1 0 = -1
• CSD.Empirical.QM.QEC.xSyndromeSign 1 1 = -1
• CSD.Empirical.QM.QEC.xSyndromeSign 2 0 = 1
• CSD.Empirical.QM.QEC.xSyndromeSign 2 1 = -1

def CSD.Empirical.QM.QEC.zSyndromeSign : Fin 3 → Fin 2 → ℂ

The phase-flip block-syndrome signs: block s against the outer pair — the same mirror table (−,+), (−,−), (+,−), now reading the block.

Equations

• CSD.Empirical.QM.QEC.zSyndromeSign = CSD.Empirical.QM.QEC.xSyndromeSign

theorem CSD.Empirical.QM.QEC.xSyndromeSign_injective : Function.Injective xSyndromeSign

The bit-flip syndrome pattern is injective: the pair of inner readings identifies the position within the block. (The 3-qubit three_qubit_syndromes_distinct, at the level of the sign table.)

theorem CSD.Empirical.QM.QEC.zSyndromeSign_injective : Function.Injective zSyndromeSign

The phase-flip block-syndrome pattern is injective: the pair of outer readings identifies the block.

theorem CSD.Empirical.QM.QEC.innerStab_syndrome_X (s j : Fin 3) (t : Fin 2) (a b : ℂ) : tel9 (innerStab s t) (tel9 (errX s j) (shorLogical a b)) = xSyndromeSign j t • tel9 (errX s j) (shorLogical a b)

★ Bit-flip syndrome, same block: an X error at position j of block s makes the errored state an eigenstate of block s's stabiliser pair with the 3-qubit sign pattern xSyndromeSign j.

theorem CSD.Empirical.QM.QEC.innerStab_fixes_X_other {s s' : Fin 3} (hss : s' ≠ s) (j : Fin 3) (t : Fin 2) (a b : ℂ) : tel9 (innerStab s' t) (tel9 (errX s j) (shorLogical a b)) = tel9 (errX s j) (shorLogical a b)

Bit flips are invisible to the other blocks' stabilisers: the inner pair of any block s' ≠ s still reads +1.

theorem CSD.Empirical.QM.QEC.outerStab_fixes_X (s j : Fin 3) (t : Fin 2) (a b : ℂ) : tel9 (outerStab t) (tel9 (errX s j) (shorLogical a b)) = tel9 (errX s j) (shorLogical a b)

Bit flips are invisible to the outer stabilisers: X commutes with X^{⊗6}, so both outer readings stay +1.

theorem CSD.Empirical.QM.QEC.Xall_anticomm_Zin (j : Fin 3) : Xall * Zin j = -(Zin j * Xall)

The block-level anticommutation behind the phase-flip syndrome: X^{⊗3} anticommutes with every single Z in the block.

theorem CSD.Empirical.QM.QEC.outerStab_syndrome_Z (s j : Fin 3) (t : Fin 2) (a b : ℂ) : tel9 (outerStab t) (tel9 (errZ s j) (shorLogical a b)) = zSyndromeSign s t • tel9 (errZ s j) (shorLogical a b)

★ Phase-flip syndrome, degenerate: a Z error at any inner position j of block s makes the errored state an eigenstate of the outer pair with the block pattern zSyndromeSign s — the reading depends only on the block, never on j.

theorem CSD.Empirical.QM.QEC.innerStab_fixes_Z (s' s j : Fin 3) (t : Fin 2) (a b : ℂ) : tel9 (innerStab s' t) (tel9 (errZ s j) (shorLogical a b)) = tel9 (errZ s j) (shorLogical a b)

Phase flips are invisible to every inner stabiliser: Z's commute, so all six inner readings stay +1.

Corrections: the headline theorems

theorem CSD.Empirical.QM.QEC.shor_corrects_X (s j : Fin 3) (a b : ℂ) : tel9 (errX s j) (tel9 (errX s j) (shorLogical a b)) = shorLogical a b

★★ Bit-flip correction at every position: re-applying the syndrome-identified X restores the Shor logical state exactly.

theorem CSD.Empirical.QM.QEC.tel9_place_Z1_Zin (s j : Fin 3) (a b : ℂ) : tel9 (place s (Z1 * Zin j)) (shorLogical a b) = shorLogical a b

The recovery core: Z₁·Z_j placed in any slot fixes the logical state — the block degeneracy, lifted.

theorem CSD.Empirical.QM.QEC.shor_corrects_Z_degenerate (s j : Fin 3) (a b : ℂ) : tel9 (place s Z1) (tel9 (errZ s j) (shorLogical a b)) = shorLogical a b

★★ Degenerate phase-flip correction: applying Z to the first qubit of the syndrome-identified block restores the state whichever inner qubit was hit — the outer syndrome cannot see j, and thanks to the code's degeneracy the recovery does not need to.

theorem CSD.Empirical.QM.QEC.shor_corrects_XZ (s j : Fin 3) (a b : ℂ) : tel9 (place s Z1) (tel9 (errX s j) (tel9 (errX s j * errZ s j) (shorLogical a b))) = shorLogical a b

★★ Composite (XZ, i.e. Y up to phase) correction: the two recoveries compose — apply the identified X, then the block's Z₁. With pauli_decomposition this completes the discretised single-error set {I, X, Z, XZ} at every one of the nine positions.