Structural nonclosure on the classical computation carrier (binary strings with drop/prepend). Three independent machine-checked proofs that the section does not close: no structure-preserving map from the frictionless model (foldᵤnfoldₙonclosure, six lines, omega) ; selfApp not equal to identity (presemanticₙotgroupC) ; irreducible factoring through header length (classicalGRMfactorsThrough). P and NP are defined on this carrier (rfl). The nonclosure constrains them. Formalized in Lean 4 with Mathlib v4. 28. 0. Zero sorry, zero custom axioms.
Larsen James Close (Sat,) studied this question.