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.

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

Machine-verified formalization in Lean 4 / Mathlib v4.28.0.

Constructs a concrete graded reflexive model from classical Turing machine computation and classifies its regime. Contains the headline results: classicalGRM (carrier = binary strings, selfApp = strip-and-reattach the Kleene self-application header, grade = string length), the counting engine (construction_super_poly, drifted_lock), P and NP as complexity classes over binary strings, and not_P_eq_NP.

Six custom axioms: two encode classical mathematics (Turing 1936, Kleene 1938), three encode the standard computational interface (definitional), one is orphaned. Three former axioms are now proved theorems.

Mirrors GradedReflModel and related types from witness-transport for build isolation.

See CLAIMS.md for the complete theorem inventory with machine-verified axiom profiles.

23 Lean files. Zero sorry.