Classical Turing Machine Model, Structural Nonclosure, and Regime Classification for the Graded Reflexive Model Framework

Machine-verified formalization in Lean 4 with Mathlib v4.28.0. Constructs a graded reflexive model from classical Turing machine computation, classifies its regime, and proves the structural nonclosure: no GRMorphism from the transport tower T(classicalGRM) to classicalGRM when the self-application header has positive length. Strengthened form (fold_unfold_nonclosure) proves the same at the weakest structural level. The three cannots assembled as a single conjunction: irreducible naming cost, structurally unreachable substrate, no polynomial cover. 28 source files, zero sorry, zero custom axioms in the main theorem chain. Complete theorem inventory in CLAIMS.md.