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: Trade logical qubits for gauge freedom; k = n − (rank G + rank S)/2.
Machine boundary: Lean Complete v1 checks the supplied stabilizer/gauge presentation, protected-logical rank formula, and dressed logical witnesses. It does not assert that the supplied stabilizers generate every abstract center or prove subsystem families.
Planned sections: Essence / Design problem / Derivation chain / Multiple pictures / Why these parameters / Failure modes / Operations story / Litmus questions.