Machine-verified formalization in Lean 4 / Mathlib v4.28.0. The reflexive object D ≅ [D,D] has two equations: fold ∘ unfold = id (certification is free) unfold ∘ fold = selfApp (extraction generates computation) Under resource bounds, certification stays free and extraction becomes costly. The gap between them, parameterized by the resource regime, generates three known stratifications: Logical : ∅ / Markov / EM Polynomial : P / NP (polynomial Markov bridge) Categorical: bounded / unbounded "!" contraction cost These are not three analogies. They are three instances of a single abstract WitnessSystem, with the collapse predicate being EM, P = NP, and ¬HasGrowthGap respectively. The collapse correspondences are mediated by explicit bridge theorems, not by definitional renaming. The key bridge theorem: PolyMarkov ↔ P = NP Markov's principle restricted to polynomial predicates — irrefutable bounded existence implies polynomial findability — is equivalent to P = NP through axiomatized search-to-decision and finder-to-decider reductions. The computability side proves a three-gap decomposition of self-referential computation: Naming gap: CLOSED (selfApp-epi gives internal naming, no Gödel numbering) Construction gap: CLOSED (fixed-point construction cost ≤ linear) Depth gap: FORCED (finite-table representability forces tower growth gap) Naming + Construction + Growth gap = False (anti-compression at []) The growth gap is proved for Nat.Partrec.Code via Mathlib's computability library. The barrier diagnostic confirms the growth gap relativizes (Baker-Gill-Solovay blocks direct P ≠ NP separation), while identifying a category mismatch with natural proofs (the gap is global slice-counting, not truth-table-local). The ISP (invariant subspace problem) side proves: Chain classification: extremal chains produce only trivial fixed points Deflation theorem: pre-fixed + non-collapse → nontrivial fixed point Operator bridge: compact → DCC path, normal → spectral path, general → orbit chain Independence: both ISP success and failure are satisfiable in abstract lattice models The deflation theorem recovers the order-theoretic template of Lomonosov's 1973 compact-operator result as a special case of the deflation mechanism. The axiom profile methodology measures which logical principles each theorem requires: Layer 0 (∅): Y combinator, Gödel I & II, halting, Kleene recursion, Myhill iso Layer 1 (Markov): Rice's theorem (exact boundary) Layer 2 (EM): Post backward ≡ EM, full hierarchy properness Applied to algebra: Bezout, CRT, Lagrange, Sylow compile at Layer 0. Maximal ideals and infinite-dimensional bases require Layer 2 (Choice/Zorn). The Markov layer is empty in algebra — specific to computation. 93 files. 0 sorry. 0 warnings. 3469 build jobs. All paper-critical theorems verified at [] or [propext, Quot.sound] via Lean.collectAxioms. Classical.choice enters only through Mathlib bridge files and deliberate countermodel constructions. Full axiom verification in AXIOM_VERIFICATION.md (3179 declarations checked). Key companion documents: THEOREM_MAP.md — every theorem with axiom profile and scope AXIOM_VERIFICATION.md — 3179 declarations verified via Lean.collectAxioms Supports three papers: The Axiom Profile of Computation Reflexive Compression Boundaries in Graded Categories Chain Obstructions and Deflation in the Invariant Subspace Problem