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: Two classical codes with H_X H_Z^T = 0 are one chain complex; homology counts logicals.
Machine boundary: Lean Complete v1 checks H_X H_Z^T = 0, exact row-interleaved lowering, and supplied boundary maps when present. It does not reconstruct topology or prove a code-family distance statement.
Planned sections: Essence / Design problem / Derivation chain / Multiple pictures / Why these parameters / Failure modes / Operations story / Litmus questions.