Informal spec: [[4,1,2]] LNCY code

Summary

The Leung-Nielsen-Chuang-Yamamoto (LNCY) [[4,1,2]] code is a four-qubit CSS stabilizer code encoding one logical qubit with code distance 2. It detects (but does not correct) a single arbitrary Pauli error and is the unique four-qubit qubit-CSS code with these parameters. The code was introduced in Leung, Nielsen, Chuang, Yamamoto, Approximate quantum error correction can lead to better codes [arxiv:quant-ph/9704002], where it is also shown to approximately correct a single amplitude-damping error with recovery fidelity 1 − 5γ² + O(γ³). We formalize the standard distance-2 stabilizer-detection structure here; the AD-recovery result is out of scope for this skeleton.

Parameters

• Physical qubits: n = 4
• Logical qubits: k = 1
• Distance: d = 2
• Family: CSS (two Z-type stabilizers, one X-type stabilizer)
• Originally introduced in: Leung-Nielsen-Chuang-Yamamoto 1997 [arxiv:quant-ph/9704002 §II, Eqs. 5–6]
• EC Zoo entry: css_4_1_2 ("[[4,1,2]] LNCY code")

Codeword basis (LNCY convention)

From [arxiv:quant-ph/9704002 §II, Eqs. 5–6]:

|0_L⟩ = (|0000⟩ + |1111⟩)/√2
|1_L⟩ = (|0011⟩ + |1100⟩)/√2

Qubit indexing in this skeleton is 0-based (so the four qubits are indexed 0, 1, 2, 3). The kets above are written in qubit-0-leftmost convention.

Stabilizer generators

Three independent generators (n − k = 3), in canonical Z-then-X order. The paper presents the code by its codewords, not by stabilizers; we use the standard stabilizer presentation that stabilizes the LNCY codewords:

(2 Z-type + 1 X-type, totalling n − k = 3 independent generators.)

Verification that these stabilize the LNCY codewords:

• S_Z1 = ZZII: eigenvalue +1 on |0000⟩ (q₀q₁=00), |1111⟩ (q₀q₁=11), |0011⟩ (q₀q₁=00), |1100⟩ (q₀q₁=11). So +1 on |0_L⟩ and |1_L⟩. ✓
• S_Z2 = IIZZ: same reasoning on q₂q₃. +1 on both codewords. ✓
• S_X1 = XXXX: maps |0000⟩ ↔ |1111⟩ and |0011⟩ ↔ |1100⟩, so |0_L⟩ → |0_L⟩ and |1_L⟩ → |1_L⟩. ✓

Alternative tableau in EC Zoo description. The EC Zoo entry quotes the Qiskit preset tableau (XXII, IIXX, ZZZZ). That tableau does not stabilize the LNCY codewords above — instead, XXII and IIXX are logical X representatives (each takes |0_L⟩ ↦ |1_L⟩). The two presentations are equivalent up to a swap of the X-side and Z-side roles, but they describe different codes-as-subspaces unless the codeword conventions are also swapped. We use the LNCY paper's codeword convention as the ground truth; the stabilizer triple (ZZII, IIZZ, XXXX) is the canonical stabilizer for those codewords. This is the same convention used implicitly by the parent code [[4,2,2]] (FourQubit_4_2_2.lean), where XXXX and ZZZZ are the stabilizers and IIZZ, IZIZ etc. become logical operators.

Logical operators

(One logical qubit ⇒ a single logicalX and logicalZ.)

Verification:

• logicalX = XXII: maps |0000⟩ ↔ |1100⟩, |1111⟩ ↔ |0011⟩. So |0_L⟩ = (|0000⟩+|1111⟩)/√2 ↦ (|1100⟩+|0011⟩)/√2 = |1_L⟩. ✓
• logicalZ = ZIZI: eigenvalues — |0000⟩ → +, |1111⟩ → +1·−1 = +1 (Z·I·Z·I = +1 on bits q₀,q₂ = 0,0; +1 on q₀,q₂=1,1). Wait, recompute: ZIZI on |q₀q₁q₂q₃⟩ gives (-1)^(q₀+q₂). On |0000⟩: (-1)^0 = +1. On |1111⟩: (-1)^2 = +1. So |0_L⟩ → +|0_L⟩ ✓. On |0011⟩: (-1)^(0+1) = -1. On |1100⟩: (-1)^(1+0) = -1. So |1_L⟩ → -|1_L⟩ ✓.

Commutation/anticommutation table (✓ = commute, ✗ = anticommute):

Codespace

The codespace is 2^k = 2-dimensional, spanned by |0_L⟩ and |1_L⟩ as above. The stabilizer projector is

P_C = (1/8)(I + S_Z1)(I + S_Z2)(I + S_X1)

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

Theorems to formalize

The skeleton mirrors Steane7.lean adapted for (n,k,d) = (4,1,2) and the 2-Z / 1-X CSS structure. With three Z×X cross-commutation pairs only two are needed (since there is one X-generator and two Z-generators): S_Z1·S_X1 and S_Z2·S_X1.

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. No paper citation; this is a verification of the generator definitions.

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

Statement. ∀ g ∈ XGenerators, IsXTypeElement g. Reference: same as T1.

T3: cross-commutation S_Z1 · S_X1 = S_X1 · S_Z1

Statement. ZZII and XXXX overlap (anticommute pairwise) at qubits 0 and 1, total 2 anticommuting positions (even) → operators commute. Reference: paper's stabilizer structure (implicit in Eqs. 5–6); standard CSS argument via commutes_iff_even_anticommutes.

T4: cross-commutation S_Z2 · S_X1 = S_X1 · S_Z2

Statement. IIZZ and XXXX anticommute pairwise at qubits 2 and 3, total 2 anticommuting positions (even) → commute. Same reference as T3.

T5: all-pair generator commutation

Statement. ∀ g h ∈ generators, g * h = h * g. Follows from T1–T4 plus the CSS shortcuts ZType_commutes, XType_commutes. Reference: implicit in [LNCY §II] (any stabilizer code requires this).

T6: −I ∉ stabilizer subgroup

Statement. negIdentity 4 ∉ Subgroup.closure generators. Standard CSS proof via CSS.negIdentity_not_mem_closure_union.

T7: generator list ↔ generator set equality

Statement. listToSet generatorsList = generators where generatorsList = [S_Z1, S_Z2, S_X1].

T8: all generators have phase 0

Statement. AllPhaseZero generatorsList.

T9: rows of the check matrix are linearly independent

Statement. rowsLinearIndependent generatorsList. The check matrix has 3 rows over GF(2)^8 and is verifiable by decide for n = 4.

T10: generator independence

Statement. GeneratorsIndependent 4 generatorsList. Follows from T9.

T11: stabilizerGroup.toSubgroup = subgroup

Statement. The bundled StabilizerGroup 4 built from generatorsList has the same underlying subgroup as Subgroup.closure generators.

T12: logical X and logical Z anticommute

Statement. Anticommute logicalX logicalZ. XXII · ZIZI anticommute pairwise only at qubit 0 (X·Z, then X·I, then I·Z, then I·I); exactly 1 anticommuting position (odd) → anticommute.

T13: logical X commutes with each stabilizer generator

Statement. XXII commutes with each of ZZII, IIZZ, XXXX:

• vs ZZII: anticommuting at qubits 0, 1; total 2 (even) → commute.
• vs IIZZ: no overlap → commute.
• vs XXXX: both X-type → commute.

T14: logical Z commutes with each stabilizer generator

Statement. ZIZI commutes with each of ZZII, IIZZ, XXXX:

• vs ZZII: both Z-type → commute.
• vs IIZZ: both Z-type → commute.
• vs XXXX: anticommuting at qubits 0, 2; total 2 (even) → commute.

T15: logicalX ∈ centralizer stabilizerGroup

Statement. Follows from T13 via Subgroup.forall_comm_closure_iff.

T16: logicalZ ∈ centralizer stabilizerGroup

Statement. Follows from T14 via the same idiom.

T17: StabilizerCode 4 1 packaging

Statement. The bundled StabilizerCode 4 1 stabilizerCode is constructed from generatorsList with logicalOps : Fin 1 → LogicalQubitOps 4 stabilizerGroup built from T15, T16, T12. The k = 1 case uses logical_commute_cross := fun ℓ ℓ' h => (h (Subsingleton.elim ℓ ℓ')).elim.

T18: stabilizerCode.toStabilizerGroup.toSubgroup = Subgroup.closure generators

Statement. Bridge between the bundled stabilizer-code view and the raw Subgroup.closure generators view. Used by the distance proof.

T19: every weight-1 single-qubit Pauli anticommutes with some generator

Statement. ∀ i : Fin 4, ∀ P ∈ {X, Y, Z}, ∃ g ∈ generators, Anticommute (weightOneAt i P) g.

Proof outline (mirroring FourQubit_4_2_2.lean):

• P = X: anticommutes with one of the Z-stabilizers (S_Z1 if i ∈ {0,1}, S_Z2 if i ∈ {2,3}).
• P = Y: same (Y locally anticommutes with Z, like X does).
• P = Z: anticommutes with S_X1 = XXXX.

T20: code distance = 2 (HasCodeDistance stabilizerCode 2)

Statement.

HasCodeDistance stabilizerCode 2

i.e. (i) distance ≥ 1 [decide], (ii) logicalX = XXII is a nontrivial logical operator of weight exactly 2 [witness], and (iii) no weight-1 Pauli is a nontrivial logical operator [from T19, via no_weight_one_mem_centralizer_of_anticommute_witness].

Method: finite enumeration (n = 4 is small); the helper hasCodeDistance_of from Framework/Core/Logical/CodeDistance.lean reduces the proof to T19 plus the witness logicalX.

Reference: distance-2 claim is from [LNCY §II] — "the code corrects for a single amplitude damping error" (under the approximate-EC criterion; the distance-2 detection property is the projective version of that). The EC Zoo entry states: "Detects a single-qubit error or single erasure as a distance-two code".

T21: bundled StabilizerCodeWithDistance 4 1 2

Statement. Package T17 with T20 into the StabilizerCodeWithDistance structure for downstream use.

Edge cases / convention notes

1. Qubit indexing is 0-based. Throughout the skeleton, qubits are Fin 4 = {0, 1, 2, 3}. The LNCY paper writes |n₁ n₂ n₃ n₄⟩ with 1-based indices; under our 0-based convention, n₁ ↔ q₀, n₂ ↔ q₁, n₃ ↔ q₂, n₄ ↔ q₃. The codeword strings (0000, 1111, 0011, 1100) are identical under either indexing — only the labels change.

2. Codeword convention is locked. Stage-2 review must check the LNCY codewords (Eqs. 5–6) vs. the chosen stabilizer (ZZII, IIZZ, XXXX). The chosen stabilizers stabilize exactly the LNCY codewords as derived above. If the reviewer prefers the EC Zoo "Qiskit ID 6" tableau (XXII, IIXX, ZZZZ), then logicalX should be ZIZI or ZZZZ-type and logicalZ should be XXII-type — but this corresponds to a different 2-d subspace of the four-qubit Hilbert space. We use the LNCY codeword convention as the gold standard.

3. No nontrivial phases on stabilizer generators. All three generators have phasePower = 0. No i-factor or −1-factor appears.

4. No logical Y in this skeleton. For k = 1 codes the optional logicalY can be derived as i · X̄ · Z̄, but the LNCY paper does not single out logicalY, and it is not required for any downstream theorem. We omit it; a Stage-4 follow-up could add it following the Steane7 pattern.

5. HasCodeDistance vs. amplitude-damping recovery. The paper's main result (Eq. 20, fidelity 1 − 5γ² + O(γ³) under AD) uses approximate error correction criteria. Our HasCodeDistance 2 captures only the projective distance-2 detection property — it does not claim approximate AD correction. The AD result would require a separate framework not currently in the repo (continuous-parameter noise channels, residue-norm bounds, etc.) and is explicitly out-of-scope for this skeleton.

6. Uniqueness claim. EC Zoo describes this as "the only qubit CSS code with such parameters". We do not formalize this uniqueness in this skeleton — it would require classifying all [[4,1,2]] CSS codes up to equivalence, which is a substantial separate theorem. The skeleton instantiates one such code and proves its distance; uniqueness is left as future work.

Formalization plan: [[4,1,2]] LNCY code

Strategy summary

The [[4,1,2]] LNCY code is a CSS code with 2 Z-stabilizers + 1 X-stabilizer on 4 qubits, encoding 1 logical qubit. The structure is exceptionally close to the existing FourQubit_4_2_2.lean (same n = 4, same CSS detection shape), differing only in:

• Stabilizer split: LNCY has (ZZII, IIZZ, XXXX) (2 Z + 1 X) vs. [[4,2,2]]'s (ZZZZ, XXXX) (1 Z + 1 X);
• Logical structure: k = 1 instead of k = 2, so the Subsingleton.elim-shortcut closes logical_commute_cross (no need for the off-diagonal pairwise commutation theorems);
• Logical operators: logicalX = XXII, logicalZ = ZIZI (specific Paulis on weight-2 supports) instead of the four logicals IXIX/IIXX/IIZZ/IZIZ of the [[4,2,2]] code.

The distance proof reuses the existing no_weight_one_mem_centralizer_of_anticommute_witness helper (Framework/Core/CSS/CSSDistance.lean) — essentially the same proof shape as FourQubit_4_2_2.lean's code_has_distance_two, adjusted for the new generator partition.

Distance method: finite enumeration via the standard CSS helper. No homological framework needed; n = 4 is small enough that decide on weight-1 anti-witness suffices.

Theorem dependency graph

T1 (Z-type)       T3 (S_Z1·S_X1 = comm)     T8 (phase 0)
T2 (X-type)       T4 (S_Z2·S_X1 = comm)     T9 (rows indep)
   \                 /
    T5 (gen commute)        T7 (list ↔ set)        T10 (gens indep, ← T9)
       \                       /
        T6 (-I ∉ subgroup)     T11 (stabGroup.toSubgroup = subgroup)
              \                  /
               T8 + T10 + T6 → T17 partial setup
                          |
T12 (X̄ ⊥ Z̄)              |
T13 (X̄ ⊥ stabs)  T14 (Z̄ ⊥ stabs)
       \              /
        T15, T16 (logicals in centralizer)
              \    /
              T17 (StabilizerCode 4 1) ← needs T7, T8, T10, T5, T6, T12, T15, T16
                 |
              T18 (subgroup bridge)
                 |
T19 (weight-1 anticomm witness)
                 |
              T20 (HasCodeDistance 2) ← needs T17, T18, T19, T12 (logicalX nontrivial)
                 |
              T21 (StabilizerCodeWithDistance)

Per-theorem proof sketch

T1: ZGenerators are Z-type

• Approach: rcases hg with rfl | rfl; then for each generator, fin_cases i <;> simp [...] on the per-qubit predicate.
• Reuse: copy FourQubit_4_2_2.ZGenerators_are_ZType verbatim, expand to 2 generators instead of 1.
• Difficulty: trivial.

T2: XGenerators are X-type

• Approach: same as T1, with only 1 X-generator (matching FourQubit_4_2_2.XGenerators_are_XType).
• Difficulty: trivial.

T3: S_Z1 * S_X1 = S_X1 * S_Z1 (i.e. ZZII and XXXX)

• Approach: pauli_comm_even_anticommutes; the anticommute-filter Finset is {0, 1} (size 2 = even).
• Reuse: line-for-line analog of Z1_comm_X1 in FourQubit_4_2_2.lean:114.
• Difficulty: trivial (standard CSS pattern).

T4: S_Z2 * S_X1 = S_X1 * S_Z2 (i.e. IIZZ and XXXX)

• Approach: same; anticommute-filter Finset is {2, 3} (size 2 = even).
• Difficulty: trivial.

T5: 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.

T6: -I ∉ subgroup

• Approach: one-shot via CSS.negIdentity_not_mem_closure_union, fed T1, T2, and the cross-commutation T3+T4 packaged as ZGenerators_commute_XGenerators.
• Reuse: copy FourQubit_4_2_2.negIdentity_not_mem verbatim.
• Difficulty: trivial.

T7: listToSet generatorsList = generators

• Approach: ext g; simp after unfolding. Three elements in the list, three in the set (split as 2-Z + 1-X union).
• Reuse: minor adaptation of FourQubit_4_2_2.listToSet_generatorsList.
• Difficulty: trivial.

T8: AllPhaseZero generatorsList

• Approach: chain of AllPhaseZero_cons.mpr ⟨rfl, …⟩ per element. Three elements ⇒ three nested ⟨rfl, …⟩.
• Reuse: pattern from any small code (Steane7 has 6, [[4,2,2]] has 2).
• Difficulty: trivial.

T9: rows linearly independent

• Approach: by decide. Three rows in (GF(2))^8; concrete and tiny.
• Difficulty: trivial.

T10: generators independent

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

T11: stabilizerGroup.toSubgroup = subgroup

• Approach: unfold mkStabilizerFromGenerators + apply T7.
• Reuse: copy FourQubit_4_2_2.stabilizerGroup_toSubgroup_eq verbatim.
• Difficulty: trivial.

T12: Anticommute logicalX logicalZ (i.e. XXII vs ZIZI)

• Approach: pauli_anticomm_odd_anticommutes; anticommute-filter Finset is {0} (size 1 = odd). Q1 (X·I), Q2 (I·Z), Q3 (I·I) all commute.
• Reuse: pattern from FourQubit_4_2_2.logicalX_1_anticommutes_logicalZ_1.
• Difficulty: trivial.

T13: logicalX commutes with each generator (3 lemmas)

• Approach: per generator, pauli_comm_even_anticommutes + explicit Finset. Cases:
  • vs S_Z1=ZZII: filter {0, 1} (size 2).
  • vs S_Z2=IIZZ: filter {} (size 0).
  • vs S_X1=XXXX: pauli_comm_componentwise (both X-type).
• Reuse: combinations of FourQubit_4_2_2.logicalX_i_commutes_* patterns.
• Difficulty: trivial.

T14: logicalZ commutes with each generator (3 lemmas)

• Approach: dual of T13. Cases:
  • vs S_Z1=ZZII: pauli_comm_componentwise (both Z-type).
  • vs S_Z2=IIZZ: pauli_comm_componentwise (both Z-type).
  • vs S_X1=XXXX: filter {0, 2} (size 2).
• Difficulty: trivial.

T15: logicalX ∈ centralizer stabilizerGroup

• Approach: standard idiom (used in FourQubit_4_2_2.lean):

  rw [StabilizerGroup.mem_centralizer_iff,
      stabilizerGroup_toSubgroup_eq, subgroup]
  rw [Subgroup.forall_comm_closure_iff]
  intro s hs
  ...
  

• Reuse: copy FourQubit_4_2_2.logicalX_1_mem_centralizer verbatim (modulo generator-set unfolding).
• Difficulty: trivial.

T16: logicalZ ∈ centralizer stabilizerGroup

• Approach: same as T15.
• Difficulty: trivial.

T17: StabilizerCode 4 1 packaging

• Approach: structure literal with fields populated from T7–T16. logical_commute_cross := fun ℓ ℓ' h => (h (Subsingleton.elim ℓ ℓ')).elim closes the cross-commute field trivially in the k = 1 case.
• Reuse: copy Steane7.stabilizerCode shape (k = 1 case).
• Difficulty: trivial.

T18: stabilizerCode.toStabilizerGroup.toSubgroup = Subgroup.closure generators

• Approach: unfold + apply T7.
• Reuse: pattern from FourQubit_4_2_2.stabilizerCode_toSubgroup_eq (it's private there; we'll need to re-prove or mirror it).
• Difficulty: trivial.

T19: weight-1 anticommute witness

• Approach: backtracking dispatch by (i, P) cases:

  match P, hP with
  | .X, _ | .Y, _ => ⟨S_Z_(i covers), ..., weight_anticomm_Z_proof⟩
  | .Z, _ => ⟨S_X1, ..., weight_anticomm_X1_proof⟩
  | .I, hP => exact (hP rfl).elim
  

  Two helper lemmas needed:
  • weightOneAt_anticomm_S_Z (i : Fin 4) (P ∈ {X, Y}): for the Z-side, pick S_Z1 if i ∈ {0,1}, S_Z2 if i ∈ {2,3}. Internally fin_cases i splits.
  • weightOneAt_Z_anticomm_S_X1 (i : Fin 4): weight-1 Z at any qubit anticommutes with S_X1 = XXXX.
• Reuse: very close to FourQubit_4_2_2.weight_one_anticomm_witness, with the twist that we need to pick which Z-generator to use (the [[4,2,2]] code had only one Z, so no branching). Use a sub-case on i < 2 vs i ≥ 2.
• Difficulty: standard (slightly more cases than [[4,2,2]]).

T20: HasCodeDistance stabilizerCode 2

• Approach:

  refine hasCodeDistance_of stabilizerCode 2 (by decide)
    ⟨logicalX, (logicalOps 0).xOp_nontrivial, by decide⟩ ?_
  intro w hw_pos hw_lt g hg_weight h_nontrivial
  interval_cases w
  -- w = 1 case: use T19 + helper
  rcases (IsNontrivialLogicalOperator_iff _ _).mp h_nontrivial with ⟨h_cent, _, _⟩
  exact no_weight_one_mem_centralizer_of_anticommute_witness
    stabilizerCode.toStabilizerGroup generators T18 T19 g hg_weight h_cent
  

• Reuse: copy FourQubit_4_2_2.code_has_distance_two (line 534).
• Difficulty: standard.

T21: StabilizerCodeWithDistance 4 1 2

• Approach: one-line structure literal bundling T17 + T20.
• Difficulty: trivial.

Risk register

1. Tableau-vs-codewords confusion. The EC Zoo description quotes a Qiskit tableau (XXII, IIXX, ZZZZ) that is the dual of our chosen stabilizer (ZZII, IIZZ, XXXX) (X and Z roles flipped, same up to CSS swap). If a reviewer interprets the EC Zoo tableau as the ground-truth stabilizer, they would mark our logicalX = XXII as wrong (it would be a stabilizer under their convention) and demand logicalX = ZZZZ or ZZII. We document this clearly in informal_spec.md § "Stabilizer generators" — the chosen stabilizers are dictated by the LNCY paper's codewords (Eqs. 5–6), not by the Qiskit preset. Mitigation already in place.

2. Logical Z support choice ambiguity. logicalZ = ZIZI is one valid choice; logicalZ' = IZIZ differs from it by ZZZZ, and ZZZZ = S_Z1 · S_Z2 lies in the stabilizer. So ZIZI and IZIZ are the same logical Z modulo the stabilizer. The choice is arbitrary; we pick ZIZI for symmetry with logicalX = XXII. No theorem statement depends on this choice except T14 (the support of the explicit Finset would change).

3. hasCodeDistance_of step for w = 0 lower bound. The helper signature in CodeDistance.lean:52 takes ∀ w, 1 ≤ w → w < d → ..., so w = 0 is excluded. With d = 2, only w = 1 needs handling, making this very clean.

4. Worktree symlink. Done at setup — lake build should reuse main's mathlib. If a future lake build fails with "Mathlib not found", check .lake/packages symlink integrity.

Estimated effort

• Lines of code: ~320 (slightly above the catalog's 300 estimate; the extra Z-generator + one extra cross-commutation lemma vs. the [[4,2,2]] file account for the bulk).
• Hours: ~2–3 for an experienced agent following the FourQubit_4_2_2.lean template.
• Longest theorem: T19 (weight-1 anticommute witness) with ~8 cases. Should close in one attempt if the helper lemmas are written carefully.
• Total sorry count to close: 21 (one per theorem; some bundle several lemmas into one sorry block for atomicity, see the Lean skeleton's TODO(css_4_1_2-T<n>) markers).

Reuse audit: [[4,1,2]] LNCY code

This code is exceptionally close in structure to FourQubit_4_2_2.lean (same n = 4, same CSS detection structure, same distance proof method) and Steane7.lean (canonical k = 1 CSS instantiation). Reuse is correspondingly very high.

Directly applicable (use as-is)

Core types and structures

• NQubitPauliGroupElement 4 — physical Pauli group on 4 qubits (QEC/Stabilizer/Foundations/PauliGroup/NQubitElement.lean)
• NQubitPauliOperator.identity 4 — the all-I operator
• NQubitPauliOperator.set i P — set qubit i to local Pauli P
• Subgroup.closure, StabilizerGroup 4, mkStabilizerFromGenerators
• IsXTypeElement, IsZTypeElement from Framework/Core/CSS/CSSPredicates.lean
• LogicalQubitOps 4 stabilizerGroup — bundled logical-qubit data (Framework/Core/Logical/LogicalOperators.lean:189)
• StabilizerCode 4 1, StabilizerCodeWithDistance 4 1 2 (Framework/Core/Stabilizer/StabilizerCode.lean, Framework/Core/Logical/CodeDistance.lean:81)
• HasCodeDistance predicate (Framework/Core/Logical/CodeDistance.lean:28)
• centralizer, StabilizerGroup.mem_centralizer_iff, Subgroup.forall_comm_closure_iff (Framework/Core/Stabilizer/Centralizer.lean)

CSS shortcuts (all directly applicable — this is a CSS code)

• CSS.negIdentity_not_mem_closure_union (Framework/Core/CSS/CSSNoNegI.lean) — closes -I ∉ closure(Z ∪ X) given the type predicates and the cross-commutation hypothesis.
• CSSCommutationLemmas.ZType_commutes and XType_commutes (Framework/Core/CSS/CSSCommutationLemmas.lean) — two Z-type elements always commute, same for X-type.
• weightOneAt, no_weight_one_mem_centralizer_of_anticommute_witness (Framework/Core/CSS/CSSDistance.lean:25, :31) — the distance proof is one application of this lemma + a weight-1 anti-witness function (T19).

Tactics

• pauli_comm_componentwise [...] — closes g * h = h * g when no two qubits anticommute (e.g. both Z-type) (Foundations/PauliGroup/CommutationTactics.lean:36).
• pauli_comm_even_anticommutes — converts g * h = h * g to an "even number of anticommuting qubits" goal (Foundations/PauliGroup/CommutationTactics.lean:54).
• pauli_anticomm_odd_anticommutes — same for Anticommute g h (Foundations/PauliGroup/CommutationTactics.lean:66).

Independence machinery

• rowsLinearIndependent (decidable on small n) (Foundations/BinarySymplectic/CheckMatrixDecidable.lean)
• GeneratorsIndependent_of_rowsLinearIndependent (Framework/Symplectic/IndependentEquiv.lean)
• AllPhaseZero_cons, AllPhaseZero_nil (Foundations/PauliGroup/NQubitElement.lean)

Helpers used in the distance proof

• hasCodeDistance_of (Framework/Core/Logical/CodeDistance.lean:54)
• IsNontrivialLogicalOperator_iff (Framework/Core/Logical/LogicalOperators.lean:176)
• LogicalQubitOps.xOp_nontrivial (Framework/Core/Logical/LogicalOperators.lean:326)

Lightly adapted (existing pattern, new instance)

Top-level file structure

Mirror FourQubit_4_2_2.lean (Codes/Small/FourQubit_4_2_2.lean) at the section level (§1 generators → §14 distance). The differences:

• §1 (generators): [[4,2,2]] has {ZZZZ, XXXX}; LNCY has {ZZII, IIZZ, XXXX}. Add one extra Z-generator definition (S_Z2).
• §3, §4 (typing/cross-commutation): 2×1 = 2 cross pairs instead of 1×1 = 1. Pattern unchanged, just one more lemma.
• §9 (independence): decide runs on a 3-row matrix instead of 2-row. Still trivially decidable.
• §10–§13 (logicals): only one logical qubit (logicalX, logicalZ) instead of two; the Subsingleton.elim shortcut from Steane7.lean:510 discharges logical_commute_cross. Pattern from Steane7, not [[4,2,2]].
• §14 (distance): T19's anti-witness function dispatches over which Z-generator to use (S_Z1 for i ∈ {0, 1}, S_Z2 for i ∈ {2, 3}). [[4,2,2]] had only one Z-generator so no such split.

Specific copy-paste sites (with adaptation)

• Z1, Z2 (S_Z1, S_Z2): adapt from Steane7.lean:49-65 (per-qubit .set chain) for support {0, 1} and {2, 3} respectively.
• X1 (S_X1 = XXXX): directly reuse the definition from FourQubit_4_2_2.lean:64 (XXXX).
• ZGenerators, XGenerators, generators, subgroup: Steane7.lean:85-98 pattern.
• ZGenerators_are_ZType: Steane7.lean:105 pattern for 2 Z generators (rcases with rfl | rfl).
• XGenerators_are_XType: FourQubit_4_2_2.lean:99 pattern (1 X generator).
• Cross-commutation S_Z1_comm_S_X1, S_Z2_comm_S_X1: copy FourQubit_4_2_2.Z1_comm_X1 (line 114), adjusting Finset for {0, 1} and {2, 3}.
• ZGenerators_commute_XGenerators: Steane7.lean:227 pattern (2×1 cases instead of 3×3).
• generators_commute, negIdentity_not_mem, generatorsList, listToSet_generatorsList: all line-for-line analogs of FourQubit_4_2_2.lean:149, :165, :175, :179.
• AllPhaseZero_generatorsList: nested ⟨rfl, ...⟩ for 3 elements (extend FourQubit_4_2_2.lean:188 from 2 to 3).
• rowsLinearIndependent_generatorsList, GeneratorsIndependent_4_generatorsList: copy FourQubit_4_2_2.lean:195-202.
• stabilizerGroup, stabilizerGroup_toSubgroup_eq: copy FourQubit_4_2_2.lean:207-215.
• logicalX, logicalZ: define directly (XXII and ZIZI per the spec). Use the .set pattern from FourQubit_4_2_2.lean:227-240.
• logicalX_anticommutes_logicalZ: FourQubit_4_2_2.lean:245 pattern with filter {0} (size 1).
• Per-generator logical-commutation lemmas (logicalX_commutes_S_Z1 etc.): 6 lemmas total (2 logicals × 3 generators). Each follows FourQubit_4_2_2.lean:318 or :331 (pauli_comm_componentwise for same-type-type commute, pauli_comm_even_anticommutes + Finset for cross-type commute).
• logicalX_mem_centralizer, logicalZ_mem_centralizer: FourQubit_4_2_2.lean:384-407 pattern, simplified to one logical per centralizer (no k = 2 partitioning).
• stabilizerCode, logicalOps: Steane7.lean:496-510 pattern (k = 1 case with Subsingleton.elim cross-commute).
• stabilizerCode_toSubgroup_eq: FourQubit_4_2_2.lean:472 pattern (private bridge lemma).
• weightOneAt_anticomm_S_Z, weightOneAt_Z_anticomm_S_X1: adapt FourQubit_4_2_2.lean:480 and :499 patterns; the Z-side helper needs an extra parameter for which Z-generator (or two separate lemmas: one for S_Z1, one for S_Z2).
• weight_one_anticomm_witness: FourQubit_4_2_2.lean:517 pattern, with an inner fin_cases i to dispatch between S_Z1 and S_Z2.
• code_has_distance_two: FourQubit_4_2_2.lean:534 pattern.
• stabilizerCodeWithDistance: FourQubit_4_2_2.lean:546 pattern.

New per-code definitions

Nothing genuinely new — every definition has a 1-to-1 analog in FourQubit_4_2_2.lean or Steane7.lean. The only structural novelty is the 2-Z + 1-X split (everything else in the repo has either balanced splits or single-generator splits per Pauli type), but no new abstraction is required to express it.

Umbrella file update

Add the new module to the Codes/Small.lean umbrella: QEC/Stabilizer/Codes/Small.lean currently imports 6 small codes (Shor9, Steane7, Steane7TransversalGates, FourQubit_4_2_2, QuantumHamming, FiveQubit_5_1_3). Append:

import QEC.Stabilizer.Codes.Small.CSS_4_1_2

and update the doc comment to mention the LNCY [[4,1,2]] code.

Gap audit: [[4,1,2]] LNCY code

Repo gaps (this code surfaces / requires new abstractions)

None. This code is the cleanest possible engineering-track CSS formalization. It exercises the standard CSS path end-to-end:

• Z/X type predicates → already in Framework/Core/CSS/CSSPredicates.lean
• CSS no--I shortcut → Framework/Core/CSS/CSSNoNegI.lean
• CSS commutation lemmas (ZType×ZType, XType×XType) → Framework/Core/CSS/CSSCommutationLemmas.lean
• Weight-1 anticomm-witness distance helper → Framework/Core/CSS/CSSDistance.lean
• k = 1 packaging via Subsingleton.elim cross-commute shortcut → used in Steane7.lean:510
• StabilizerCodeWithDistance bundling → standard
• Distance proof via hasCodeDistance_of + weight_one_anticomm_witness → exactly the [[4,2,2]] pattern, with the only twist being a 2-way case-split on i < 2 vs i ≥ 2 for the Z-generator choice.

The skeleton is essentially a CSS-detection-code "second exerciser" of the same path that FourQubit_4_2_2.lean walked. No new abstraction is justified by this one code; if a third CSS detection code is added (e.g. iceberg / [[2m, 2m-2, 2]] next in the queue), a small lemma CSS.distance_two_of_anticomm_witness that bundles hasCodeDistance_of + weight_one_anticomm_witness + IsNontrivialLogicalOperator_iff into one call would deduplicate this distance-2 pattern. Not blocking for this code.

Mathlib gaps (lemmas not in mathlib v4.30)

None anticipated. Everything needed is either project-local (the pauli_* tactics, weightOneAt, etc.) or in standard mathlib v4.30 (Subgroup.closure, Finset.filter, decide, Fin.cases, Subsingleton.elim).

Likely "BLOCKED(<reason>)" sorries

None expected. Stage 4 should close all 21 sorries in one or two attempt rounds, with the only realistic source of friction being the mechanical idioms documented in CLAUDE.md (most relevantly: _root_.mul_assoc qualification when open NQubitPauliGroupElement is in scope, change step before rw [one_mul, mul_one] in closure_induction proofs — but those don't even arise here since the centralizer proofs use Subgroup.forall_comm_closure_iff rather than closure_induction).

Potential mechanical friction points (not blockers, just heads-up)

1. EC Zoo tableau confusion. Stage-4 agents might be tempted to "verify" the stabilizer choice against the EC Zoo description, which quotes (XXII, IIXX, ZZZZ). As documented in informal_spec.md § "Stabilizer generators" — this is the dual of our chosen (ZZII, IIZZ, XXXX). The choice is dictated by the LNCY codewords (Eqs. 5–6) and the requirement that the chosen stabilizers stabilize those codewords. We have verified this in writing.

2. logicalZ = ZIZI vs IZIZ. Both are valid logical Z representatives (differ by ZZZZ = S_Z1·S_Z2 which is in the stabilizer). We pick ZIZI for symmetry with logicalX = XXII (both have support {0, 2}-style: actually logicalX has support {0, 1} and logicalZ has support {0, 2}; the only shared support qubit is qubit 0, where they anticommute, hence the anticommute-filter {0}). Stage 4 should not silently switch choices; if the skeleton's pinned choice doesn't close T14 or T19 cleanly, the right fix is to investigate why, not to change the logical operator.

3. Filter cardinalities for cross-type commutations (T13, T14):

   • logicalX = XXII vs S_Z1 = ZZII: anticommute filter {0, 1} (card 2).
   • logicalX = XXII vs S_Z2 = IIZZ: anticommute filter {} (card 0).
   • logicalZ = ZIZI vs S_X1 = XXXX: anticommute filter {0, 2} (card 2).
   • All three are even cardinality → commute. The empty-filter case is well-supported by pauli_comm_componentwise since when neither operator has X overlapping the other's Z, they commute componentwise.

4. Distance-2 lower bound only requires w = 1. The interval-case interval_cases w with 1 ≤ w < 2 reduces to the single case w = 1, which no_weight_one_mem_centralizer_of_anticommute_witness closes. There is no w = 2 lower-bound case (the bound is < d, and 2 ≮ 2). Less work than the [[5,1,3]] distance-3 case.

Progress log: [[4,1,2]] LNCY code (css_4_1_2)

Session 1 (2026-05-23)

• Starting sorries: 26 across 21 theorem statements (T1–T21).
• Budget: 8h, per-sorry 15min autoprove + 25min sorry-filler-deep.
• Plan order: T1 → T21 (per plan.md dependency graph).
• Reference template: Codes/Small/FourQubit_4_2_2.lean (same n, same CSS shape).

Setup

• Worktree mathlib symlink verified.
• Skeleton lake build confirmed: 26 declaration uses sorry warnings, no errors.
• Proof approach: direct edits driven by the FourQubit_4_2_2 template (mechanical adaptation, k=1 vs k=2; 2 Z-generators vs 1).

Batch 1 — T1 through T16 (typing, commutation, centralizer)

• T1 (ZGenerators_are_ZType): closed by rcases hg with rfl | rfl, per-generator fin_cases i <;> simp. First attempt missed NQubitPauliOperator.identity in the simp set — Lean reported NQubitPauliOperator.identity 4 2 = PauliOperator.I ∨ … was unsolved. Added NQubitPauliOperator.identity to the simp lemmas; closed.
• T2 (XGenerators_are_XType): same fix. (Note: later cleaned out the extra NQubitPauliOperator.identity here — linter.unusedSimpArgs flagged it because for X1 specifically all positions get overwritten by .set, so identity never appears in the residual goal.)
• T3 (S_Z1_comm_S_X1): pauli_comm_even_anticommutes + filter {0, 1}. Decided via decide.
• T4 (S_Z2_comm_S_X1): filter {2, 3}. Same pattern.
• T5 (generators_commute): standard rcases dispatch, 4 cases (Z×Z, Z×X, X×Z, X×X) routing to ZType_commutes, cross, XType_commutes.symm. Verbatim from [[4,2,2]] except Or.inl/Or.inr on the 2-Z generator list.
• T6 (negIdentity_not_mem): one-shot CSS.negIdentity_not_mem_closure_union.
• T7 (listToSet_generatorsList): simp only [...] + ext + final simp only. First attempt failed because the list has 3 elements and Set.mem_insert_iff unfolds left-associated ((a ∨ b) ∨ c), whereas Set.mem_union (ZGenerators ∪ XGenerators) after Set.mem_insert_iff unfolds right-associated (a ∨ (b ∨ c)). Added or_assoc to the final simp set to close.
• T8 (AllPhaseZero_generatorsList): nested AllPhaseZero_cons.mpr ⟨rfl, ...⟩ × 3. Used the explicit rw + refine ⟨rfl, ?_⟩ chain for clarity over the simpa shortcut.
• T9 (rowsLinearIndependent_generatorsList): by decide.
• T10 (GeneratorsIndependent_4_generatorsList): non-sorry — a term that uses T9 via GeneratorsIndependent_of_rowsLinearIndependent (in the skeleton already; no sorry to close).
• T11 (stabilizerGroup_toSubgroup_eq): simp only [...] + rw.
• T12 (logicalX_anticommutes_logicalZ): filter {0}, pauli_anticomm_odd_anticommutes.
• T13a-c (logicalX_commutes_S_{Z1,Z2,X1}):
  • vs S_Z1: filter {0, 1} (even).
  • vs S_Z2: pauli_comm_componentwise (no overlap with anticommute).
  • vs S_X1: pauli_comm_componentwise (both X-type).
• T14a-c (logicalZ_commutes_S_{Z1,Z2,X1}):
  • vs S_Z1: pauli_comm_componentwise (both Z-type).
  • vs S_Z2: pauli_comm_componentwise (both Z-type).
  • vs S_X1: filter {0, 2} (even).
• T15, T16 (logicalX/Z_mem_centralizer): StabilizerGroup.mem_centralizer_iff + forall_comm_closure_iff + rcases.

Status after batch 1: 16/26 closed, 10 remaining. Commit 5a4238a.

Batch 2 — T17/T18 + T19 helpers + T19 witness + T20 + T21

• T17 (stabilizerCode): non-sorry — structure literal already populated in the skeleton; the logical_commute_cross field uses Subsingleton.elim directly. Nothing to close here.
• T18 (stabilizerCode_toSubgroup_eq): change + rw. Same as the [[4,2,2]] template, verbatim.
• T19a (weightOneAt_anticomm_S_Z1): the trick is that the filter equality has to incorporate the hi : i = 0 ∨ i = 1 case-split inside the ext proof — at the call site we can't pick a specific concrete value for i since the lemma is universally quantified over i. Solution: do the rcases hi <;> rcases hP inside the filter-equality proof, between ext j and fin_cases j. The resulting case explosion (2 × 2 × 4 = 16 cases) is handled cleanly by simp.
• T19b (weightOneAt_anticomm_S_Z2): same shape, mirror of T19a.
• T19c (weightOneAt_Z_anticomm_S_X1): no hi constraint (Z·X anticommutes at every qubit), so the [[4,2,2]] template applies verbatim.
• T19 (weight_one_anticomm_witness): match on P, hP:
  • P = X / P = Y: pick S_Z1 or S_Z2 by i ∈ {0,1} vs i ∈ {2,3} dichotomy. Initial draft used by_cases hi : i = 0 ∨ i = 1 per branch; a small refactor pulled out the dichotomy as a single have hi_dichotomy : (i = 0 ∨ i = 1) ∨ (i = 2 ∨ i = 3) (closed by fin_cases i <;> tauto) reused across X and Y branches.
  • P = Z: pick S_X1.
  • P = I: contradiction from hP : P ≠ I.
• T20 (code_has_distance_two): verbatim from [[4,2,2]] using hasCodeDistance_of + IsNontrivialLogicalOperator_iff + no_weight_one_mem_centralizer_of_anticommute_witness. The (logicalOpsCSS_4_1_2 0).xOp_nontrivial invocation gives the weight-2 logicalX witness directly.
• T21 (stabilizerCodeWithDistance): non-sorry — structure literal bundling T17 + T20.

Cleanup pass: two linter.unusedSimpArgs warnings flagged the unused NQubitPauliOperator.identity simp argument in T2 and T19c (the simp set normalizes via .set chains, which fully overwrite the identity for those theorems). Removed both arguments — file now compiles with zero warnings.

Final whole-repo lake build: clean, all 3422 jobs succeed. No new warnings introduced anywhere.

Status after batch 2: 26/26 sorries closed (21/21 theorem statements). 0 BLOCKED. Final LoC = 505. Ready for PR.