Structural consequences of the retraction equation on the classical carrier. Machine-checked in Lean 4 with Mathlib v4.28.0. One equation on binary strings -- fold . unfold = id -- forces a canonical carrier architecture. The dual composition selfApp = unfold . fold is idempotent and classifies every fold/unfold geometry into three regimes. On the classical carrier (headerLen > 0), three independent results exclude full closure: fold shortens by headerLen unfold lengthens by headerLen headerLen > 0 ──────────────────────────────── No map can commute with both. FoldUnfoldSection → False (six lines, omega) selfApp([]) = header ≠ [] (selfApp ≠ id, pre-semantic) selfApp factors through headerLen drift = headerLen exactly (tight, achieved) A fourth result -- the super-polynomial counting gap -- establishes that the naming obstruction is intrinsic to the carrier's information geometry. P and NP are defined on this carrier (rfl). The carrier's constraints are the carrier's, not the classes'. The obstruction is encoding-invariant. 21 source files, approximately 4,300 lines. Zero sorry. Zero custom axioms. Standard kernel axioms: propext, Classical.choice, Quot.sound.