STATUS: stub — full derivations land in the pedagogy pass (spec section 7, foundations scope ~ Faist lecture notes). Lean L1 target: this topic's framework definitions (spec section 11).
One-liner: A code is the +1 eigenspace of an abelian Pauli group; k = n − rank.
Machine boundary: Lean Complete v1 checks a finite presentation's commuting rows, canonical GF(2) rank, k, logical witnesses, and bounded distance certificates. It does not yet supply the planned reader derivation or a family theorem.
Planned sections: Essence / Design problem / Derivation chain / Multiple pictures / Why these parameters / Failure modes / Operations story / Litmus questions.