Informal spec: iceberg [[2m, 2m−2, 2]] error-detecting code

Summary

The iceberg code family (a.k.a. generalized parity code, self-dual quantum parity-check code, or "[[2m, 2m−2, 2]] detection code") is a self-complementary, self-dual CSS stabilizer code on n = 2m physical qubits, encoding k = 2m − 2 logical qubits at distance d = 2. It detects (but does not correct) any single-qubit Pauli error.

The stabilizer is generated by exactly two operators: the all-X operator XX...X and the all-Z operator ZZ...Z, both acting on all 2m physical qubits. For m = 2 this is the [[4, 2, 2]] four-qubit code; for m = 3 it is the [[6, 4, 2]] code; in general it is the highest-rate distance-2 CSS code when an even number of qubits is used.

The "iceberg" name comes from the fact that each codeword |b̄⟩ is a sum of a "visible" basis state (an even-weight bitstring b) and an "invisible" basis state (its bitwise negation ¬b, which is also even-weight when n is even).

Parameters

• Physical qubits: n = 2m (parametric in m)
• Logical qubits: k = 2m − 2
• Distance: d = 2 (detects a single error; cannot correct)
• Family: CSS, self-dual (the X-stab and Z-stab share the same support)
• Parameter constraint: m ≥ 2. The m = 1 case would give a trivial [[2, 0, 2]] code with no logical qubits, which we exclude via [Fact (2 ≤ m)] (mirroring RotatedSurfaceCodeN's [Fact (3 ≤ L)]).
• Originally introduced in:
  • [Steane 1996, arxiv:quant-ph/9605021] (general CSS framework)
  • [Gottesman 1997, arxiv:quant-ph/9702029] (stabilizer-formalism analysis)
  • [Viola–Knill–Lloyd 1998, arxiv:quant-ph/9809071] (dynamical decoupling)

Source-availability note. The arxiv abstracts retrieved during Stage 2 do not provide explicit per-logical-qubit logical-operator formulas; only the two stabilizer generators are quoted directly from the EC Zoo entry. The logical-operator convention chosen below is derived by hand from first-principles symplectic commutation analysis, then cross-checked against the existing FourQubit_4_2_2.lean formalization for the m = 2 specialization (see § "Relation to FourQubit_4_2_2.lean" below). It is not directly quoted from any of the three references — the references specify the codeword basis (and stabilizers) but leave the logical-operator choice unspecified up to Clifford equivalence (any maximal set of weight-2 operators in the centralizer that pairwise (anti)commute correctly is a valid logical basis).

Stabilizer generators

Exactly two generators, n − k = 2m − (2m − 2) = 2:

S_X := X X X ... X   (X on every one of the 2m qubits, no I's)
S_Z := Z Z Z ... Z   (Z on every one of the 2m qubits, no I's)

In Lean notation:

def S_Z (m : ℕ) [Fact (2 ≤ m)] : NQubitPauliGroupElement (2 * m) :=
  ⟨0, NQubitPauliOperator.Z (2 * m)⟩

def S_X (m : ℕ) [Fact (2 ≤ m)] : NQubitPauliGroupElement (2 * m) :=
  ⟨0, NQubitPauliOperator.X (2 * m)⟩

These overlap at all 2m qubit positions (every X-pair anticommutes locally with the matching Z-pair). The count of anticommuting positions is 2m, which is even since 2m is even — so S_X and S_Z commute. This is the unique "iceberg constraint": the two full-support stabilizers commute precisely because the number of qubits is even.

Logical operators (k = 2m − 2 logicals)

We adopt the split-anchor convention:

• Qubits 0, 1, ..., 2m − 3 are the "individual logical" positions: logical qubit i (for i : Fin (2m − 2)) is anchored on physical qubit i.
• Qubit 2m − 2 is the "Z-anchor" (always part of every Z̄_i).
• Qubit 2m − 1 is the "X-anchor" (always part of every X̄_i).

For i : Fin (2m − 2):

X̄_i := X_i · X_{2m-1}      (X at qubits i and 2m-1, I elsewhere; weight 2)
Z̄_i := Z_i · Z_{2m-2}      (Z at qubits i and 2m-2, I elsewhere; weight 2)

In Lean:

def logicalX (m : ℕ) [Fact (2 ≤ m)] (i : Fin (2 * m - 2)) :
    NQubitPauliGroupElement (2 * m) :=
  ⟨0,
    ((NQubitPauliOperator.identity (2 * m)).set ⟨i.val, _⟩ PauliOperator.X)
      |>.set ⟨2 * m - 1, _⟩ PauliOperator.X⟩

def logicalZ (m : ℕ) [Fact (2 ≤ m)] (i : Fin (2 * m - 2)) :
    NQubitPauliGroupElement (2 * m) :=
  ⟨0,
    ((NQubitPauliOperator.identity (2 * m)).set ⟨i.val, _⟩ PauliOperator.Z)
      |>.set ⟨2 * m - 2, _⟩ PauliOperator.Z⟩

(Index coercions Fin (2m - 2) ↪ Fin (2m) and explicit Fin constructions for 2m - 1 / 2m - 2 are populated by the Lean skeleton; see gap_audit.md for the Fin machinery used.)

By-hand verification of the (anti)commutation table

For Pauli operators P = ⟨0, p⟩ and Q = ⟨0, q⟩ with phase 0, the "number of qubits where they anticommute" is the cardinality of {i | (p i, q i) ∈ {(X,Z), (Z,X), (X,Y), (Y,X), (Y,Z), (Z,Y)}}. They commute iff this cardinality is even. (See NQubitPauliGroupElement.commutes_iff_even_anticommutes.)

Stabilizer commutation (sanity, already used to motivate n = 2m):

Logical–stabilizer commutation:

So every logical operator is in the centralizer of the stabilizer.

Logical pairwise (anti)commutation:

(*) For i ≠ j, both indices are in {0, ..., 2m−3}, neither equals 2m−2 nor 2m−1. So X̄_i's support {i, 2m−1} is disjoint from Z̄_j's support {j, 2m−2}: no anticommuting Pauli pair anywhere. Therefore commute.

The diagonal-anticommutation count of 1 (odd) for X̄_i · Z̄_i is the key fact: the anticommuting position is precisely qubit i (since both operators have non-identity Pauli there, and X anticommutes with Z), while at the anchor positions only one operator has non-identity Pauli (qubit 2m−1: only X̄_i; qubit 2m−2: only Z̄_i). Hence the anticommuting set is exactly {i}, cardinality 1, odd ⇒ anticommute. ✓

Why the X-anchor and Z-anchor are different qubits

If both anchors were the same qubit (say 2m−1), then X̄_i · Z̄_i would anticommute at both qubit i and qubit 2m−1 (count 2, even ⇒ commute) — contradicting the required diagonal anticommutation. Splitting the anchors across the two "extra" qubits gives the unique anticommuting position at qubit i, satisfying the diagonal anticommutation.

Why this differs from FourQubit_4_2_2.lean (m = 2 case)

For m = 2 (n = 4, k = 2), our convention yields:

X̄_0 = X I I X  (qubits 0 and 3)
X̄_1 = I X I X  (qubits 1 and 3)
Z̄_0 = Z I Z I  (qubits 0 and 2)
Z̄_1 = I Z Z I  (qubits 1 and 2)

The existing FourQubit_4_2_2.lean formalization uses a different logical basis (per its file header):

X̄_1 = I X I X   (qubits 1 and 3)
X̄_2 = I I X X   (qubits 2 and 3)
Z̄_1 = I I Z Z   (qubits 2 and 3)
Z̄_2 = I Z I Z   (qubits 1 and 3)

Both bases describe the same code (the same stabilizer subgroup, hence the same code subspace), but the choice of logical-operator labels and supports is different. They are equivalent under a Clifford on the logical qubits — i.e., the two formalizations describe the same physical code but with different "logical basis" choices.

Per the agent spec, we do NOT prove equivalence here. The parametric iceberg family at m = 2 and FourQubit_4_2_2.lean coexist as separate formalizations, mirroring the RepetitionCode3.lean / RepetitionCodeN.lean relationship (where RepetitionCode3 is a special hand-tuned n = 3 instance and RepetitionCodeN is the parametric n + 2 family; both prove distance 1 and the resulting StabilizerCode objects are not lifted into each other).

The two conventions are linked by the index relabeling (i_iceberg, j_4_2_2) = (0, 1) ↔ (1, 2) plus a Clifford swap on the anchor structure; we leave this lift as future work (research-track, not engineering-track).

Codespace

The code subspace is the simultaneous +1 eigenspace of S_X and S_Z. Following the EC Zoo description:

Each codeword is a superposition of a computational basis state labeled by an even-weight bitstring b and a state labeled by the negation of b.

A logical basis state |b̄⟩ (where b ∈ {0,1}^(2m−2) indexes the logical register) can be written as

|b̄⟩ = (1/√2)( |b · c_Z(b) · c_X(b)⟩ + |¬b · ¬c_Z(b) · ¬c_X(b)⟩ )

where c_Z(b) ∈ {0, 1} is the parity of b (chosen so total bitstring has even weight, making S_Z act as +1) and c_X(b) is determined by the remaining even-weight constraint. The exact formula is not needed in the formalization (it would only feed a "codespace dimension = 2^k" theorem, which we do not prove directly — instead, the dimension follows from generators_independent plus the 2^(n−k) index theorem).

Theorems to formalize

The skeleton's theorem set follows _TEMPLATE.lean's §1–§14 layout, parametrized over m.

T1: Z-generator is Z-type

For every g in {S_Z m}, IsZTypeElement g. (Trivial: case-split on the singleton, apply IsZTypeElement definition with PauliOperator.IsZType holding at every qubit because S_Z is the all-Z operator.) [Source: derived from the all-Z definition; conceptually trivial.]

T2: X-generator is X-type

For every g in {S_X m}, IsXTypeElement g. (Trivial, mirrors T1.)

T3: Cross-commutation S_Z · S_X = S_X · S_Z

The all-Z and all-X operators on 2m qubits commute (anticomm count = 2m, even). The cleanest proof is pauli_comm_even_anticommutes followed by reducing the filter to Finset.univ (count 2m) and applying Nat.even_two_mul or directly proving Even (2 * m). Alternative: extract the commutes_of_pauli_inner_zero style proof from symplecticInner_X_Z = (2m mod 2 = 0). [Source: standard CSS commutation. The structurally cleanest form uses NQubitPauliOperator.symplecticInner evaluation at the all-X / all-Z operators on even n; analogue of allX_allZ_anticommute but with the parity reversed.]

T4: All generators commute pairwise

∀ g h ∈ generators m, g * h = h * g. Follows from T1, T2, T3 via CSSCommutationLemmas.ZType_commutes / XType_commutes.

T5: −I ∉ subgroup

The closure of {S_X m, S_Z m} does not contain the negative-identity element. Standard CSS argument via CSS.negIdentity_not_mem_closure_union, consuming T1, T2, T3.

T6: Generator list / set equality

listToSet generatorsList = generators m. Direct unfolding via listToSet_cons / listToSet_nil. The generator list is [S_Z m, S_X m] (length 2 = n − k).

T7: Phase-zero generators

AllPhaseZero generatorsList. Trivial: both generators have phase 0.

T8: Generator independence (linear independence of check-matrix rows)

The two check-matrix rows for S_Z m and S_X m are linearly independent over ZMod 2. The check matrix of [S_Z m, S_X m] has shape 2 × 4m; the first row is (0 ... 0, 1 ... 1) (zeros on the X-part, ones on the Z-part), and the second row is (1 ... 1, 0 ... 0). These are independent since neither row is a scalar multiple of the other (the only nonzero combinations to consider are themselves, and 0 ≠ ones on both halves). Parametric proof needed: cannot decide because m is symbolic. Likely unfolds into a finite case analysis on the 2 × 2 coefficient matrix in (ZMod 2).

T9: Bundled StabilizerGroup (2 * m)

Standard mkStabilizerFromGenerators packaging, consuming T4 and T5.

T10: stabilizerGroup_toSubgroup_eq

Bridge between stabilizerGroup.toSubgroup and the Subgroup.closure generators m definition. Standard, mirrors RepetitionCodeN.

T11: Logical X anticommutes Logical Z (diagonal)

For every i : Fin (2m − 2), Anticommute (logicalX m i) (logicalZ m i). Anticomm support is {i.val} in Finset (Fin (2m)) — cardinality 1, odd. Use pauli_anticomm_odd_anticommutes plus a parametric filter-equality proof. This is the heart of the parametric proof — see plan.md §"Per-theorem proof sketch / T11".

T12: Logical operators commute pairwise (off-diagonal)

For every i j : Fin (2m − 2):

• T12a: logicalX m i · logicalX m j = logicalX m j · logicalX m i (both X-type, trivial).
• T12b: logicalZ m i · logicalZ m j = logicalZ m j · logicalZ m i (both Z-type, trivial).
• T12c (i ≠ j): logicalX m i · logicalZ m j = logicalZ m j · logicalX m i. Anticomm support is empty (disjoint supports), so commute.

T13: Logical X in centralizer (parametric)

For every i : Fin (2m − 2), logicalX m i ∈ centralizer (stabilizerGroup m). Reduces via Subgroup.forall_comm_closure_iff to showing logicalX m i commutes with each of the two generators S_Z m and S_X m:

• vs. S_X m: both X-type, commute (via XType_commutes or pauli_comm_componentwise).
• vs. S_Z m: anticomm at {i.val, 2m - 1}, count 2, even ⇒ commute.

T14: Logical Z in centralizer (parametric)

For every i : Fin (2m − 2), logicalZ m i ∈ centralizer (stabilizerGroup m). Symmetric to T13: vs. S_Z m both Z-type commute; vs. S_X m anticomm at {i.val, 2m - 2}, count 2, even ⇒ commute.

T15: StabilizerCode (2 * m) (2 * m - 2) packaging

Bundle T6–T14 plus the off-diagonal commutation T12 to produce the StabilizerCode structure. The logical_commute_cross field uses the "all four off-diagonal pairs commute" pattern from FourQubit_4_2_2.lean generalized over the Fin (2m − 2) × Fin (2m − 2) index space.

T16: stabilizerCode_toSubgroup_eq

Bridge for the distance proof: stabilizerCode.toStabilizerGroup.toSubgroup = Subgroup.closure (generators m). Standard change + unfold.

T17: Weight-1 anticommute witness

The key lemma feeding the distance proof. For every qubit i : Fin (2m) and every non-identity PauliOperator P, there exists g ∈ generators m such that Anticommute (weightOneAt i P) g. The "easy" case:

• If P = X or P = Y: weight-1 element has non-Z at qubit i, anticommutes with the all-Z stabilizer S_Z m at qubit i (single anticomm position, odd ⇒ anticommute).
• If P = Z: weight-1 element has Z at qubit i, anticommutes with the all-X stabilizer S_X m at qubit i (single anticomm position, odd ⇒ anticommute).

No dichotomy needed (unlike CSS_4_1_2.lean): every qubit is "covered" by both S_X and S_Z (full-support stabilizers), so the witness choice depends only on P, not on i.

T18: code_has_distance_two : HasCodeDistance stabilizerCode 2

Uses the PR #34 helper hasCodeDistance_two_of_anticommute_witness:

theorem code_has_distance_two (m : ℕ) [Fact (2 ≤ m)] :
    HasCodeDistance (stabilizerCode m) 2 :=
  hasCodeDistance_two_of_anticommute_witness (stabilizerCode m)
    (generators m)
    (stabilizerCode_toSubgroup_eq m)
    (weight_one_anticomm_witness m)
    ⟨logicalX m ⟨0, ...⟩, ..., by ...⟩

The witness for the "exists weight-2 nontrivial logical" requirement is logicalX m 0 (which has weight exactly 2: X at qubits 0 and 2m - 1). weight (logicalX m 0) = 2 requires a small parametric weight computation; see gap_audit.md for the issue and the planned approach.

T19: StabilizerCodeWithDistance (2 * m) (2 * m - 2) 2 packaging

Trivial wrapper from T15 + T18.

Edge cases / convention notes

1. m = 1 excluded. Without [Fact (2 ≤ m)], k = 2m - 2 = 0 and the StabilizerCode would have zero logical qubits, making Fin k = Fin 0 empty and the logical-operator universe vacuous. The theorems all still typecheck at m = 1 but become vacuously true; we exclude this case to keep the [[2m, 2m−2, 2]] parameter table meaningful and to avoid Nat.sub underflow when computing 2m - 2 for m = 1.

2. 2m - 2 and 2m - 1 use Nat.sub. Since m ≥ 2, both 2m - 2 ≥ 2 and 2m - 1 ≥ 3, so the subtraction is well-defined. We will need explicit Fin constructions ⟨2 * m - 1, by omega⟩ and ⟨2 * m - 2, by omega⟩ in the Lean code. The [Fact (2 ≤ m)] hypothesis discharges these bound proofs via omega. Mirror approach: see RepetitionCode/N.lean's use of Fin.castSucc / Fin.succ for n + 1 / n + 2 indexing (different approach, but same flavor of "construct a Fin from a parameter computation").

3. 0-based qubit indexing throughout. Matches the rest of the repo (Steane7.lean, FourQubit_4_2_2.lean, etc.).

4. Phase conventions. All generators and logical operators have phasePower = 0. No logical Y is defined in the skeleton (optional per _TEMPLATE.lean §10).

5. Distance proof method: hasCodeDistance_two_of_anticommute_witness (PR #34). This is the canonical closer for distance-2 CSS codes and was added to the framework specifically to avoid the interval_cases w; rcases ...; exact boilerplate that every distance-2 formalization was instantiating verbatim. The witness function (T17 above) is straightforward because both stabilizers have full support — no need for the hi_dichotomy pattern from CSS_4_1_2.lean.

6. Connection to existing repo abstractions: the iceberg [[2m, 2m−2, 2]] parametric family is the first generalized parametric CSS code with k > 2 logical qubits. The k-many off-diagonal logical commutations (T12) and the centralizer membership (T13, T14) are the first uses of parametric Fin k indexing for logicals in this repo. Test of the LogicalQubitOps API at scale.

Relation to existing repo files

Formalization plan: iceberg [[2m, 2m−2, 2]]

Strategy summary

The iceberg family has the simplest possible CSS structure (two generators: S_X = XX..X, S_Z = ZZ..Z) and falls into the parametric CSS bucket (parameter m, parameter constraint [Fact (2 ≤ m)]). The skeleton mirrors FourQubit_4_2_2.lean for the per-generator and per-logical-operator proofs, and lifts the indexing into a Fin (2m − 2)-indexed family for the logical operators. The distance proof rides on the PR #34 helper hasCodeDistance_two_of_anticommute_witness from CSSDistance.lean.

The single new ingredient over the existing parametric repository is the parametric weight-1 anticommute witness and the parametric all-X / all-Z commutation for even n (the iceberg-specific n = 2m constraint is what makes the two stabilizers commute, which fails for the odd-n case used by Steane7 / Shor9 / Repetition3).

Theorem dependency graph

T1 (Z-type S_Z) ───┐
                   ├─→ T4 (all pairs commute) ──┐
T2 (X-type S_X) ───┤                            ├─→ T5 (-I not in S)
                   │                            │
T3 (S_Z S_X comm) ─┘                            └─→ T9 (StabilizerGroup)

T6 (listToSet) ─→ T9 ─→ T10 (toSubgroup_eq)

T7 (phase 0)   ─→ T15 (StabilizerCode)
T8 (independence) ─→ T15
T9, T10        ─→ T13, T14 (logicals in centralizer)
                 └─→ T15

T11 (logical X anticomm Z, diag) ─→ T15
T12 (logical off-diag commutation) ─→ T15

T15 ─→ T16 (stabilizerCode_toSubgroup_eq)
T15, T17 (anti-witness) ─→ T18 (HasCodeDistance 2)
T15, T18 ─→ T19 (StabilizerCodeWithDistance)

Per-theorem proof sketch

T1 (Z-type predicate for S_Z m)

intro g hg
rcases (by simpa [ZGenerators] using hg) with rfl
refine ⟨rfl, ?_⟩
intro i
exact Or.inr (by simp [S_Z, NQubitPauliOperator.Z, PauliOperator.IsZType])

The NQubitPauliOperator.Z (2*m) operator is the constant function fun _ => Z, so the per-qubit PauliOperator.IsZType (Z) is trivial.

• Approach: direct unfold.
• Difficulty: trivial.

T2 (X-type predicate for S_X m)

Mirror of T1, swap Z ↔ X.

T3 (S_Z m and S_X m commute)

The interesting parametric proof. Two approaches:

Approach A (preferred): direct pauli_comm_even_anticommutes. The filter is Finset.univ (every qubit anticommutes), cardinality 2m, which is even via Nat.even_two_mul.

private lemma S_Z_comm_S_X (m : ℕ) [Fact (2 ≤ m)] : S_Z m * S_X m = S_X m * S_Z m := by
  classical
  pauli_comm_even_anticommutes
  have hfilter :
      (Finset.univ.filter
        (NQubitPauliGroupElement.anticommutesAt (n := 2 * m)
          (S_Z m).operators (S_X m).operators)) = (Finset.univ : Finset (Fin (2 * m))) := by
    ext i
    simp [Finset.mem_filter, NQubitPauliGroupElement.anticommutesAt,
      S_Z, S_X, NQubitPauliOperator.Z, NQubitPauliOperator.X, PauliOperator.mulOp]
  rw [hfilter, Finset.card_univ, Fintype.card_fin]
  exact ⟨m, by ring⟩

Approach B: lift the existing allX_allZ_anticommute framework. In SymplecticInner.lean:106, the all-X / all-Z anticommutation theorem states "Odd n ⇒ anticommute". The natural dual ("Even n ⇒ commute") might already be derivable but doesn't seem to be stated directly. We could add a allX_allZ_commute_of_even lemma to SymplecticInner.lean, but this is a separate cleanup; Approach A is self-contained.

• Approach: filter-equals-univ + even-via-2m.
• Difficulty: standard. Estimated ~10 LoC.

T4 (all pairs commute)

Combines T1, T2, T3 via CSSCommutationLemmas.ZType_commutes and XType_commutes. Two-way rcases on Z-vs-X membership; 4 cases (2 trivial diag from CSS, 2 cross from T3 + symmetry).

• Difficulty: trivial after T1/T2/T3.

T5 (−I ∉ subgroup)

Standard CSS argument via CSS.negIdentity_not_mem_closure_union.

• Difficulty: trivial.

T6 (listToSet_generatorsList)

def generatorsList (m : ℕ) [Fact (2 ≤ m)] : List (NQubitPauliGroupElement (2 * m)) :=
  [S_Z m, S_X m]

lemma listToSet_generatorsList (m : ℕ) [Fact (2 ≤ m)] :
    listToSet (generatorsList m) = generators m := by
  simp only [generatorsList, generators, ZGenerators, XGenerators,
    NQubitPauliGroupElement.listToSet_cons, NQubitPauliGroupElement.listToSet_nil]
  ext g; simp only [...]

Same pattern as FourQubit_4_2_2.lean (which has [Z1, X1]).

• Difficulty: trivial.

T7 (AllPhaseZero)

Same pattern as FourQubit_4_2_2.lean. Both generators have phasePower = 0 by construction.

• Difficulty: trivial.

T8 (Generator independence — PARAMETRIC, this is the main risk)

The check matrix of [S_Z m, S_X m] is the 2 × 4m matrix

S_Z m | 0 0 ... 0 | 1 1 ... 1
S_X m | 1 1 ... 1 | 0 0 ... 0

We need linear independence of these two rows over ZMod 2. Two nontrivial linear combinations: each row alone (already nonzero), and their sum 1 1 ... 1 1 1 ... 1 (also nonzero). The 4 combinations are: {0, row₁, row₂, row₁+row₂}, three nonzero.

Proof approach: rowsLinearIndependent unfolds to "for all f : Fin 2 → ZMod 2, (∀ j, ∑ i, f i * checkMatrix i j = 0) → f = 0". For our two-row case, the columns split as:

• Columns 0 to 2m−1 (X-part): only row 2 (S_X) contributes, so the per-column constraint is f 1 * 1 = 0, forcing f 1 = 0.
• Columns 2m to 4m−1 (Z-part): only row 1 (S_Z) contributes, so the per-column constraint is f 0 * 1 = 0, forcing f 0 = 0.

So both coefficients must vanish — independence holds. Implementation:

theorem rowsLinearIndependent_generatorsList (m : ℕ) [Fact (2 ≤ m)] :
    NQubitPauliGroupElement.rowsLinearIndependent (generatorsList m) := by
  unfold NQubitPauliGroupElement.rowsLinearIndependent
  rw [Fintype.linearIndependent_iff]
  intro f hf i
  -- Specialize hf at an X-column (e.g. Fin.castAdd m 0) to get f 1 = 0
  -- Specialize hf at a Z-column (e.g. Fin.natAdd (2*m) 0) to get f 0 = 0
  -- Then fin_cases i; assumption / exact h_X / exact h_Z
  sorry

Could possibly be closed by decide if we manage to specialize to a concrete m first, but since m is symbolic, we need a parametric argument. Estimated effort: ~30–50 LoC (the more complex parametric proof in the file).

• Approach: hand-rolled per-column specialization (no induction needed because there are only 2 rows).
• Difficulty: standard. The parametric flavor is the only friction; the actual math is simpler than RepetitionCode/N.lean's 3-band argument.
• Risk: needs Fin.natAdd / Fin.castAdd discipline for indexing.

T9, T10 (StabilizerGroup packaging)

Standard mkStabilizerFromGenerators invocation. Mirror RepetitionCodeN.lean:388–395.

• Difficulty: trivial.

T11 (logical X anticomm logical Z, diagonal)

For each i : Fin (2m − 2):

theorem logicalX_anticommutes_logicalZ_diag (m : ℕ) [Fact (2 ≤ m)]
    (i : Fin (2 * m - 2)) :
    Anticommute (logicalX m i) (logicalZ m i) := by
  classical
  pauli_anticomm_odd_anticommutes
  -- Goal: Odd ((Finset.univ.filter (anticommutesAt ...)).card)
  -- Show filter = {⟨i.val, by omega⟩} (the qubit-i index lifted into Fin (2m))
  have hfilter :
      (Finset.univ.filter
        (NQubitPauliGroupElement.anticommutesAt (n := 2 * m)
          (logicalX m i).operators (logicalZ m i).operators)) =
        ({⟨i.val, by omega⟩} : Finset (Fin (2 * m))) := by
    ext j
    -- Per-qubit analysis: anticommute at qubit j iff j = i-as-Fin(2m)
    -- Three positions matter:
    --   - j = i (lifted): X vs Z, anticommute
    --   - j = 2m-1: X vs I, commute
    --   - j = 2m-2: I vs Z, commute
    --   - else: I vs I, commute
    sorry
  rw [hfilter, Finset.card_singleton]; decide

The hfilter proof is the parametric meat. Need to do per-qubit case analysis without fin_cases (since m is symbolic). The approach is by_cases on the three "interesting" positions plus the general case, using Fin.ext_iff to compare values numerically.

• Approach: 4-case by_cases on the qubit's value being i, 2m-2, 2m-1, or "other".
• Difficulty: standard parametric (~25 LoC per logical (anti)comm). This proof shape appears 6 times (T11, T12c, T13×2 directions, T14×2), so a private helper pauli_overlap_at_pair_set would amortize.
• Risk: Fin.ext reasoning on 2m - 1 and 2m - 2 can trip up simp. Workaround: omega after Fin.ext_iff.

T12 (logical pairwise commutation)

• T12a (X̄_i · X̄_j): both X-type, use XType_commutes / pauli_comm_componentwise. Trivial.

• T12b (Z̄_i · Z̄_j): dual of T12a. Trivial.

• T12c (X̄_i · Z̄_j for i ≠ j): anticomm support is empty, so commute. Proof: filter equals ∅, cardinality 0, even.

  The subtlety: we need i ≠ j ⇒ (i : Fin (2m)) ≠ (j : Fin (2m)) (when lifting Fin (2m−2) ↪ Fin (2m)). This follows from the lift being injective — write the lift as Fin.castLE (with the bound proof) and use Fin.castLE_injective.

  theorem logicalX_commutes_logicalZ_offdiag (m : ℕ) [Fact (2 ≤ m)]
      {i j : Fin (2 * m - 2)} (hij : i ≠ j) :
      logicalX m i * logicalZ m j = logicalZ m j * logicalX m i := by
    classical
    pauli_comm_even_anticommutes
    have hfilter : (Finset.univ.filter
        (anticommutesAt (logicalX m i).operators (logicalZ m j).operators))
        = (∅ : Finset (Fin (2 * m))) := by
      ext k; simp [Finset.mem_filter, anticommutesAt, logicalX, logicalZ, ...]
      -- Per-qubit case analysis: no anticomm at any qubit because supports
      -- are disjoint when i ≠ j (and i, j < 2m-2).
      sorry
    rw [hfilter, Finset.card_empty]
    exact even_zero
  

• Difficulty: T12a/b trivial, T12c standard parametric (similar shape to T11 but with empty filter).

T13, T14 (logicals in centralizer)

Standard pattern from FourQubit_4_2_2.lean:384: rewrite via StabilizerGroup.mem_centralizer_iff_closure, intro s ∈ generators, case-split on Z- or X-gen, dispatch via per-generator commutation lemma.

The per-generator commutation lemmas are:

• logicalX_commutes_S_Z m i: logicalX m i * S_Z m = S_Z m * logicalX m i. Anticomm support {i, 2m-1}, count 2, even ⇒ commute. (Parametric.)

• logicalX_commutes_S_X m i: logicalX m i * S_X m = S_X m * logicalX m i. Both X-type, trivial via XType_commutes.

• logicalZ_commutes_S_Z m i: both Z-type, trivial.

• logicalZ_commutes_S_X m i: anticomm support {i, 2m-2}, count 2, even ⇒ commute. (Parametric.)

• Difficulty: parametric but mechanical (~15 LoC × 2 each).

T15 (StabilizerCode packaging — the k = 2m-2 novelty)

The logical_commute_cross field requires a fin_cases ℓ <;> fin_cases ℓ' expansion. Cannot literally fin_cases over Fin (2m − 2) because m is symbolic. Instead, use if hℓ : ℓ = ℓ' then exact (hne hℓ).elim else [per-case commutations]. The per-case commutations (T12a, T12b, T12c, and T12c flipped) are then applied unconditionally — they don't depend on specific ℓ, ℓ' values, only on ℓ ≠ ℓ'.

private def logicalOpsIceberg (m : ℕ) [Fact (2 ≤ m)] :
    Fin (2 * m - 2) → LogicalQubitOps (2 * m) (stabilizerGroup m) :=
  fun i => ⟨logicalX m i, logicalZ m i,
            logicalX_mem_centralizer m i, logicalZ_mem_centralizer m i,
            logicalX_anticommutes_logicalZ_diag m i⟩

noncomputable def stabilizerCode (m : ℕ) [Fact (2 ≤ m)] :
    StabilizerCode (2 * m) (2 * m - 2) where
  hk := by have : Fact (2 ≤ m) := inferInstance; omega
  -- (... usual fields with parametric proofs from T6-T14 ...)
  logicalOps := logicalOpsIceberg m
  logical_commute_cross := fun ℓ ℓ' hne => by
    -- Cannot fin_cases on Fin (2m - 2) symbolically.
    -- Instead, apply T12 unconditionally.
    refine ⟨?_, ?_, ?_, ?_⟩
    · exact logicalX_commutes_logicalX m ℓ ℓ'  -- T12a (always commutes)
    · exact logicalX_commutes_logicalZ_offdiag m hne  -- T12c (i ≠ j)
    · exact (logicalX_commutes_logicalZ_offdiag m (Ne.symm hne)).symm  -- T12c flipped
    · exact logicalZ_commutes_logicalZ m ℓ ℓ'  -- T12b (always commutes)

• Difficulty: standard once T11-T14 are in place. The fin_cases problem is sidestepped by stating T12a/b as "for all i j" (no i ≠ j hypothesis), and T12c as "for i ≠ j" (with the hne hypothesis). See "Risk register" below for an alternative.

T16 (stabilizerCode_toSubgroup_eq)

Trivial change + rw [listToSet_generatorsList]. Mirror FourQubit_4_2_2.lean:472.

T17 (weight-1 anti-witness — parametric)

private lemma weight_one_anticomm_witness (m : ℕ) [Fact (2 ≤ m)] :
    ∀ i : Fin (2 * m), ∀ P : PauliOperator, P ≠ PauliOperator.I →
      ∃ g ∈ generators m, NQubitPauliGroupElement.Anticommute
        (weightOneAt i P) g := by
  intro i P hP
  match P, hP with
  | PauliOperator.X, _ =>
    exact ⟨S_Z m, by simp [generators, ZGenerators],
      weightOneAt_X_anticomm_S_Z m i⟩
  | PauliOperator.Y, _ =>
    exact ⟨S_Z m, by simp [generators, ZGenerators],
      weightOneAt_Y_anticomm_S_Z m i⟩
  | PauliOperator.Z, _ =>
    exact ⟨S_X m, by simp [generators, XGenerators],
      weightOneAt_Z_anticomm_S_X m i⟩
  | PauliOperator.I, hP => exact (hP rfl).elim

with three private helpers:

• weightOneAt_X_anticomm_S_Z m i: weight-1 X at qubit i vs. all-Z S_Z. Anticomm support is {i} (X·Z anticommute at qubit i; everywhere else the weight-1 element has I, commute). Single qubit, odd ⇒ anticommute.
• weightOneAt_Y_anticomm_S_Z m i: weight-1 Y at qubit i vs. all-Z S_Z. Same structure (Y·Z anticommute).
• weightOneAt_Z_anticomm_S_X m i: weight-1 Z at qubit i vs. all-X S_X. Symmetric.

Each is the parametric version of FourQubit_4_2_2.lean's weightOneAt_anticomm_Z1 (lines 480–495). The proof shape is identical; the only change is the filter equality, which needs a per-qubit by_cases j = i instead of fin_cases j (since m symbolic).

• Difficulty: standard parametric (~15 LoC each, 3 helpers).
• No hi_dichotomy needed (cleaner than CSS_4_1_2.lean).

T18 (HasCodeDistance 2 — one-liner via PR #34 helper)

theorem code_has_distance_two (m : ℕ) [Fact (2 ≤ m)] :
    HasCodeDistance (stabilizerCode m) 2 :=
  hasCodeDistance_two_of_anticommute_witness (stabilizerCode m)
    (generators m)
    (stabilizerCode_toSubgroup_eq m)
    (weight_one_anticomm_witness m)
    ⟨logicalX m ⟨0, by have : Fact (2 ≤ m) := inferInstance; omega⟩,
      (logicalOpsIceberg m _).xOp_nontrivial,
      ?_⟩

The ?_ is weight (logicalX m ⟨0, _⟩) = 2. This is parametric weight 2 (not decide-able for symbolic m). Need a weight_logicalX lemma.

• Difficulty: standard once the weight-2 helper is in place. Estimated 10 LoC for the helper, 5 LoC for the use.
• Risk: parametric weight computation may be fiddly; see gap_audit.md.

T19 (StabilizerCodeWithDistance packaging)

Trivial wrapper.

Risk register

1. Parametric weight computation (T18 witness). For symbolic m, the weight of logicalX m 0 (X at two qubits, identity elsewhere) equals 2. Need a weight_setIdentity_set_set style lemma or a direct computation. Likely candidate: NQubitPauliOperator.weight_set_set showing weight ((identity n).set i P |>.set j Q) = (1 if P ≠ I else 0) + (1 if Q ≠ I else 0) when i ≠ j. May not exist yet; if not, write the proof inline.

2. Fin (2m - 2) lift to Fin (2m). Need a clean coercion. Two approaches:

   • Fin.castLE (Nat.sub_le _ _) — works for 2m - 2 ≤ 2m.
   • ⟨i.val, by omega⟩ — explicit construction.

   Either is fine; the second is more explicit and grep-able.

3. Fin (2 * m - 2) itself is awkward. Lean's Fin (2 * m - 2) works fine when m ≥ 2, but Fin.cases / fin_cases won't reduce symbolically. All proofs over this index must avoid fin_cases — instead, use Fin.ext_iff to compare Fin values numerically and omega to discharge bounds. This is the same discipline as RotatedSurfaceCodeN.lean and RepetitionCode/N.lean.

4. logical_commute_cross field with parametric Fin k. Cannot fin_cases ℓ, so the proof has to work by structure. Mitigation strategy: state T12a and T12b "always commute" (no i ≠ j hypothesis, trivially derived from X-type / Z-type structure), state T12c "for i ≠ j" (with the hne carry). Then the logical_commute_cross field is just refine ⟨T12a, T12c, T12c.symm, T12b⟩.

5. Independence parametric proof (T8). This is the longest part of the file. Mitigation: it's structurally simpler than RepetitionCode/N.lean because there are only 2 rows; the per-column specialization is direct.

6. Module orphan trap. Need to add Iceberg.lean umbrella and import from Codes.lean. Both edits required; without them the file would silently never be compiled.

7. Stage-3 SKIPPED. Per the task spec: "The user is running this end-to-end without human review. Your informal_spec.md MUST be self-sufficient." The above logical-operator convention has been verified by hand (see informal_spec.md § "By-hand verification of the (anti)commutation table") and cross-checked against the m = 2 specialization. The papers do not specify a canonical logical basis (verified by direct WebFetch); the choice is documented as a deliberate convention with full justification.

Estimated effort

• LoC: ~500 total (matches the scoring estimate). Breakdown:
  • Imports + header: 30
  • Generators + sets (§1–§2): 30
  • Type predicates (§3, T1–T2): 30
  • Cross-commutation (§4, T3): 25
  • All-pair commutation (§5, T4): 20
  • −I lemma (§6, T5): 10
  • Generator list + phase 0 (§7, T6, T7): 30
  • Independence (§9, T8): 50 (main parametric proof; biggest risk)
  • StabilizerGroup (§8, T9, T10): 25
  • Logical operators (§10): 25
  • Logical anticommutation (§11, T11, T12): 80 (k = 2m-2 family, 4 cases)
  • Logical centralizer (§12, T13, T14): 80 (per-generator commutation, 4 helpers)
  • StabilizerCode packaging (§13, T15): 50
  • Distance bridge + witness (§14, T16, T17): 40
  • HasCodeDistance + packaging (T18, T19): 15
• Time: 2 sessions (one to close T1–T10, one for T11–T19).
• Proof attempts: the longest is T8 (independence) at ~30–50 LoC.

Reuse audit: iceberg [[2m, 2m−2, 2]]

Directly applicable (use as-is)

Pauli-group foundations

• NQubitPauliGroupElement n — QEC/Stabilizer/Foundations/PauliGroup/NQubitElement.lean.
• NQubitPauliOperator n, .identity n, .X n, .Z n, .set i P — QEC/Stabilizer/Foundations/PauliGroup/NQubitOperator.lean. The "all-X" and "all-Z" constructors are direct fits for the iceberg's full-support generators.
• PauliOperator.X, .Z, .Y, .I, .IsXType, .IsZType, .mulOp — QEC/Stabilizer/Foundations/PauliGroupSingle/Operator.lean.

Commutation infrastructure

• pauli_comm_even_anticommutes tactic — Foundations/PauliGroup/CommutationTactics.lean. Reduces a commutation goal to "Even ((Finset.univ.filter anticommutesAt).card)". Used for T3 (stabilizer commutation), T11–T14 (logical commutations), T17 helpers (weight-1 anti-witnesses).
• pauli_anticomm_odd_anticommutes tactic — same file. Dual of above; reduces Anticommute to "Odd (... .card)". Used for T11 (logical X̄ anticomm logical Z̄).
• pauli_comm_componentwise [...] tactic — same file. Closes componentwise-commutation when generators have disjoint or matching Pauli supports. Useful for the trivial "X̄·X̄" and "Z̄·Z̄" cases of T12, and for "logical commutes with same-type stabilizer".
• commutes_of_componentwise_commutes — Foundations/PauliGroup/Commutation.lean.
• Anticommute predicate — Foundations/PauliGroup/Commutation.lean:233.
• anticommutesAt function — same file.

CSS predicates and lemmas

• IsZTypeElement, IsXTypeElement — Framework/Core/CSS/CSSPredicates.lean. Direct fit for T1, T2.
• CSSCommutationLemmas.ZType_commutes, .XType_commutes — Framework/Core/CSS/CSSCommutationLemmas.lean. Used for T4 (all-pair commutation) and inside the centralizer proofs for the trivial cases.
• CSS.negIdentity_not_mem_closure_union — Framework/Core/CSS/CSSNoNegI.lean. Direct fit for T5.

Stabilizer-code structure

• StabilizerGroup n, .toSubgroup, .is_abelian, .no_neg_identity — Framework/Core/Stabilizer/StabilizerGroup.lean.
• mkStabilizerFromGenerators n L h_comm h_no_neg — Framework/Core/Stabilizer/StabilizerCode.lean:62.
• centralizer S, .mem_centralizer_iff, .mem_centralizer_iff_closure — Framework/Core/Stabilizer/Centralizer.lean.
• Subgroup.forall_comm_closure_iff — Framework/Core/Stabilizer/SubgroupLemmas.lean.
• negIdentity n, .negIdentity_eq_minusOne, .negIdentity_ne_one — Foundations/PauliGroup/NQubitElement.lean.

Generator-list / symplectic plumbing

• NQubitPauliGroupElement.listToSet, .listToSet_cons, .listToSet_nil — Foundations/PauliGroup/NQubitElement.lean.
• NQubitPauliGroupElement.AllPhaseZero, .AllPhaseZero_cons, .AllPhaseZero_nil — same file. Used in T7.
• NQubitPauliGroupElement.rowsLinearIndependent — same file.
• GeneratorsIndependent, GeneratorsIndependent_of_rowsLinearIndependent — Framework/Core/Stabilizer/StabilizerCode.lean:42, 48. Used in T8.

Logical-operator structure

• LogicalQubitOps n S — Framework/Core/Logical/LogicalOperators.lean:189. The 5-field structure (xOp, zOp, x_mem_centralizer, z_mem_centralizer, anticommute) is the target of T15's logicalOps field.
• IsNontrivialLogicalOperator, LogicalQubitOps.xOp_nontrivial, .zOp_nontrivial — same file.

Code distance

• hasCodeDistance_two_of_anticommute_witness — Framework/Core/CSS/CSSDistance.lean:165 (NEW in PR #34). This is the canonical closer for T18. Saves ~5 LoC of interval_cases / rcases boilerplate that every distance-2 CSS code would otherwise reproduce.

  Signature:

  theorem hasCodeDistance_two_of_anticommute_witness {k : ℕ}
      (C : StabilizerCode n k)
      (genSet : Set (NQubitPauliGroupElement n))
      (h_closure : C.toStabilizerGroup.toSubgroup = Subgroup.closure genSet)
      (h_anticomm : ∀ i : Fin n, ∀ P : PauliOperator, P ≠ .I →
        ∃ g ∈ genSet, Anticommute (weightOneAt i P) g)
      (h_witness : ∃ g, IsNontrivialLogicalOperator g C.toStabilizerGroup ∧
        weight g = 2) :
      HasCodeDistance C 2
  

• no_weight_one_mem_centralizer_of_anticommute_witness — Framework/Core/CSS/CSSDistance.lean:32 (transitively used by the above; we do not call it directly).

• weightOneAt i P — Framework/Core/CSS/CSSDistance.lean:26. The parametric weight-1 element constructor used in T17.

• HasCodeDistance, hasCodeDistance_of — Framework/Core/Logical/CodeDistance.lean.

• StabilizerCodeWithDistance n k d — Framework/Core/Logical/CodeDistance.lean:81. Final packaging in T19.

Lightly adapted (existing pattern, new instance)

Generator structure (from FourQubit_4_2_2.lean)

• The [S_Z, S_X] two-generator pattern (one Z, one X, both full-support): copy from FourQubit_4_2_2.lean:174 (generatorsList := [Z1, X1]). Generalize the explicit 4 to 2 * m and the explicit .set 0/1/2/3 chains to NQubitPauliOperator.Z (2 * m) / NQubitPauliOperator.X (2 * m).

Z-type / X-type predicate proofs (from FourQubit_4_2_2.lean)

• ZGenerators_are_ZType pattern (FourQubit_4_2_2.lean:88–96): replace the singleton rcases hg with rfl and fin_cases i with a parametric intro i and direct PauliOperator.IsZType unfold on the constant Z (2*m) i = .Z.

Cross-commutation proof (T3, from FourQubit_4_2_2.lean:114)

The shape pauli_comm_even_anticommutes + filter equality is identical. The only difference: the filter equals Finset.univ (not a small explicit set like {0, 1, 2, 3}), and the cardinality is 2 * m, which is parametrically even.

Logical (anti)commutation proofs (from FourQubit_4_2_2.lean:245)

Each pauli_anticomm_odd_anticommutes/pauli_comm_even_anticommutes + filter-equality block from FourQubit_4_2_2.lean translates directly, with two changes:

1. Replace fin_cases i (in the filter ext proof) with parametric by_cases on the three "special" qubits (i-lifted, 2m-2, 2m-1) plus the general case.
2. The explicit small Finset (e.g. {3} or {1, 3}) becomes a parametric singleton {⟨i.val, _⟩} or empty ∅.

Logical-in-centralizer proofs (from FourQubit_4_2_2.lean:384)

Direct pattern reuse: mem_centralizer_iff_closure, intro s ∈ generators, rcases on Z/X-generator, dispatch via per-generator commutation lemma.

StabilizerCode packaging (from FourQubit_4_2_2.lean:447–467)

The logical_commute_cross 4-tuple is the only k = 2 → k > 2 generalization point. The fin_cases ℓ <;> fin_cases ℓ' from FourQubit_4_2_2.lean:459 cannot be replicated parametrically; replace with a single refine ⟨_,_,_,_⟩ that uses always-commute lemmas (T12a, T12b) and the conditional i ≠ j lemma (T12c). See plan.md § T15.

Distance proof (from FourQubit_4_2_2.lean:534)

theorem code_has_distance_two : HasCodeDistance stabilizerCode 2 :=
  hasCodeDistance_two_of_anticommute_witness stabilizerCode generators
    stabilizerCode_toSubgroup_eq weight_one_anticomm_witness
    ⟨logicalX_1, (logicalOps4_2_2 0).xOp_nontrivial, by decide⟩

Translates almost verbatim to the iceberg's parametric form, with by decide on the weight-2 fact replaced by a parametric weight computation.

Parametric proof discipline (from Codes/Repetition/N.lean,

Codes/Small/QuantumHamming.lean, Codes/RotatedSurface/N.lean)

• [Fact (2 ≤ m)] instance, mirroring [Fact (3 ≤ L)] in RotatedSurfaceCodeN.lean:48.
• Parametric noncomputable def stabilizerGroup (m : ℕ) [Fact ...], mirror RepetitionCodeN.lean:388.
• Per-row check-matrix decomposition for rowsLinearIndependent (T8), mirror RepetitionCodeN.lean:219.
• The Subgroup.forall_comm_closure_iff + intro s hs pattern for centralizer membership, mirror RepetitionCodeN.lean:398.

New per-code definitions

These have no direct analog in the repo and must be defined fresh:

• logicalX m i, logicalZ m i for i : Fin (2m - 2). The per-logical-qubit operators with Fin (2m-2) ↪ Fin (2m) lifting and the "X-anchor at qubit 2m-1, Z-anchor at qubit 2m-2" convention. Closest existing similar: FourQubit_4_2_2.lean:227, 231, 235, 239 (logicalX_1, logicalX_2, logicalZ_1, logicalZ_2) — but those are hand-tuned for m = 2 with explicit qubit indices.

• Parametric Fin (2m-2) → Fin (2m) coercion. Either Fin.castLE (by omega : 2m - 2 ≤ 2m) or explicit ⟨i.val, by have : Fact (2 ≤ m) := inferInstance; omega⟩. The explicit form is more readable in the skeleton; we'll prefer it.

• Parametric all-X / all-Z commutation lemma (T3). Could be moved later to Foundations/BinarySymplectic/SymplecticInner.lean as a dual to the existing allX_allZ_anticommute (which handles odd n). For now, keep it private inside the iceberg file; revisit in a separate cleanup PR.

• Parametric weight of weight-2 logical operator (T18 witness). The fact weight (logicalX m 0) = 2 for symbolic m. Could become a small generic helper NQubitPauliOperator.weight_set_set_of_ne showing weight ((identity n).set i P |>.set j Q) = (1 if P ≠ I) + (1 if Q ≠ I) when i ≠ j. Investigate whether a similar helper already exists during Stage 4.

• Parametric logicalOpsIceberg : Fin (2m-2) → LogicalQubitOps .... Mirror logicalOps4_2_2 : Fin 2 → LogicalQubitOps 4 ... from FourQubit_4_2_2.lean:438. The parametric form uses a single uniform fun i => ⟨logicalX m i, logicalZ m i, ...⟩ rather than the hand-matched match ℓ with | 0 => ... | 1 => ... from the m = 2 case.

Gap audit: iceberg [[2m, 2m−2, 2]]

Repo gaps (this code surfaces / requires new abstractions)

Gap 1: parametric "all-X commutes with all-Z when n is even" lemma

Status: missing in Foundations/BinarySymplectic/SymplecticInner.lean.

The current allX_allZ_anticommute (n : ℕ) (hn : Odd n) lemma (SymplecticInner.lean:106) gives the odd n anticommute fact. The dual "even n ⇒ commute" is needed for T3 (the iceberg stabilizer's whole existence depends on this fact: S_X · S_Z = S_Z · S_X precisely because n = 2m is even). It does not appear to exist anywhere in Foundations/.

Resolution path during Stage 4:

• Option A (preferred): prove the commutation inline in the iceberg file using pauli_comm_even_anticommutes + filter-equals-univ + the parametric evenness fact Even (2 * m). The proof is ~10 LoC.
• Option B (cleanup PR after iceberg lands): add a dual allX_allZ_commute_of_even (n : ℕ) (hn : Even n) : (⟨0, X n⟩ : ...) * (⟨0, Z n⟩ : ...) = (⟨0, Z n⟩ : ...) * (⟨0, X n⟩ : ...) lemma to SymplecticInner.lean. Then the iceberg's T3 becomes one line: allX_allZ_commute_of_even (2 * m) (by ⟨m, by ring⟩).

Recommend Option A for the initial PR (keeps the iceberg PR focused).

Gap 2: parametric weight-of-weight-2-Pauli lemma

Status: probably missing.

T18 needs weight (logicalX m 0) = 2 for symbolic m. The logical X is ((identity (2m)).set i X).set j X with i ≠ j (here i = 0 and j = 2m - 1). There may or may not be a generic weight_set_set_of_ne_of_both_nonI helper; needs investigation during Stage 4.

Possible candidate names to grep for first:

• weight_set
• weight_setIdentity
• weight_of_support
• NQubitPauliOperator.weight

Resolution path:

• If a helper exists, use it directly.
• If not, prove the weight inline by directly computing the support cardinality:

  have hsupp : (logicalX m 0).operators.support = {⟨0, _⟩, ⟨2*m - 1, _⟩} := by
    ext k; ... -- 4-case by_cases on k
  have : weight (logicalX m 0) = 2 := by
    rw [weight, NQubitPauliOperator.weight_eq_support_card, hsupp,
      Finset.card_insert_of_notMem (by ...), Finset.card_singleton]
  

  Cost: ~10 LoC.

Gap 3: Fin (2 * m - 2) ↪ Fin (2 * m) coercion clarity

Status: no clean reusable helper; explicit construction needed.

The lift i : Fin (2m - 2) to Fin (2m) is needed many times throughout the file (definition of logicalX, definition of logicalZ, every commutation-filter proof). Fin.castLE would work but requires the bound proof 2*m - 2 ≤ 2*m to be passed each time. An anonymous constructor ⟨i.val, by ...⟩ keeps the call sites short but obscures structure.

Decision: use a private abbreviation early in the file:

/-- Lift a logical-qubit index `Fin (2m-2)` into the physical-qubit index
`Fin (2m)`. -/
@[inline] private def logIdx {m : ℕ} [Fact (2 ≤ m)] (i : Fin (2 * m - 2)) :
    Fin (2 * m) :=
  ⟨i.val, by have : Fact (2 ≤ m) := inferInstance; omega⟩

This keeps each call site to logIdx i instead of either repeating the bound proof or invoking Fin.castLE with the bound proof as argument.

Note: this is an idiom, not a repo-wide gap — but worth flagging in case a similar pattern is later promoted to Geometry/.

Gap 4: parametric fin_cases for Fin (2 * m - 2)

Status: known limitation, no resolution needed.

fin_cases ℓ does not work on Fin (2 * m - 2) when m is symbolic. This affects T15's logical_commute_cross field: rather than the fin_cases ℓ <;> fin_cases ℓ' <;> exact ... pattern from FourQubit_4_2_2.lean:459, we use a structural refine ⟨_, _, _, _⟩ that consumes the always-commute T12a/T12b lemmas and the conditional T12c lemma. Same trick used in RepetitionCodeN.lean:443 (logical_commute_cross := fun ℓ ℓ' h => (h (Subsingleton.elim ℓ ℓ')).elim) — but that proof requires Subsingleton (Fin k) which only holds for k ≤ 1. The iceberg's k = 2m - 2 ≥ 2 violates that.

Resolution: spelled out in plan.md § T15. No new abstraction needed.

Mathlib gaps (lemmas not in mathlib v4.30)

None expected. The parametric proofs use only:

• Finset.univ.filter, Finset.card, Finset.card_singleton, Finset.card_empty, Finset.card_insert_of_notMem, etc. — all standard.
• Even, Nat.even_two_mul, even_two, Even.zero — standard.
• Fin.val_eq_val, Fin.ext, Fin.castLE — standard.
• Nat.sub arithmetic via omega — standard.
• simp +decide, pauli_comm_even_anticommutes — repo-local.

No new mathlib lemma is required.

Likely "BLOCKED(<reason>)" sorries

None anticipated. All theorems should close with current infrastructure

• the inline-proven parametric lemmas in the iceberg file. The risks are about LoC budget and proof-engineering effort, not about missing abstractions.

If something unexpected blocks Stage 4 — e.g., the pauli_comm_even_anticommutes tactic fails to specialize to Fin (2 * m) — the fallback is to prove the commutation directly via NQubitPauliGroupElement.commutes_iff_symplectic_inner_zero plus a hand computation. This is still a "no blocker" path; just more LoC.

Architectural / future-cleanup notes

1. Move allX_allZ_commute_of_even to SymplecticInner.lean in a follow-up PR (per Gap 1, Option B).

2. Move Fin (2m-2) ↪ Fin (2m) lift to Geometry/FinPeriodic.lean if subsequent parametric codes need similar lifts. Currently it's iceberg-specific; promote if a second use site appears.

3. Generalize hasCodeDistance_two_of_anticommute_witness to hasCodeDistance_d_of_anticommute_witnesses_le_d_minus_one in a future PR — for distance-3+ codes the helper currently only handles d = 2. This is out of scope for iceberg (it's a d = 2 code), but noting for the next non-CSS code in the queue.

4. pauli_comm_componentwise extension: the current tactic handles componentwise commutation when supports are disjoint or identical. For the off-diagonal logical commutation T12c (where X̄_i and Z̄_j have disjoint supports when i ≠ j), this tactic might already close the goal in one line — investigate during Stage 4. If yes, T12c shrinks from ~25 LoC to 1 line.

Progress log: iceberg [[2m, 2m−2, 2]]

Session 1 (2026-05-24)

• Starting sorries: 24 across T1–T19 (some Ti have multiple helper sub-sorries)
• Skeleton parses cleanly with lake build QEC.Stabilizer.Codes.Iceberg.N
• Worktree symlink to main repo's .lake/packages confirmed
• Plan order from plan.md: T1, T2, T3 (+bundle), T4, T5, T6, T7, T8, T10, T11, T12a, T12b, T12c, T13-helpers (×2), T14-helpers (×2), T13, T14, T15, T16, T17, T18

Closed so far in this session

• T1 (ZGenerators_are_ZType): direct unfold; per-qubit Or.inr S_Z is constant Z
• T2 (XGenerators_are_XType): mirror of T1
• T3 (S_Z_comm_S_X): pauli_comm_even_anticommutes + filter = univ; cardinality = 2m, even via ⟨m, by ring⟩
• T3-bundle (ZGenerators_commute_XGenerators): rcases on singletons + S_Z_comm_S_X
• T4 (generators_commute): 4-way rcases dispatch via Z/X-type commutes + T3
• T5 (negIdentity_not_mem): CSS.negIdentity_not_mem_closure_union via T1/T2/T3
• T6 (listToSet_generatorsList): direct simp on Set extensionality
• T7 (AllPhaseZero_generatorsList): chain AllPhaseZero_cons + rfl
• T8 (rowsLinearIndependent_generatorsList): parametric column-evaluation argument. Key idea: peel off f at each row by evaluating hf at one Z-column (extracts f 0) and one X-column (extracts f 1). ~60 LoC, harder than the [[4,2,2]] by decide but much cleaner than RepetitionN's approach.
• T10 (stabilizerGroup_toSubgroup_eq): standard.
• T11 (logicalX_anticommutes_logicalZ_diag): parametric by_cases on logIdx/xAnchor/zAnchor/else. Filter = {logIdx i}, cardinality 1, odd. Introduced 3 anchor-distinct helper lemmas.
• T12a (logicalX_commutes_logicalX): commutes_of_componentwise_commutes + split_ifs + simp [PauliOperator.mulOp]. Bypasses pauli_comm_componentwise's fin_cases i.
• T12b (logicalZ_commutes_logicalZ): mirror of T12a.
• T12c (logicalX_commutes_logicalZ_offdiag for i ≠ j): split_ifs + simp_all on mulOp; ~20 LoC. The simp_all resolves all cases since the supports are fully disjoint (no shared qubit).
• T13-helpers (logicalX_commutes_S_Z, logicalX_commutes_S_X): one parametric filter ({logIdx i, xAnchor m}, count 2 even); one componentwise commute.
• T14-helpers (logicalZ_commutes_S_Z, logicalZ_commutes_S_X): mirror of T13-helpers.
• T13, T14 (logicalX/Z_mem_centralizer): standard forall_comm_closure_iff dispatch.
• T15 (stabilizerCode): structure literal — logical_commute_cross via structural refine ⟨_, _, _, _⟩ consuming T12a/T12b/T12c + by_cases on ℓ = ℓ' (since fin_cases ℓ <;> fin_cases ℓ' is unavailable for parametric Fin (2m − 2)).
• T16 (stabilizerCode_toSubgroup_eq): change + rw [listToSet_generatorsList].
• T17 (weight_one_anticomm_witness): clean 3-way match P, hP. No hi_dichotomy needed — both stabilizers have full support.
• weight_logicalX helper: parametric support computation, used by T18.
• T18 (code_has_distance_two): one-liner via hasCodeDistance_two_of_anticommute_witness (PR #34 helper).
• T19 (stabilizerCodeWithDistance): structure literal packaging.

Cleanup (post-T19, agent killed mid-cleanup; spawning agent finished)

• 3 linter warnings on N.lean resolved:
  • Line 565: dropped unused hza.symm from simp [hza.symm, PauliOperator.mulOp]
  • Line 736: dropped unused hxa.symm from simp [hxa.symm]
  • Line 741: show → change (tactic actually rewrites the goal)
  • Line 486: simp [logIdx] → simp only [logIdx] (new linter.flexible site introduced post-cleanup; resolved before commit)
• Stage-2 baseline files committed alongside Stage-4 wrap-up (oversight: Stage 2 produced them in the worktree but didn't commit them):
  • QEC/Stabilizer/Codes/Iceberg.lean (family umbrella)
  • pipeline/attempts/iceberg/{informal_spec, plan, reuse_audit, gap_audit}.md
• state.yaml: status flipped formalization → pr-ready, formalization_completed_at set, final_loc recorded.
• lake build clean repo-wide (3341 jobs); no new linter warnings on the new file.