Computation Precedes Naming: Naming Returns Computation

One equation on binary strings — fold ∘ unfold = id — forces structural results at each level of determination. The dual composition selfApp = unfold ∘ fold is idempotent and classifies every fold/unfold geometry into one of three regimes. Three independent results prove nonclosure on the classical carrier. P and NP are defined on this carrier definitionally. The structural results constrain every computation on it. P ≠ NP on the classical carrier. Machine-checked in Lean 4 with Mathlib: 22 source files, ~4,300 lines, zero sorry, zero custom axioms.