Informal spec: [[6,2,2]] C_6 code

Summary

The Knill C_6 code is a six-qubit normal self-dual CSS stabilizer code encoding two logical qubits with code distance 2. It detects (but does not correct) a single arbitrary Pauli error and, in Knill's qubit-pair grouping, detects any error acting on one of the three pairs (allowing pair-error correction when the location is already known). The code was introduced in E. Knill, Quantum computing with realistically noisy devices (Nature 434, 39 (2005); preprint arxiv:quant-ph/0410199), where it is used at the second and higher concatenation levels of Knill's C_4/C_6 fault-tolerant architecture (with [[4,2,2]] at the inner level).

This file formalizes the standard distance-2 stabilizer-detection structure of C_6 using the EC Zoo's canonical stabilizer presentation (Qiskit preset ID 126) and logical-operator choice (Knill 2004).

Parameters

• Physical qubits: n = 6
• Logical qubits: k = 2
• Distance: d = 2
• Family: CSS (2 Z-type stabilizers, 2 X-type stabilizers)
• Originally introduced in: E. Knill 2004/2005 [arxiv:quant-ph/0410199 §-, fault-tolerance application]
• EC Zoo entry: stab_6_2_2 ("[[6,2,2]] C_6 code")
• Geometric description (EC Zoo): color code on a triangular-prism ladder with three rungs and periodic boundary conditions; Z- and X-type stabilizers lie on the three square faces.

Equivalence notes (informational; NOT formalized here)

The EC Zoo entry lists C_6 as a special case of several other codes:

1. Ganti-Onunkwo-Young (GOY) code at r = 1: "The Ganti-Onunkwo-Young code for r = 1 is the C_6 code." GOY's natural family presentation has 2 weight-2 + 2 weight-4 generators at r = 1, which differs from the uniform-weight-4 Knill presentation formalized here. The codes are mathematically equivalent (same stabilizer subgroup / same codespace) under generator-set replacement. Future GOY parametric formalization will need a bridge lemma.

2. [[k+4, k, 2]] "H code" at k = 2: "The [[k+4,k,2]] H code for k = 2 is the C_6 code." Same caveat — equivalent code, different parametric presentation.

3. Khesin-Lu-Shor code at r = 2, m = 2^r - 1 = 3: equivalence detail per EC Zoo.

4. stab_4_2_2 cousin: the [[4,2,2]] code (FourQubit_4_2_2.lean) is the inner code in Knill's C_4/C_6 concatenation; C_6 is the outer code. Same (n, k, d) = (?, 2, 2) parameters as [[4,2,2]] is to [[6,2,2]] — both are k = 2 CSS detection codes, structurally the closest existing formalization template.

We formalize only the Knill C_6 presentation (the EC Zoo entry's canonical stabilizer + logicals).

Stabilizer generators

Four independent generators (n − k = 4), in canonical Z-then-X order. The stabilizer tableau is from EC Zoo (citing Qiskit preset ID 126):

(All four generators have uniform weight 4. This is the normal self-dual structure: the X-side check matrix equals the Z-side check matrix.)

Geometric interpretation (per EC Zoo parents:2d_color): Each stabilizer corresponds to a square face of a triangular prism with three rungs and periodic boundary conditions. Qubits {0,1} are the "top" pair, {2,3} the "second" pair, {4,5} the "third" pair. S_Z1/S_X1 cover the first two pairs; S_Z2/S_X2 cover the first and third pairs. (The implicit third face would be the {2,3,4,5} support, which is the product S_Z1 · S_Z2 modulo X-side, so it is dependent — only 4 independent generators total.)

Pairwise overlap structure (matters for the §4 cross-commutation proof):

All four ZX cross-pairs commute (even overlap counts). The two ZZ pairs trivially commute (both Z-type). The two XX pairs trivially commute (both X-type). So all six pairs are confirmed abelian.

Logical operators

(Two logical qubits ⇒ two pairs (X̄_L, Z̄_L) and (X̄_S, Z̄_S), following Knill's L/S labelling.)

From [arxiv:quant-ph/0410199] via EC Zoo:

Naming convention: we name them logicalX_1, logicalZ_1, logicalX_2, logicalZ_2 in the Lean file (matching FourQubit_4_2_2.lean's naming convention for k = 2 codes), where _1 corresponds to Knill's "L" pair and _2 corresponds to his "S" pair.

Verification of (anti)commutation with stabilizers: every logical must commute with every stabilizer (4 stabilizers × 4 logicals = 16 checks).

All 16 stabilizer-vs-logical checks commute. ✓

Verification of pairwise logical (anti)commutation: 6 checks (4 logicals choose 2).

All pairwise checks correct. ✓

Verification of nontriviality (each logical is not in the stabilizer subgroup):

• The X-side stabilizer subgroup is ⟨S_X1, S_X2⟩ = {I, S_X1, S_X2, S_X1·S_X2}. The four possible X-type elements have supports {} (I), {0,1,2,3} (S_X1), {0,1,4,5} (S_X2), {2,3,4,5} (S_X1·S_X2 = II XX XX). None of these equal X_L = IIXXII (support {2,3}) or X_S = IXIXXI (support {1,3,4}, with mixed weight-3 — clearly not a product of two weight-4 X-stabs). ✓

• The Z-side analog: Z_L = ZIIZZI (support {0,3,4}, weight 3) and Z_S = IIIIZZ (support {4,5}, weight 2) — neither equals any element of ⟨S_Z1, S_Z2⟩ = {I, ZZZZ II, ZZ II ZZ, II ZZ ZZ}. ✓

Codespace

The codespace is 2^k = 4-dimensional. The stabilizer projector is

P_C = (1/16)(I + S_Z1)(I + S_Z2)(I + S_X1)(I + S_X2)

which projects onto this 4-d subspace. We do not formalize P_C explicitly in this skeleton — it follows from the abstract Codespace framework once the StabilizerGroup 6 is in hand.

Theorems to formalize

The skeleton mirrors FourQubit_4_2_2.lean (the structurally closest existing CSS k = 2 detection code) and CSS_4_1_2.lean (for the multi-Z-stabilizer cross-commutation and weight-1 anti-witness patterns).

The numbered theorems below are the TODO(stab_6_2_2-T<n>) markers in the Lean skeleton.

T1: each Z-generator is Z-type (operators in {I, Z})

Statement. ∀ g ∈ ZGenerators, IsZTypeElement g. Reference: standard CSS predicate from Framework/Core/CSS/CSSPredicates.lean. Two generators (S_Z1, S_Z2) to check.

T2: each X-generator is X-type (operators in {I, X})

Statement. ∀ g ∈ XGenerators, IsXTypeElement g. Two generators (S_X1, S_X2).

T3: S_Z1 * S_X1 = S_X1 * S_Z1 (ZZZZ II and XXXX II commute)

Statement. S_Z1 * S_X1 = S_X1 * S_Z1. Justification. Anticommute at all four overlap qubits {0,1,2,3}; count 4 (even) ⇒ commute. Standard CSS argument.

T4: S_Z1 * S_X2 = S_X2 * S_Z1 (ZZZZ II and XX II XX commute)

Statement. S_Z1 * S_X2 = S_X2 * S_Z1. Justification. Anticommute at qubits {0,1}; count 2 (even) ⇒ commute.

T5: S_Z2 * S_X1 = S_X1 * S_Z2 (ZZ II ZZ and XXXX II commute)

Statement. S_Z2 * S_X1 = S_X1 * S_Z2. Justification. Anticommute at qubits {0,1}; count 2 (even) ⇒ commute.

T6: S_Z2 * S_X2 = S_X2 * S_Z2 (ZZ II ZZ and XX II XX commute)

Statement. S_Z2 * S_X2 = S_X2 * S_Z2. Justification. Anticommute at qubits {0,1,4,5}; count 4 (even) ⇒ commute.

T7: ZGenerators_commute_XGenerators

Statement. ∀ z ∈ ZGenerators, ∀ x ∈ XGenerators, z * x = x * z. Combines T3–T6 by rcases.

T8: all-pair generator commutation

Statement. ∀ g h ∈ generators, g * h = h * g. Combines T1, T2, T7 via the CSS-type-commutation lemmas from CSSCommutationLemmas.lean.

T9: negIdentity 6 ∉ subgroup

Statement. negIdentity 6 ∉ Subgroup.closure generators. Justification. One-line consequence of T1, T2, T7 via CSS.negIdentity_not_mem_closure_union.

T10: listToSet generatorsList = generators

Statement. NQubitPauliGroupElement.listToSet [S_Z1, S_Z2, S_X1, S_X2] = generators. Four elements in the list, four in the set (split as 2-Z + 2-X union).

T11: AllPhaseZero generatorsList

Statement. NQubitPauliGroupElement.AllPhaseZero [S_Z1, S_Z2, S_X1, S_X2]. Justification. All generators are constructed with phasePower = 0.

T12: rows of the symplectic check matrix are linearly independent

Statement. rowsLinearIndependent [S_Z1, S_Z2, S_X1, S_X2]. Justification. Closes by decide on the 4-row, 12-column (over GF(2)) check matrix.

T13: generators independent

Statement. GeneratorsIndependent 6 generatorsList. Justification. One-line consequence of T12 via GeneratorsIndependent_of_rowsLinearIndependent.

T14: stabilizerGroup.toSubgroup = subgroup

Statement. The bundled StabilizerGroup 6 from mkStabilizerFromGenerators has the expected underlying subgroup.

T15: Anticommute logicalX_1 logicalZ_1 (i.e. X_L = IIXXII vs Z_L = ZIIZZI)

Statement. NQubitPauliGroupElement.Anticommute logicalX_1 logicalZ_1. Justification. Overlap = {3}; anticommute-count 1 (odd) ⇒ anticommute. [Knill 2004 via EC Zoo Logical operators section.]

T16: Anticommute logicalX_2 logicalZ_2 (i.e. X_S = IXIXXI vs Z_S = IIIIZZ)

Statement. NQubitPauliGroupElement.Anticommute logicalX_2 logicalZ_2. Justification. Overlap = {4}; anticommute-count 1 (odd) ⇒ anticommute.

T17: logicalX_1 * logicalX_2 = logicalX_2 * logicalX_1 (X_L and X_S commute)

Statement. Standard equation form. Justification. Both X-type ⇒ trivially commute (componentwise X·X = X·X).

T18: logicalX_1 * logicalZ_2 = logicalZ_2 * logicalX_1 (X_L and Z_S commute)

Statement. Standard equation form. Justification. Overlap = {} (X_L on {2,3}, Z_S on {4,5}); 0 anticommute (even).

T19: logicalX_2 * logicalZ_1 = logicalZ_1 * logicalX_2 (X_S and Z_L commute)

Statement. Standard equation form. Justification. Overlap = {3,4} (X_S on {1,3,4}, Z_L on {0,3,4}); 2 anticommute (even).

T20: logicalZ_1 * logicalZ_2 = logicalZ_2 * logicalZ_1 (Z_L and Z_S commute)

Statement. Standard equation form. Justification. Both Z-type ⇒ trivially commute.

T21: logicalX_1 commutes with each generator

Four per-generator lemmas:

• vs S_Z1=ZZZZ II: overlap {2,3}; count 2 (even) ✓
• vs S_Z2=ZZ II ZZ: overlap {}; count 0 ✓
• vs S_X1=XXXX II: both X-type ✓
• vs S_X2=XX II XX: both X-type ✓

T22: logicalX_2 commutes with each generator

Four per-generator lemmas:

• vs S_Z1=ZZZZ II: overlap {1,3}; count 2 (even) ✓
• vs S_Z2=ZZ II ZZ: overlap {1,4}; count 2 (even) ✓
• vs S_X1, S_X2: both X-type ✓

T23: logicalZ_1 commutes with each generator

Four per-generator lemmas:

• vs S_Z1, S_Z2: both Z-type ✓
• vs S_X1=XXXX II: overlap {0,3}; count 2 (even) ✓
• vs S_X2=XX II XX: overlap {0,4}; count 2 (even) ✓

T24: logicalZ_2 commutes with each generator

Four per-generator lemmas:

• vs S_Z1, S_Z2: both Z-type ✓
• vs S_X1=XXXX II: overlap {}; count 0 ✓
• vs S_X2=XX II XX: overlap {4,5}; count 2 (even) ✓

T25: logicalX_1 ∈ centralizer stabilizerGroup

Builds on T21 via standard Subgroup.forall_comm_closure_iff pattern.

T26: logicalX_2 ∈ centralizer stabilizerGroup

Builds on T22.

T27: logicalZ_1 ∈ centralizer stabilizerGroup

Builds on T23.

T28: logicalZ_2 ∈ centralizer stabilizerGroup

Builds on T24.

T29: StabilizerCode 6 2 packaging

Statement. Construct stabilizerCode : StabilizerCode 6 2 with the fields populated from T8, T10, T11, T13, T15, T16, T25–T28. The logical_commute_cross field requires fin_cases ℓ <;> fin_cases ℓ' (4 cases) and consumes T17–T20 to fill the off-diagonal commutation quadruple.

T30: stabilizerCode.toStabilizerGroup.toSubgroup = closure generators

Statement. Bridge between the StabilizerCode-derived subgroup and the closure generators form. Needed for the distance proof.

T31: weight-1 anticommute witness

Statement. ∀ i : Fin 6, ∀ P ≠ I, ∃ g ∈ generators, Anticommute (weightOneAt i P) g.

Strategy. Dispatch on P (X, Y, Z) and (for X, Y) on which Z-stab covers qubit i. Support structure (key for the dichotomy):

• Qubits {0,1}: BOTH S_Z1 and S_Z2 cover (overlap). EITHER stab works for P ∈ {X,Y}.
• Qubits {2,3}: ONLY S_Z1 covers. Use S_Z1 for P ∈ {X,Y}.
• Qubits {4,5}: ONLY S_Z2 covers. Use S_Z2 for P ∈ {X,Y}.

For P = Z, the dual support structure on the X-stabs is identical (same partition), so we can use either S_X1 (covers {0,1,2,3}) or S_X2 (covers {0,1,4,5}):

• Qubits {0,1}: BOTH work; pick S_X1.
• Qubits {2,3}: ONLY S_X1 works.
• Qubits {4,5}: ONLY S_X2 works.

The cleanest dispatch is therefore a three-way partition of qubits {0,1} / {2,3} / {4,5} for both P = X/Y and P = Z. Conceptually similar to CSS_4_1_2.lean's hi_dichotomy : (i ∈ {0,1}) ∨ (i ∈ {2,3}) but with three branches instead of two. See gap_audit.md for further discussion.

T32: HasCodeDistance stabilizerCode 2

Statement. Uses hasCodeDistance_two_of_anticommute_witness (PR #34, Framework/Core/CSS/CSSDistance.lean) with witness function T31 and an explicit weight-2 nontrivial logical (logicalX_1 = IIXXII, weight 2; or logicalZ_2 = IIIIZZ, weight 2).

T33: StabilizerCodeWithDistance 6 2 2 packaging

One-line bundle of T29 + T32.

Edge cases / convention notes

1. Qubit indexing is 0-based throughout, matching the rest of the repo. EC Zoo's tableau text uses qubit-leftmost convention (qubit 0 on the left), as do we.

2. Logical pair labelling. Knill labels the two logical pairs "L" and "S" (presumably "long" and "short" referring to support weight). We index them as _1 (= Knill's "L", (X_L, Z_L) = (IIXXII, ZIIZZI)) and _2 (= Knill's "S", (X_S, Z_S) = (IXIXXI, IIIIZZ)). This matches the indexing convention of FourQubit_4_2_2.lean.

3. Phase conventions. All four stabilizers and all four logicals have phasePower = 0 (no i or −1 factor). This matches Knill 2004's convention; the EC Zoo tableau implicitly assumes this.

4. Generator weight is uniform = 4. Unlike GOY (parametric family, 2 weight-2 + 2 weight-4 at r = 1), Knill's C_6 presentation uses all-weight-4 generators. This makes the CSS structure especially clean for formalization.

5. Distance is exactly 2 (not greater). The witness for d ≤ 2 is either logicalX_1 = IIXXII (weight 2) or logicalZ_2 = IIIIZZ (weight 2). The lower bound d ≥ 2 reduces to "no weight-1 logical", which is the T31 witness function.

6. Non-overlap subtlety for weight-1 witness (T31). Both Z-stabs together cover all qubits, BUT each individual Z-stab covers only 4 of 6 qubits. So the witness function needs a per-qubit dispatch ("which Z-stab covers qubit i?"). Crucially, S_Z1 and S_Z2 overlap at qubits {0,1} (both contain Z there). The qubits where they disagree are {2,3} (only S_Z1) and {4,5} (only S_Z2). See gap_audit.md for the dichotomy structure.

Citations

• Primary: E. Knill, Quantum computing with realistically noisy devices, Nature 434, 39 (2005); arxiv:quant-ph/0410199.
• Stabilizer tableau source: EC Zoo stab_6_2_2 entry citing Qiskit preset ID 126.
• Logical operator source: EC Zoo stab_6_2_2 entry citing Knill 2004 (arxiv:quant-ph/0410199).
• Related codes (for equivalence notes, not formalized here): GOY (goy), [[k+4,k,2]] H code (quantum_h), KLS (kls), [[4,2,2]] (stab_4_2_2).

Formalization plan: [[6,2,2]] C_6 code

Strategy summary

The Knill C_6 [[6,2,2]] code is the second k = 2 CSS code to be formalized in the repo (after FourQubit_4_2_2.lean). It is also a multi-Z-stabilizer / multi-X-stabilizer CSS code (like CSS_4_1_2.lean), so the relevant template-blending is:

• From FourQubit_4_2_2.lean (k = 2 CSS structure): all the logical- operator infrastructure (logicalX_1, logicalX_2, logicalZ_1, logicalZ_2), the pairwise off-diagonal commutation theorems (T17–T20), and the logical_commute_cross field's fin_cases ℓ <;> fin_cases ℓ' 4-case dispatch.
• From CSS_4_1_2.lean (multi-Z-stab CSS structure): the hi_dichotomy pattern for the weight-1 anticommute witness, plus the partial-support Z-generators that don't include NQubitPauliOperator.identity fall-through in their simp sets.

The distance proof reuses hasCodeDistance_two_of_anticommute_witness (Framework/Core/CSS/CSSDistance.lean, introduced in PR #34) — the proven, reusable distance-2 closer that abstracts the "witness function + explicit weight-2 logical" boilerplate.

Distance method: finite enumeration via the CSS helper. No homological framework needed; n = 6 is small enough that explicit witness Finsets are tractable.

Key structural difference from FourQubit_4_2_2.lean: in FourQubit_4_2_2.lean, the single Z-stab ZZZZ covers all 4 qubits, so the weight-1 anti-witness function trivially picks Z1 for X/Y errors at any qubit. In C_6, each Z-stab covers only 4 of 6 qubits, so the weight-1 anti-witness needs a qubit-dependent dispatch (see T31 below).

Theorem dependency graph

T1 (Z-gens Z-type)        T2 (X-gens X-type)
   \                       /
T3,T4,T5,T6 (4 ZX cross-commutes) ←──┐
   \                              T7 (combined ZGenerators_commute_XGenerators)
   |                                  /
T8 (gen pairwise commute) ←───── T1, T2, T7
   |
T9 (-I ∉ subgroup) ←────────────  T1, T2, T7

T10 (list ↔ set)
T11 (phase 0)         T12 (rows indep)
                            \
                             T13 (gens indep)
   \    \    /
T14 (stabilizerGroup.toSubgroup = subgroup) ←─ T10

T15 (X̄_1 ⊥ Z̄_1)         T16 (X̄_2 ⊥ Z̄_2)
T17 (X̄_1 comm X̄_2)       T18 (X̄_1 comm Z̄_2)
T19 (X̄_2 comm Z̄_1)       T20 (Z̄_1 comm Z̄_2)

T21 (X̄_1 ⊥ stabs)  T22 (X̄_2 ⊥ stabs)
T23 (Z̄_1 ⊥ stabs)  T24 (Z̄_2 ⊥ stabs)
       \         |        |        /
T25 (X̄_1 ∈ centralizer)
T26 (X̄_2 ∈ centralizer)
T27 (Z̄_1 ∈ centralizer)
T28 (Z̄_2 ∈ centralizer)
       \   \   /    /
T29 (StabilizerCode 6 2) ← needs T8, T9, T10, T11, T13, T15, T16, T25–T28
                          and T17–T20 for the cross-commute field
       |
T30 (stabilizerCode-side subgroup bridge)
       |
T31 (weight-1 anticomm witness)
       \                              /
        T32 (HasCodeDistance 2) ←── needs T29, T30, T31, T15 (or T16) for the logical witness
              |
        T33 (StabilizerCodeWithDistance 6 2 2)

Per-theorem proof sketch

T1: ZGenerators are Z-type

• Approach: rcases hg with rfl | rfl; per generator, fin_cases i <;> simp [PauliOperator.IsZType, S_Z*, NQubitPauliOperator.set, NQubitPauliOperator.identity].
• Reuse: line-for-line analog of CSS_4_1_2.ZGenerators_are_ZType (2 generators).
• Note: BOTH S_Z1 and S_Z2 have partial support (cover only 4 of 6 qubits). Keep NQubitPauliOperator.identity in the simp set for the qubits where the stabilizer's .set chain doesn't reach.
• Difficulty: trivial.

T2: XGenerators are X-type

• Approach: same as T1, with S_X1, S_X2.
• Difficulty: trivial.

T3: S_Z1 * S_X1 = S_X1 * S_Z1 (ZZZZ II vs XXXX II)

• Approach: pauli_comm_even_anticommutes; anticomm-filter Finset is {0, 1, 2, 3} (size 4 = even).
• Reuse: direct analog of FourQubit_4_2_2.Z1_comm_X1 (which uses Finset {0,1,2,3} over Fin 4); here it's {0,1,2,3} over Fin 6.
• Difficulty: trivial.

T4: S_Z1 * S_X2 = S_X2 * S_Z1 (ZZZZ II vs XX II XX)

• Approach: pauli_comm_even_anticommutes; anticomm-filter Finset is {0, 1} (size 2 = even).
• Reuse: analog of CSS_4_1_2.S_Z1_comm_S_X1 (filter {0,1} over Fin 4).
• Difficulty: trivial.

T5: S_Z2 * S_X1 = S_X1 * S_Z2 (ZZ II ZZ vs XXXX II)

• Approach: pauli_comm_even_anticommutes; anticomm-filter Finset is {0, 1} (size 2 = even).
• Difficulty: trivial.

T6: S_Z2 * S_X2 = S_X2 * S_Z2 (ZZ II ZZ vs XX II XX)

• Approach: pauli_comm_even_anticommutes; anticomm-filter Finset is {0, 1, 4, 5} (size 4 = even).
• Difficulty: trivial.

T7: ZGenerators_commute_XGenerators

• Approach: rcases hz with rfl | rfl; rcases hx with rfl | rfl; exact T3/T4/T5/T6 in each branch.
• Reuse: line-for-line analog of CSS_4_1_2.ZGenerators_commute_XGenerators (2 Z gens × 1 X gen), extended to 2 × 2 = 4 cases.
• Difficulty: trivial.

T8: all-pair generator commutation

• Approach: standard CSS structural argument; reuse CSSCommutationLemmas.ZType_commutes and XType_commutes. Case-split on (g, h) ∈ (Z ∪ X) × (Z ∪ X).
• Reuse: copy FourQubit_4_2_2.generators_commute verbatim.
• Difficulty: trivial.

T9: −I ∉ subgroup

• Approach: one-shot via CSS.negIdentity_not_mem_closure_union, fed T1, T2, and the cross-commutation T7.
• Reuse: copy FourQubit_4_2_2.negIdentity_not_mem verbatim.
• Difficulty: trivial.

T10: listToSet generatorsList = generators

• Approach: ext g; simp after unfolding. Four elements in the list, four in the set.
• Reuse: minor adaptation of CSS_4_1_2.listToSet_generatorsList (which has 3 elements, here we extend to 4).
• Difficulty: trivial.

T11: AllPhaseZero generatorsList

• Approach: chain of AllPhaseZero_cons.mpr ⟨rfl, …⟩ per element. Four elements ⇒ four nested ⟨rfl, …⟩.
• Reuse: pattern from CSS_4_1_2.AllPhaseZero_generatorsList.
• Difficulty: trivial.

T12: rows linearly independent

• Approach: by decide. Four rows in (GF(2))^12; concrete and tractable.
• Difficulty: trivial.

T13: generators independent

• Approach: one-line consequence of T12 via GeneratorsIndependent_of_rowsLinearIndependent.
• Difficulty: trivial.

T14: stabilizerGroup.toSubgroup = subgroup

• Approach: unfold mkStabilizerFromGenerators + apply T10.
• Reuse: copy CSS_4_1_2.stabilizerGroup_toSubgroup_eq verbatim.
• Difficulty: trivial.

T15: Anticommute logicalX_1 logicalZ_1 (IIXXII vs ZIIZZI)

• Approach: pauli_anticomm_odd_anticommutes; anticomm-filter Finset is {3} (size 1 = odd). At qubit 3: X·Z (anticomm). At qubits 0 (I·Z), 2 (X·I), 4 (I·Z): commute.
• Reuse: analog of FourQubit_4_2_2.logicalX_1_anticommutes_logicalZ_1.
• Difficulty: trivial.

T16: Anticommute logicalX_2 logicalZ_2 (IXIXXI vs IIIIZZ)

• Approach: pauli_anticomm_odd_anticommutes; anticomm-filter Finset is {4} (size 1 = odd). At qubit 4: X·Z (anticomm). Other positions trivially commute.
• Difficulty: trivial.

T17: logicalX_1 * logicalX_2 = logicalX_2 * logicalX_1

• Approach: both X-type ⇒ trivially commute via pauli_comm_componentwise [logicalX_1, logicalX_2].
• Reuse: copy FourQubit_4_2_2.logicalX_1_commutes_logicalX_2.
• Difficulty: trivial.

T18: logicalX_1 * logicalZ_2 = logicalZ_2 * logicalX_1 (IIXXII vs IIIIZZ)

• Approach: supports disjoint ({2,3} vs {4,5}) ⇒ empty filter ⇒ even count 0. Could use pauli_comm_componentwise (since they have no overlap, the I·X and X·I per-qubit factors trivially commute) OR the explicit empty-Finset filter.
• Decision: use pauli_comm_componentwise (cleaner — no decide on the cardinality).
• Difficulty: trivial.

T19: logicalX_2 * logicalZ_1 = logicalZ_1 * logicalX_2 (IXIXXI vs ZIIZZI)

• Approach: overlap = {3, 4}; anticomm-filter Finset is {3, 4} (size 2 = even). Use pauli_comm_even_anticommutes with explicit filter.
• Reuse: analog of FourQubit_4_2_2.logicalX_1_commutes_logicalZ_2.
• Difficulty: trivial.

T20: logicalZ_1 * logicalZ_2 = logicalZ_2 * logicalZ_1

• Approach: both Z-type ⇒ trivially commute via pauli_comm_componentwise.
• Reuse: copy FourQubit_4_2_2.logicalZ_1_commutes_logicalZ_2.
• Difficulty: trivial.

T21–T24: each logical commutes with each generator (4 logicals × 4 gens = 16 lemmas)

Detailed cases (size of anticomm-filter Finset for the pauli_comm_even_anticommutes cases):

Use pauli_comm_componentwise for both-X-type/both-Z-type and for empty-overlap cases; use pauli_comm_even_anticommutes + explicit filter for the rest.

• Reuse: 8 lemmas use direct analogs of patterns in FourQubit_4_2_2.lean / CSS_4_1_2.lean; 8 lemmas use trivial componentwise dispatch.
• Difficulty: standard mechanical.

T25: logicalX_1 ∈ centralizer stabilizerGroup

• Approach: rw [StabilizerGroup.mem_centralizer_iff, stabilizerGroup_toSubgroup_eq, subgroup]; rw [Subgroup.forall_comm_closure_iff]; intro s hs; then case-split on the union and unfold.
• Reuse: copy FourQubit_4_2_2.logicalX_1_mem_centralizer (4-way case split since we have 2-Z + 2-X here, not 1-Z + 1-X).
• Difficulty: trivial.

T26, T27, T28: same template as T25 for X_2, Z_1, Z_2.

T29: StabilizerCode 6 2 packaging

• Approach: structure literal. The key complication vs. CSS_4_1_2.stabilizerCode (k = 1) is the logical_commute_cross field. For k = 2 it cannot use Subsingleton.elim; instead use fin_cases ℓ <;> fin_cases ℓ' (the 4-case dispatch from FourQubit_4_2_2.stabilizerCode):

  logical_commute_cross := by
    intro ℓ ℓ' hne
    fin_cases ℓ <;> fin_cases ℓ'
    · exact (hne rfl).elim    -- (0, 0)
    · refine ⟨T17, T18, T19.symm, T20⟩    -- (0, 1)
    · refine ⟨T17.symm, T19, T18.symm, T20.symm⟩    -- (1, 0)
    · exact (hne rfl).elim    -- (1, 1)
  

• Reuse: copy FourQubit_4_2_2.stabilizerCode shape (k = 2 case).
• Difficulty: standard.

T30: stabilizer-code subgroup bridge

• Approach: change + rw [listToSet_generatorsList].
• Reuse: copy CSS_4_1_2.stabilizerCode_toSubgroup_eq.
• Difficulty: trivial.

T31: weight-1 anticommute witness

This is the most novel theorem in the file. Strategy:

∀ i : Fin 6, ∀ P : PauliOperator, P ≠ I →
  ∃ g ∈ generators, Anticommute (weightOneAt i P) g

Approach. Three-way hi_trichotomy on qubit i:

have hi_trichotomy : (i = 0 ∨ i = 1) ∨ (i = 2 ∨ i = 3) ∨ (i = 4 ∨ i = 5) := by
  fin_cases i <;> tauto

Then dispatch on P:

• P = X or P = Y: pick Z-stab.
  • (i = 0 ∨ i = 1): either S_Z1 or S_Z2 works; pick S_Z1 for canonicality.
  • (i = 2 ∨ i = 3): only S_Z1 covers, use it.
  • (i = 4 ∨ i = 5): only S_Z2 covers, use it.
• P = Z: pick X-stab — dual analysis (same partition).
  • (i = 0 ∨ i = 1): pick S_X1.
  • (i = 2 ∨ i = 3): only S_X1 covers.
  • (i = 4 ∨ i = 5): only S_X2 covers.

Three helper lemmas (mirroring CSS_4_1_2.lean's 3 helpers):

-- For (i ∈ {0,1,2,3}, P ∈ {X,Y}): weight-1 at i anticommutes with S_Z1.
weightOneAt_anticomm_S_Z1 (i : Fin 6) (P : PauliOperator)
  (hi : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3)
  (hP : P = X ∨ P = Y) : Anticommute (weightOneAt i P) S_Z1

-- For (i ∈ {0,1,4,5}, P ∈ {X,Y}): weight-1 at i anticommutes with S_Z2.
weightOneAt_anticomm_S_Z2 (i : Fin 6) (P : PauliOperator)
  (hi : i = 0 ∨ i = 1 ∨ i = 4 ∨ i = 5)
  (hP : P = X ∨ P = Y) : Anticommute (weightOneAt i P) S_Z2

-- For (i ∈ {0,1,2,3}, P = Z): weight-1 Z at i anticommutes with S_X1.
weightOneAt_Z_anticomm_S_X1 (i : Fin 6) (hi : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3)
  : Anticommute (weightOneAt i Z) S_X1

Plus one more for S_X2 (qubits {0,1,4,5}, P = Z).

The proof shape for each helper is line-by-line analogous to CSS_4_1_2.weightOneAt_anticomm_S_Z1, just with Fin 6 instead of Fin 4 and a 4-way rcases hi instead of 2-way.

• Difficulty: standard; this is the longest single proof in the file. ~30 LoC.

T32: HasCodeDistance stabilizerCode 2

• Approach: one-line via hasCodeDistance_two_of_anticommute_witness.
• Reuse: copy CSS_4_1_2.code_has_distance_two line 487, switching in T31 as the witness and logicalX_1 (or logicalZ_2) as the weight-2 nontrivial logical.
• Difficulty: trivial.

T33: StabilizerCodeWithDistance 6 2 2

• Approach: one-line structure literal bundling T29 + T32.
• Difficulty: trivial.

Risk register

1. Three-way partition vs. two-way hi_dichotomy. CSS_4_1_2.lean used a clean 2-way dichotomy (qubits {0,1} vs {2,3}). C_6 has a three-way partition ({0,1} | {2,3} | {4,5}), but the {0,1} subset is ambiguous (covered by both Z-stabs). The plan resolves the ambiguity by picking S_Z1 for {0,1}, and the helper lemmas are scoped to the correct subset. Mitigation: factor the four-disjunction hypotheses (e.g. i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 for S_Z1) into the helpers' preconditions to keep the dispatch readable.

2. Larger fin_cases i <;> fin_cases j in helper lemmas. For Fin 6 × Fin 6 in the ext j step of each helper, the inner fin_cases j runs over 6 values, the outer over 4 (for the per-stab support). 24 cases per rcases hP branch × 2 P-branches = 48 cases. Should still close in seconds with simp [...]. Risk: if simp is slow, fall back to omega or decide after ext. No real risk; FiveQubit_5_1_3.lean deals with similar combinatorics for n = 5.

3. pauli_comm_componentwise performance with mixed weight-3 + weight-3 logicals. X_S = IXIXXI and Z_L = ZIIZZI both have weight 3 (not weight 2 like [[4,2,2]]'s logicals). The component-wise check at all 6 qubits with mixed I/X/Z entries should still close fast, but watch for lake build timeouts if simp chains explode. Mitigation: use pauli_comm_even_anticommutes + explicit {i, j} filter as a fallback.

4. EC Zoo vs. Knill paper for logical operators. The EC Zoo entry cites Knill 2004 for the logical operators, but the exact form X_L=IIXXII, Z_L=ZIIZZI, X_S=IXIXXI, Z_S=IIIIZZ is from the EC Zoo entry, not the paper text itself. We verified all 16 stabilizer-vs- logical commutations + 6 pairwise logical commutations in informal_spec.md. If a reviewer disputes, the verification table is right there and reproducible. Mitigation in place.

5. linter.unusedSimpArgs from NQubitPauliOperator.identity in X-generator simp sets. Per docs/lean-patterns.md § "identity in simp sets for CSS generator equality", X-generators of C_6 cover only 4 of 6 qubits, so identity IS needed in the simp set (qubits {4,5} for S_X1, qubits {2,3} for S_X2 fall through to identity). Action: keep NQubitPauliOperator.identity in the simp set for T1 and T2 (in C_6 the X-side is partial-support unlike the [[4,2,2]] case).

6. logical_commute_cross quadruple ordering. Each off-diagonal case requires four equations in a specific order:

   X_ℓ * X_ℓ' = X_ℓ' * X_ℓ ∧
   X_ℓ * Z_ℓ' = Z_ℓ' * X_ℓ ∧
   Z_ℓ * X_ℓ' = X_ℓ' * Z_ℓ ∧
   Z_ℓ * Z_ℓ' = Z_ℓ' * Z_ℓ
   

   For (ℓ, ℓ') = (0, 1): takes T17, T18, T19.symm, T20. For (ℓ, ℓ') = (1, 0): takes T17.symm, T19, T18.symm, T20.symm. Mitigation: copy FourQubit_4_2_2.lean:457-467 verbatim — it already has the right symmetry pattern worked out for k = 2.

Estimated effort

• Lines of code: ~500 (catalog estimate was 300; the multi-Z-stab + multi-X-stab combinatorics push the helper count to ~16 logicals×stab commutation lemmas + 4 helper lemmas for T31, so 500 is more realistic. CSS_4_1_2 ended up at 505 LoC with 3 generators × 1 logical-X + 1 logical-Z, so C_6 with 4 generators × 2 logical-X + 2 logical-Z scales linearly to ~550 LoC, but some lemmas are shared between logicals so 500 is a reasonable midpoint).
• Hours: ~3 for an experienced agent following the FourQubit_4_2_2.lean + CSS_4_1_2.lean blended template. No novel proof patterns required.
• Longest theorem: T31 (weight-1 anticommute witness, ~30 LoC with helpers). Should close in one attempt if helpers are written correctly.
• Total sorry count to close: 33 (one per theorem).

Why this is well-suited to engineering track

• No new framework needed. All required infrastructure is in place: hasCodeDistance_two_of_anticommute_witness (PR #34), CSS predicates, IsXTypeElement, IsZTypeElement, the cross-commutation lemmas, the LogicalQubitOps k = 2 packaging.
• Two strong templates. FourQubit_4_2_2.lean (k = 2 structure) + CSS_4_1_2.lean (multi-Z-stab structure). Blend the two.
• Small n. All decide / fin_cases proofs close in seconds.
• Concrete, well-cited code. Knill 2004 is heavily cited and the EC Zoo entry is precise. No spec ambiguity.
• Useful regression test. First k = 2 multi-Z-stab CSS code; if the proof pattern works here, it generalizes cleanly to GOY (parametric) and other [[k+4, k, 2]] H-code instances.

Reuse audit: [[6,2,2]] C_6 code

This file maps every needed primitive in SixQubit_6_2_2.lean to its existing home in the repo, so Stage 4 can copy proof patterns rather than reinvent them.

Directly applicable (use as-is)

Core stabilizer infrastructure

• NQubitPauliGroupElement 6 — physical Pauli group on 6 qubits. [QEC/Stabilizer/Foundations/PauliGroup/NQubitElement.lean]
• NQubitPauliOperator.identity, NQubitPauliOperator.set — the .identity chain + .set i P for generator construction. [QEC/Stabilizer/Foundations/PauliGroup/NQubitOperator.lean]
• PauliOperator.X, Y, Z, I, .IsZType, .IsXType, .mulOp — single-qubit Pauli enum + predicates + multiplication table. [QEC/Stabilizer/Foundations/PauliGroupSingle.lean]
• StabilizerGroup n (structure) — the abstract stabilizer-group bundle. [QEC/Stabilizer/Framework/Core/Stabilizer/StabilizerGroup.lean]
• mkStabilizerFromGenerators — smart constructor for StabilizerGroup from a generator list. [same file]
• Subgroup.closure (Mathlib) — used directly in the subgroup definition. Standard mathlib API.
• Subgroup.forall_comm_closure_iff (Mathlib) — used in the centralizer-membership proofs. Standard mathlib API.

CSS-side machinery

• NQubitPauliGroupElement.IsZTypeElement, IsXTypeElement — the CSS type predicates. [QEC/Stabilizer/Framework/Core/CSS/CSSPredicates.lean]
• CSSCommutationLemmas.ZType_commutes, XType_commutes — Z-type and X-type elements pairwise commute (trivial CSS fact). [QEC/Stabilizer/Framework/Core/CSS/CSSCommutationLemmas.lean]
• CSS.negIdentity_not_mem_closure_union — proves −I ∉ subgroup from Z-type, X-type, and cross-commutation data. [QEC/Stabilizer/Framework/Core/CSS/CSSNoNegI.lean]
• NQubitPauliGroupElement.AllPhaseZero (+ AllPhaseZero_cons, AllPhaseZero_nil) — phase-zero predicate on generator lists. [QEC/Stabilizer/Foundations/PauliGroup/NQubitElement.lean]
• NQubitPauliGroupElement.rowsLinearIndependent — symplectic check- matrix row independence; closed by decide for small n. [QEC/Stabilizer/Foundations/BinarySymplectic/CheckMatrix.lean]
• GeneratorsIndependent, GeneratorsIndependent_of_rowsLinearIndependent — bundled generator independence from rowsLinearIndependent. [QEC/Stabilizer/Framework/Symplectic/IndependentEquiv.lean]

Commutation tactics

• pauli_comm_componentwise — closes g * h = h * g by per-qubit commutation table; works when supports are disjoint or both are Z-/X-type. [QEC/Stabilizer/Foundations/PauliGroup/CommutationTactics.lean]
• pauli_comm_even_anticommutes — reduces g * h = h * g to "the anticommuting-positions count is even"; used with an explicit filter Finset. [same file]
• pauli_anticomm_odd_anticommutes — reduces Anticommute g h to "the anticommuting-positions count is odd"; used with explicit Finset. [same file]
• NQubitPauliGroupElement.anticommutesAt — per-qubit anticommutation predicate used inside the filter Finset. [QEC/Stabilizer/Foundations/PauliGroup/Commutation.lean]
• NQubitPauliGroupElement.Anticommute — global anticommutation predicate (target of pauli_anticomm_odd_anticommutes). [same file]

Logical-operator infrastructure

• LogicalQubitOps n S — bundle of (xOp, zOp, x_mem_centralizer, z_mem_centralizer, anticommute) per logical qubit. [QEC/Stabilizer/Framework/Core/Logical/LogicalOperators.lean]
• StabilizerGroup.mem_centralizer_iff — translates g ∈ centralizer to a forall-comm form. [QEC/Stabilizer/Framework/Core/Stabilizer/Centralizer.lean]
• centralizer (Subgroup-valued) — the centralizer of a stabilizer group inside the Pauli group. [same file]

Code-level packaging

• StabilizerCode n k (structure) — bundled code with generator list + logical operators. [QEC/Stabilizer/Framework/Core/Stabilizer/StabilizerCode.lean]
• StabilizerCode.toStabilizerGroup — derived StabilizerGroup from the bundled code. [same file]
• StabilizerCodeWithDistance n k d — StabilizerCode + distance fact. [same file, around the end]

Distance machinery

• HasCodeDistance — the distance predicate. [QEC/Stabilizer/Framework/Core/Logical/CodeDistance.lean]
• hasCodeDistance_of — general distance-from-witness schema. [same file]
• IsNontrivialLogicalOperator, IsNontrivialLogicalOperator_iff, LogicalQubitOps.xOp_nontrivial — the nontriviality predicates and their characterization. [QEC/Stabilizer/Framework/Core/Logical/LogicalOperators.lean]
• hasCodeDistance_two_of_anticommute_witness (PR #34) — proven, reusable distance-2 closer from (genSet, h_closure, weight_one_anticomm_witness, weight_2 nontrivial logical) ⟹ HasCodeDistance code 2. Used by:
  • Codes/Small/FourQubit_4_2_2.lean (k=2 CSS detection)
  • Codes/Small/CSS_4_1_2.lean (k=1, multi-Z-stab CSS detection)
  • Codes/Iceberg/N.lean (parametric, full-support stabs) C_6 will be the fourth user — the first multi-Z-stab + k=2 user. [QEC/Stabilizer/Framework/Core/CSS/CSSDistance.lean:165-179]
• no_weight_one_mem_centralizer_of_anticommute_witness — the underlying helper that hasCodeDistance_two_of_anticommute_witness calls into. Provides the weight-1 anti-witness ⟹ no weight-1 centralizer element. [same file:32-71]
• weightOneAt — the weight-1 Pauli group element constructor. [same file:26]

Lightly adapted (existing pattern, new instance)

From Codes/Small/CSS_4_1_2.lean (the closest multi-Z-stab CSS reference)

• ZGenerators_are_ZType pattern: extends 1 → 2 → 2 generators. C_6 uses 2 Z-stabs like CSS_4_1_2.
  • C_6 source: copy CSS_4_1_2.ZGenerators_are_ZType (lines 108-120) verbatim; rename S_Z2 = IIZZ (n=4) to S_Z2 = ZZ II ZZ (n=6).
• S_Z1_comm_S_X1 pattern (partial-support Z vs full-X):
  • C_6 source: similar to CSS_4_1_2.S_Z1_comm_S_X1 (lines 139-149), but here every stab is partial-support, so all 4 cross-commute proofs use the same explicit-Finset pattern.
• weightOneAt_anticomm_S_Z1 pattern (sub-support helper):
  • C_6 source: copy CSS_4_1_2 lines 403-418 verbatim, extend the hi hypothesis from i = 0 ∨ i = 1 (2-disjunction) to i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 (4-disjunction; the support of S_Z1 for n=6).
• hi_dichotomy → hi_trichotomy pattern in weight_one_anticomm_witness:
  • C_6 source: replace hi_dichotomy : (i ∈ {0,1}) ∨ (i ∈ {2,3}) with a 3-disjunction. See gap_audit.md for details.

From Codes/Small/FourQubit_4_2_2.lean (the closest k=2 CSS reference)

• k=2 LogicalQubitOps packaging (logicalOps4_2_2, lines 438-445):
  • C_6 source: copy verbatim, renaming the 4 logicals (logicalX_1 = IIXXII, etc.).
• logical_commute_cross := by fin_cases ... proof (lines 457-467):
  • C_6 source: copy verbatim. Same 4-case dispatch structure.
• Off-diagonal logical commutation proofs (T17-T20):
  • C_6 source: copy FourQubit_4_2_2.logicalX_1_commutes_logicalX_2 (line 278), logicalX_1_commutes_logicalZ_2 (line 282-294), logicalX_2_commutes_logicalZ_1 (line 297-309), logicalZ_1_commutes_logicalZ_2 (line 313) as templates. Adjust the explicit Finsets per the new logical operator supports.
• logicalX_1_mem_centralizer per-generator dispatch (lines 384-394):
  • C_6 source: extends 1-Z + 1-X (2-case) to 2-Z + 2-X (4-case) by expanding the rcases (by simpa [ZGenerators] using hgZ) from with rfl to with rfl | rfl.
• code_has_distance_two proof (lines 534-537):
  • C_6 source: copy verbatim, swap in C_6's witness and weight-2 logical witness.

From Codes/Small/CSS_4_1_2.lean and FourQubit_4_2_2.lean (mixed)

• generatorsList, listToSet_generatorsList ([Z1, Z2, X1, X2]):
  • C_6 source: extend CSS_4_1_2.generatorsList = [S_Z1, S_Z2, S_X1] (3 elements) to [S_Z1, S_Z2, S_X1, S_X2] (4 elements).
• AllPhaseZero_generatorsList (chain of ⟨rfl, ...⟩):
  • C_6 source: extend CSS_4_1_2's 3-level nesting to 4 levels.
• stabilizerGroup_toSubgroup_eq (line 259-262 of CSS_4_1_2):
  • C_6 source: copy verbatim.
• stabilizerCode_toSubgroup_eq (line 393-397 of CSS_4_1_2):
  • C_6 source: copy verbatim.

New per-code definitions (no analog elsewhere)

These are genuinely C_6-specific and have no existing template:

• Z1, Z2, X1, X2 — the four stabilizer Pauli strings as NQubitPauliGroupElement 6.
• logicalX_1, logicalX_2, logicalZ_1, logicalZ_2 — the four logical operators per Knill 2004.
• The 16 specific Finset values ({0,1,2,3}, {0,1}, {2,3}, ...) appearing in the pauli_comm_even_anticommutes filters.
• The 4-disjunction hypotheses (i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 for qubits covered by S_Z1 / S_X1; i = 0 ∨ i = 1 ∨ i = 4 ∨ i = 5 for qubits covered by S_Z2 / S_X2) used in the weightOneAt_anticomm_* helper lemmas.
• The 3-disjunction hi_trichotomy : (i = 0 ∨ i = 1) ∨ (i = 2 ∨ i = 3) ∨ (i = 4 ∨ i = 5) used in weight_one_anticomm_witness.

These are pure data; no new tactic patterns or lemma APIs are added.

Imports needed

Copy verbatim from CSS_4_1_2.lean's import block (lines 1-19):

import Mathlib.Tactic
import QEC.Stabilizer.Framework.Core.Stabilizer.StabilizerGroup
import QEC.Stabilizer.Framework.Core.Stabilizer.SubgroupLemmas
import QEC.Stabilizer.Framework.Core.CSS.CSSPredicates
import QEC.Stabilizer.Framework.Core.CSS.CSSNoNegI
import QEC.Stabilizer.Framework.Core.Stabilizer.Centralizer
import QEC.Stabilizer.Framework.Core.CSS.CSSCommutationLemmas
import QEC.Stabilizer.Framework.Core.Logical.CodeDistance
import QEC.Stabilizer.Framework.Core.CSS.CSSDistance
import QEC.Stabilizer.Framework.Core.Logical.LogicalOperators
import QEC.Stabilizer.Framework.Core.Stabilizer.StabilizerCode
import QEC.Stabilizer.Foundations.PauliGroup.Commutation
import QEC.Stabilizer.Foundations.PauliGroup.CommutationTactics
import QEC.Stabilizer.Foundations.PauliGroup.NQubitOperator
import QEC.Stabilizer.Foundations.PauliGroup.NQubitElement
import QEC.Stabilizer.Foundations.BinarySymplectic.Core
import QEC.Stabilizer.Foundations.BinarySymplectic.CheckMatrix
import QEC.Stabilizer.Foundations.BinarySymplectic.CheckMatrixDecidable
import QEC.Stabilizer.Framework.Symplectic.IndependentEquiv

All imports already exist; no new framework modules required.

Umbrella import

Add the new file to QEC/Stabilizer/Codes/Small.lean:

import QEC.Stabilizer.Codes.Small.SixQubit_6_2_2

The cluster umbrella (QEC/Stabilizer/Codes/Small.lean) already lists the 7 existing small codes; we add the 8th. The transitive umbrella chain to Stabilizer.lean is automatic.

Conclusion

The C_6 formalization adds 0 new framework abstractions and 0 new tactic patterns. Every theorem is a direct adaptation of a pattern proven in CSS_4_1_2.lean or FourQubit_4_2_2.lean. This is the textbook "engineering track" case: the next-rank code on the queue whose proof is mechanical and whose new content is purely data (generators, logicals, Finsets).

Gap audit: [[6,2,2]] C_6 code

This file identifies the anticipated trouble spots in the C_6 formalization. Most are minor mechanical concerns; none are blocking.

Repo gaps (this code surfaces / requires new abstractions)

Nothing genuinely new

C_6 is the fourth user of hasCodeDistance_two_of_anticommute_witness, the second k = 2 CSS code, and the second multi-Z-stabilizer CSS code. Every primitive and pattern it needs already exists.

Minor: 3-way partition pattern in weight_one_anticomm_witness

CSS_4_1_2.lean introduced the hi_dichotomy (2-way partition for qubits covered by S_Z1 vs S_Z2). C_6 needs a 3-way partition:

hi_trichotomy : (i = 0 ∨ i = 1) ∨ (i = 2 ∨ i = 3) ∨ (i = 4 ∨ i = 5)

This is not a gap per se — it's a direct extension of hi_dichotomy to one more case. But if the pattern recurs (e.g. for larger Knill codes or GOY r ≥ 2), it may be worth documenting in docs/lean-patterns.md as a generalization of the 2-way pattern.

Recommended action: leave the trichotomy inline in SixQubit_6_2_2.lean for now; promote to a doc patterns entry when a 4-way / parametric version arrives.

Minor: logical_commute_cross 4-case fin_cases dispatch

The 4-case dispatch in the logical_commute_cross field of StabilizerCode 6 2 is identical in shape to FourQubit_4_2_2.stabilizerCode (lines 457-467). If a third k = 2 CSS code arrives, a LogicalQubitOps.cross_commute_pair smart constructor could collapse the four refine ⟨..., ..., ..., ...⟩ cases into one named lemma per pair (ℓ, ℓ') ∈ Fin 2 × Fin 2. Not blocking; leave for a future refactor when k ≥ 3 makes the boilerplate intolerable.

Mathlib gaps (lemmas not in mathlib v4.30)

None identified. All required mathlib lemmas (Subgroup.closure, Subgroup.forall_comm_closure_iff, Subgroup.mem_centralizer_iff, Finset.mem_filter, Finset.card_*, Fin.cases, mul_assoc, one_mul, mul_one, mul_inv_cancel) are in v4.30.

Likely "BLOCKED(<reason>)" sorries

None anticipated. Every theorem in the skeleton has a clear, existing-template-based closing strategy.

Mechanical risks (Stage-4 specific)

1. Stabilizer support structure for T31 dispatch

Risk. S_Z1 and S_Z2 overlap at qubits {0,1}, disagree at {2,3} (only S_Z1) and {4,5} (only S_Z2). This is NOT a clean disjoint partition — qubits {0,1} are ambiguous for the weight-1 witness function.

Mitigation: in T31, dispatch on a 3-way trichotomy and assign:

• i ∈ {0,1} → pick S_Z1 (arbitrary choice; could equally pick S_Z2).
• i ∈ {2,3} → pick S_Z1.
• i ∈ {4,5} → pick S_Z2.

The helper lemma weightOneAt_anticomm_S_Z1 accepts the 4-disjunction hypothesis i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 (the support of S_Z1), and the witness function dispatches the canonical choice.

Equivalent alternative (slightly cleaner): pick S_Z2 for i ∈ {0,1} instead. Either way, document the canonical choice in the witness function's docstring.

2. pauli_comm_even_anticommutes filter Finset sizes

For the cross-commutation theorems T3-T6, the filter Finsets are:

• T3: {0, 1, 2, 3} (size 4)
• T4: {0, 1} (size 2)
• T5: {0, 1} (size 2)
• T6: {0, 1, 4, 5} (size 4)

All sizes even ⇒ commute, which is the expected CSS structural fact.

Risk: the ext i; fin_cases i <;> simp [...] proof step in each filter-equality lemma now runs fin_cases i over Fin 6 (6 cases) instead of Fin 4 (4 cases). simp [Finset.mem_filter, ...] should still close each case in milliseconds.

Mitigation: if simp is slow on the 6-case branch, fall back to omega or explicit decide after the simp-induced normalization. No real risk; the [[5,1,3]] proof in FiveQubit_5_1_3.lean does similar combinatorics for n = 5.

3. Logical-operator weight irregularity

Unlike FourQubit_4_2_2.lean's clean weight-2 logicals (IXIX, IIXX, IIZZ, IZIZ — all weight 2), C_6's logicals from Knill 2004 have mixed weights: X_L=IIXXII (weight 2), Z_L=ZIIZZI (weight 3), X_S=IXIXXI (weight 3), Z_S=IIIIZZ (weight 2).

Risk: the pauli_comm_componentwise tactic (used for both-X-type and both-Z-type commutations) may be slower or fail on weight-3 operators if the underlying decision procedure has quadratic blowup.

Mitigation: if pauli_comm_componentwise fails, fall back to pauli_comm_even_anticommutes + explicit Finset (which always works, just more verbose). The repo's existing usage of pauli_comm_componentwise [logicalX_1, X1] etc. covers up to weight-4 operators on Fin 4, so weight-3 on Fin 6 should be fine.

4. Even-count weight-2 filter shapes for cross-logical commutation

T19 (X_S = IXIXXI vs Z_L = ZIIZZI) has anticommute filter {3, 4} (size 2). Q3 has X·Z, Q4 has X·Z, both anticommute pairwise; counts to 2 (even) ⇒ commute. T18 (X_L vs Z_S) has empty filter (size 0, even ⇒ commute). The other two (T17, T20) are both X-type or both Z-type so use componentwise.

Risk: writing the explicit Finset {3, 4} in Lean requires unambiguous Fin 6 literals. Use ({3, 4} : Finset (Fin 6)) with type annotation if needed.

Mitigation: copy the explicit-type annotation pattern from CSS_4_1_2.S_Z1_comm_S_X1 (line 145: ({0, 1} : Finset (Fin 4))), just changing the Fin 4 to Fin 6.

5. decide on rowsLinearIndependent for n = 6, 4 rows

The check-matrix for C_6 is 4×12 over GF(2). decide should close this in well under a second (CSS_4_1_2's 3×8 matrix closes nearly instantly). No risk.

6. Picking logicalX_1 = IIXXII (weight 2) as the witness for code_has_distance_two

The distance proof needs ONE witness g with IsNontrivialLogicalOperator g stabilizerCode.toStabilizerGroup AND weight g = 2. Both logicalX_1 (weight 2) and logicalZ_2 (weight 2) qualify. Pick logicalX_1 for canonical alignment with CSS_4_1_2.code_has_distance_two's use of logicalX.

The by decide weight check at the end of the witness construction needs weight (logicalX_1 : NQubitPauliGroupElement 6) = 2, where logicalX_1.operators = ((identity 6).set 2 X).set 3 X. The weight function counts non-I entries; for 6 qubits with two X-positions, the count is 2. No risk — decide reduces this immediately.

7. linter.unusedSimpArgs from NQubitPauliOperator.identity

Per docs/lean-patterns.md § "NQubitPauliOperator.identity in simp sets":

• Drop identity from simp set when the generator's .set chain fully covers Fin n.
• Keep identity for partial-coverage generators.

For C_6 with n = 6:

• S_Z1 = ZZZZ II: covers qubits {0,1,2,3}, leaves {4,5} → fall through to identity. Keep identity in simp.
• S_Z2 = ZZ II ZZ: covers {0,1,4,5}, leaves {2,3} → keep identity.
• S_X1 = XXXX II: covers {0,1,2,3}, leaves {4,5} → keep identity.
• S_X2 = XX II XX: covers {0,1,4,5}, leaves {2,3} → keep identity.

All 4 generators of C_6 are partial-support, so we keep NQubitPauliOperator.identity in every generator-type-check simp invocation (unlike [[4,2,2]]'s ZZZZ/XXXX, which fully cover Fin 4 and drop identity).

8. pauli_comm_componentwise lemma signature

The tactic takes a list of generator names: pauli_comm_componentwise [logicalX_1, logicalX_2]. For T17 (X_L vs X_S) and T20 (Z_L vs Z_S), this is the right path. For T18 (X_L vs Z_S with disjoint supports), we could use the same tactic — both factors commute at every qubit (one is I, the other can be anything, or both are the same Pauli at qubits 0,1). Should work.

Risk: if pauli_comm_componentwise doesn't handle mixed X-then-Z-then-I patterns well, fall back to pauli_comm_even_anticommutes with an empty Finset.

9. Build-time decide on the full skeleton (no proof yet)

The skeleton ends every theorem in sorry. lake build of the new module should produce only "declaration uses sorry" warnings — no errors. Confirm at end of Stage 2 (see success criteria).

Summary

C_6 surfaces no genuine gaps in the repo or in mathlib. The mechanical risks above are all standard for any small CSS code and already have documented mitigations in CLAUDE.md, docs/lean-patterns.md, and the existing FourQubit_4_2_2.lean / CSS_4_1_2.lean templates. Stage 4 should close all 33 sorries in ~3 hours of attentive work.

Progress log: stab_6_2_2 ([[6,2,2]] C_6 code)

Session 1 (2026-05-24)

• Starting sorries: 47 across 33 theorems (T1–T32, plus 4 sub-helpers each for T21–T24 and 4 helpers for T31)
• Budget: 8h, per-sorry 15min autoprove + 25min sorry-filler-deep
• Strategy: pattern-blend of FourQubit_4_2_2.lean (k=2 structure) + CSS_4_1_2.lean (multi-Z-stab structure)
• Plan order: T1-T9 (Z-type / X-type / commute), T10-T14 (generator list + StabilizerGroup), T15-T20 (logical anti / off-diagonal commute), T21-T24 (logical-vs-stab commutes), T25-T28 (centralizer), T29 (StabilizerCode), T30 (subgroup bridge), T31 (weight-1 witness, with 4 helpers T31a-d), T32 (distance)
• Baseline lake build QEC.Stabilizer.Codes.Small.SixQubit_6_2_2 confirmed clean (sorries only)

Closing notes

The closing strategy was direct template application rather than agent spawning: the two templates (CSS_4_1_2 + FourQubit_4_2_2) were line-by-line clear from plan.md and reuse_audit.md, and the plan.md proof sketches included exact Finset values. Hand-writing each proof following the documented template was much faster than spawning autoprove subagents — the wall-clock per sorry averaged ~1 minute (vs. autoprove's 5-15 minutes per closure).

Three commit batches:

1. 2fb8033 (T1-T14): Z-type, X-type, cross-commute, generator-list infra.
2. c8a0b03 (T15-T29): logical anti/comm + 16 logical-vs-stab lemmas
   • 4 centralizer-membership + StabilizerCode 6 2 packaging.
3. db2788a (T30-T32): subgroup bridge + 4 T31 helpers + 3-way trichotomy main witness + distance theorem.

Final state:

• Sorries closed: 47 / 47 (zero blocked)
• lake build of module: clean, zero warnings, zero info notices
• lake build repo-wide: clean (3425 jobs; one pre-existing warning in QEC/Stabilizer/Stabilizer.lean umbrella header is unrelated)
• LoC: 805 (60% larger than CSS_4_1_2's 499, tracking the combinatorial expansion to 16 logical-vs-stab lemmas + 4 T31 helpers)
• Wall-clock: ~45 minutes total

No final lean4:proof-golfer pass needed — every proof is already template-shaped and follows the existing style. The boilerplate that could be shortened (the pauli_comm_even_anticommutes + Finset.ext + decide template, repeated ~16 times) is identical to the CSS_4_1_2 and FourQubit_4_2_2 patterns; collapsing it requires a new tactic abstraction that isn't C_6-specific (noted as follow-up #1 in result.md).