Scholia

§II proved the theorem; §IV will price each claim in named assumptions. Between them sits the thing the corpus most wants checked: the literal identity. The construction g(x) = α(φ(x)(x)) never changes. What changes from Cantor to Gödel to the Y-combinator is only the reading of its four parts — the objects A, the answers B, the self-naming φ, and the twist α. Select a result and watch the same line become it. The verdict at the bottom is not a new theorem; it is where the forced fixed point is permitted to land.

The same fixed point, four destinies. When the answer-object is too rigid to contain it, the construction becomes a witness of non-surjectivity — Cantor's uncountability, Turing's undecidability: nothing was named that should have been. When the naming is total and the value may diverge, it is recursion — Kleene's theorem, the quine, the positive twin whose unique fixed point §IV pins down. When it is forced into two truth-values as a proof of its own negation, the host collapses — Russell, the Liar, Curry. And when the predicate is provability rather than truth — strictly weaker than truth, by the very gap the diagonal opens — the fixed point is a sentence the theory can neither prove nor refute: Gödel. Four fates; one line; and the dividing question, in every case, is the single bit of §II — does the twist have a fixed point of its own, and may it land?

This is the one place the apparatus must go past Lawvere, because the corpus's positive claims depend on it and §II does not reach it. The fixed-point theorem is an existence result: it manufactures some s with α(s) = s and says nothing about how many there are or whether one can write it down. For most of the genera that is the end of the story. But when the twist is the provability predicate — when α is built from □ — the diagonal's fixed points are governed by a logic of their own, and in that logic existence is upgraded to uniqueness with a formula. The Gödel sentence is not merely a sentence equivalent to its own unprovability; it is, up to provable equivalence, the only one — and it is provably equivalent to Con. The corpus leans on this every time it treats "the" Gödel sentence as a determinate object.

What this buys the corpus is precision about its own central objects. Three consequences fall out of the calculator at once. First, Gödel II is Löb at falsity: the fixed point of "I am unprovable" is Con = ¬□⊥, and Löb's theorem applied to ⊥ says T ⊬ Con unless T is inconsistent — the second incompleteness theorem, read straight off the fixed point. Second, Henkin's question is settled by the same engine: a sentence asserting its own provability is not undecidable but simply provable (its fixed point is ⊤), the exact opposite of the Gödel sentence's fate, and for the exact same reason — Löb. Third, and most important for the unification: where Lawvere stops at "a fixed point exists," the provability core delivers determinacy — the recursion is not just present but pinned down. The Engine and the Ascent (§VI) rest on this stronger fact, not on bare existence.

The corpus says, again and again, that the famous results are one construction. Made precise, that claim has a cost, and the cost is nameable. To carry a result into the cartesian closed category where Lawvere's theorem applies, one must assume certain propositions — the bridge-assumptions. Some are definitional and free; some are deep theorems in their own right; and where none suffice, the claim of identity simply fails, and a weaker, honest relation takes its place. Select a result to read its bill.

What the inspector shows is a graded honesty, and it now runs the length of the whole corpus. The limits of logic and computation — Cantor, Russell, Gödel I, Tarski, halting, Rice, the second incompleteness theorem and Löb — are genuine instances: each becomes the construction once a handful of proven bridge-assumptions (arithmetization, representability, the diagonal lemma, the s-m-n theorem, the derivability conditions) are named. The positive twin, recursion, is an instance in two homes at once — the untyped λ-calculus and the category of computable maps — and Curry's paradox is the hinge where that twin, given one structural rule too many, collapses into the first. Past that perimeter the likeness thins: the hierarchy theorems keep the technique and lose the theorem; the order and topological genera keep a schema and lose the reduction; and the Descent's receding model — Löwenheim–Skolem — keeps only a metaphor. The corpus's integrity lies in marking exactly where each falls.

The inspector sorts the corpus's claims into four ranks, and the ranks are the whole point. Across logic and computation, the unification is a theorem: each result becomes the construction once finitely many proven bridge-assumptions are named. One step out, at the complexity hierarchy theorems, only the technique survives — the diagonal as a method of separation, with no fixed-point theorem anywhere in it. Among the other genera, the order-theoretic and topological fixed-point theorems, there is a real family resemblance under a single schema — richness plus regularity yields a fixed point — but no reduction in either direction; the kinship is conceptual, not deductive. And in the human sciences the connection is a suggestion, sometimes productive and sometimes, as in the Lucas–Penrose argument, a fallacy wearing the costume of a proof.

Read down the ranks and the corpus's real shape appears. Its spine — the Diagonal, the Engine, the Ascent — is proven isomorphism to one theorem. Its breadth — the Atlas — is an honest schema that the author declines to overstate. Its most poetic reach — the Descent — is marked, in the corpus's own hand, as suggestion. And its center — the Mirror — is the theorem from which all of this is measured. A research program that grades itself this strictly has earned the one claim it does make.