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: Dynamical codes are sequences of measured Pauli products; the ISG is the state's instantaneous stabilizer.
Machine boundary: Lean Complete v1 checks ordered commuting rounds, the declared finite snapshot, and periodic row-space recurrence where required. It does not formalize spacetime distance or dynamic logical transport.
Planned sections: Essence / Design problem / Derivation chain / Multiple pictures / Why these parameters / Failure modes / Operations story / Litmus questions.