Locating Hardness: Axioms, Compression and ISP

The standard question about computability theory’s central theorems is what they prove — the halting problem is undecidable, Rice’s theorem blocks program analysis, Gödel’s theorems delimit formal systems. These three papers ask where the proof requires something extra. The answer is precise in each case: hardness enters at a specific axiom, a specific gap, a specific lattice condition — and not anywhere else.

All three papers work from the same categorical foundation: a monoidal closed category with a reflexive object D ≅ [D, D], formalized in Lean 4 with zero sorry, zero Classical.choice, and zero custom axioms. Lean 4’s #print axioms command makes axiom-tracking a measurement rather than a philosophical position — the kernel profile of a theorem is the literal set of axioms its proof term depends on. Starting from this common base, the trilogy asks three versions of the same question: is this result forced by the structure, or does something extra enter?

The Axiom Profile of Computation

Standard mathematics uses “proof by contradiction” for two logically distinct operations. Negation introduction assumes P and derives absurdity — the conclusion is negative, it says something does not hold. Reductio ad absurdum assumes ¬P and derives absurdity — it converts a negative impossibility into a positive conclusion, extracting a witness from a double negation. Classical logic identifies these because it validates P ↔ ¬¬P. Constructive logic distinguishes them: negation introduction is intuitionistic, reductio requires excluded middle, and Markov’s principle — if a Turing machine cannot not-halt, then it halts — sits exactly between them.

The paper reports the axiom profile of each central theorem of computability theory, formalized from the equational theory of monoidal closed categories. The partition falls into three layers. Layer 0 (zero axioms, fully constructive): the Y combinator, Kleene’s recursion theorem, halting undecidability, both Gödel incompleteness theorems, the s-m-n theorem, Myhill’s isomorphism theorem. Layer 1 (Markov boundary): Rice’s theorem — the single step requiring extraction of a halting witness from a double negation. Layer 2 (full excluded middle): Post’s theorem backward direction, arithmetic hierarchy properness in full generality.

That Gödel’s first incompleteness theorem compiles at zero axioms surprises people who remember it as a proof by contradiction. The disambiguation matters: incompleteness has two sides — unprovability (T cannot prove G) and unrefutability (T cannot prove ¬G). Both are negation introduction: assume the contrary, derive absurdity, conclude the negation. Neither step extracts a positive conclusion from a double negation. The proof looks like reductio because it assumes a decider or a proof and derives contradiction — but the contradiction IS the output, a negative result, not a stepping stone to a positive witness. Reductio would be needed only if you wanted to conclude that a halting computation exists by ruling out its non-existence. The standalone file ConstructiveGodel.lean compiles at ∅, confirming this directly.

The boundary between Layer 0 and Layer 1 is established by twenty standalone Lean 4 files, each axiomatizing only the minimum structure needed for its theorem and reporting the exact axiom profile via #print axioms. The boundary is one axiom thick.

Reflexive Compression Boundaries in Graded Categories

Self-reference is cheap to construct — not necessarily cheap to execute. The Y combinator has bounded construction cost: fixed-point formation adds only constant overhead to the cost of the function being fixed. But evaluating the resulting fixed point is where unbounded cost enters. The paper locates precisely where, by decomposing the complexity of self-referential computation into three independent gaps.

Gap 1 (naming): does the fixed-point operator ω map distinct endomorphisms to distinct elements of D? This reduces to whether selfApp is right-cancellable (epi) on endomorphisms — closed by the categorical structure alone. Gap 2 (construction): is building ω(f) cheap? The cost is bounded by cost(f) plus constants from the reflexive isomorphism — also closed by categorical structure. Gap 3 (depth transfer): does evaluating fixed points preserve computational cost? This does not reduce to the categorical structure. It reduces to the growth gap hypothesis: whether the space of endomorphisms eventually outgrows the space of elements at each grade level — a quantitative condition independent of the equational axioms, and formally independent of them.

Three conditions, jointly contradictory: naming, bounded construction, and the growth gap cannot coexist. A reflexive object cannot simultaneously name its endomorphisms faithfully, construct their fixed points cheaply, and accommodate differential semantic complexity growth. Non-uniformity is necessary — uniform graded reflexive isomorphisms prevent the growth gap, so computational growth gaps require graded non-uniformity in the iso, yielding a sharp dichotomy between denotational models (uniform iso, no growth gap) and computational ones (non-uniform iso, growth gap holds). The non-uniformity theorem has a resource-bounded consequence: Markov’s principle at polynomial bounds is equivalent to P = NP — a bridge theorem identifying a resource-bounded witness-extraction principle with the classical search/verification collapse, without itself being a proof of either direction.

Chain Obstructions and the Invariant Subspace Problem

The invariant subspace problem asks whether every bounded linear operator on a separable infinite-dimensional complex Hilbert space has a nontrivial closed invariant subspace. Open since the 1950s. The paper reformulates it as a fixed-point problem on the complete lattice of closed subspaces, then gives a structural account of why the standard approaches fail.

The two canonical fixed-point strategies — iterate from the bottom of the lattice, or from the top — are both immediately blocked. Not because the method is poorly applied, but because the operator collapses both extremes to themselves: F(⊥) = ⊥ and F(⊤) = ⊤, so any chain starting at 0 or H stays there. The difficulty of the ISP does not live in the existence of fixed points — Tarski’s theorem guarantees those — it lives in their location between the extremes.

The chain classification theorem makes this precise: every chain-based approach is bottom-up (blocked), top-down (blocked), or an intermediate orbit chain. Intermediate chains are the only viable route, and their success reduces to two conditions: stabilization (the chain eventually stops growing) and properness (it never reaches ⊤). Three new sufficient conditions follow — the deflation theorem, the lattice intermediate value theorem, and the DCC theorem. The deflation theorem abstracts the order-theoretic template from Lomonosov’s theorem: the compact-operator commutation hypothesis is precisely what supplies the proper pre-fixed point the deflation theorem requires. Independence results confirm that the abstract lattice axiom system neither forces nor precludes nontrivial fixed points; the missing ingredient in the general case is analytic, not order-theoretic.

What the trilogy shows together

Each paper isolates a different layer of how mathematical structure resists collapse. The axiom profile paper shows that computability theory’s core theorems are constructive — the layer structure is not philosophical, it is measured. The compression boundaries paper shows that constructing self-reference is cheap; cost lives in evaluation, and the depth-transfer gap is formally independent of both the naming and construction gaps. The chain obstructions paper shows that the difficulty of the ISP is not in the existence of fixed points but in their location, and identifies precisely what any resolution must supply.

The shared commitment: not “this is hard” but “hardness enters here, at this axiom, this gap, this lattice condition” — and not anywhere else.

Citations: