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.