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: Logicals live in the centralizer modulo the stabilizer; distance is their minimum weight.
Machine boundary: Lean Complete v1 checks static or dressed logical witnesses, witness-based upper bounds, and a bounded small-exact enumeration class. It does not turn a cited distance into a proof or cover family and Floquet spacetime distance.
Planned sections: Essence / Design problem / Derivation chain / Multiple pictures / Why these parameters / Failure modes / Operations story / Litmus questions.