Math Mapgenerated 2026-10-25 · a354234
PUBLIC BUILD
P-010probeOpen2026-09-14structurallogic-computability

Determined but uncomputable — a fifth magnitude slot, or a different axis?

busy-beaver · computability · undecidability · magnitude-taxonomy · ZFC-independence · aaronson-yedidia

no run lists this probe in builds_on:

Stands onnonefrom builds_on: and related:
Stood on byEX-06 EX-10 N-012incoming references, computed at build — never typed

The friction. BB(n) fits no slot in the magnitude taxonomy (§7). Not free — no experimental input; it is fixed by a definition. Not derived — there are no inputs for it to be a function of. Not computed — no algorithm converges, ever. Not bounded — lower bounds only, and unboundedly improvable. So: determined but uncomputable — input cost zero, value completely fixed, no procedure produces it.

The obstruction is not where it first appears. Each individual BB(n) is a constant and therefore trivially computable — return 4098 computes BB(5). What is uncomputable is the function n ↦ BB(n). So the real index is not computability; it is how strong a theory you need. Aaronson–Yedidia, sharpened by Riebel to 745 states, gives a 745-state machine that halts iff ZFC is inconsistent. BB(745) is a specific natural number, with a definite value, that ZFC provably cannot name.

A third species of undecidability. CH is model-dependent — different truth values in different models. P vs NP is arithmetical and open, determinate but out of reach, with three barrier theorems (relativization, natural proofs, algebrization) saying why the tools are too weak. BB(745) is arithmetical, determinate, and provably beyond one named theory, with the boundary locatable to within a few states.

What would settle it. Whether "determined but uncomputable" is a fifth magnitude slot or a statement about theories rather than about numbers. The taxonomy sorts numbers; this may belong on a different axis entirely — the same move as the certificate-direction axis just added to §8.2 (which end of an interval is open), which is likewise orthogonal to the slots.

One claim to press, not accept. The session says the difficulty "is concentrated, locatable, and you can watch it arrive." That overreaches. 745 is an upper bound on where ZFC-independence starts, not a location; the honest statement is that it can be bracketed — between 6 and 745 — and that bracket is wide. Recorded here with its correction, both together.

Cross-references. The three P-vs-NP barriers (relativization, natural proofs, algebrization) as the neighbouring "determinate but out of reach" case; the bound-producing mechanisms table and its new certificate-direction axis in docs/rung-vocabulary-v4-part1.md §8.2 — BB is the lower-open mirror of the anthropic/unitarity upper-open bounds.

Amendment 1 — the invariant exists, and it is an ordinal. A statement is independent of a theory T exactly when it outruns the fast-growing hierarchy at T's proof-theoretic ordinal — Goodstein and Paris–Harrington escape PA because they grow like F_{ε₀}, and ε₀ is PA's ordinal. So the "determined but uncomputable" invariant is named: the proof-theoretic ordinal at which a statement's growth outpaces the theory. It has no evaluation — the map from state count to ordinal is unknown and has no reason to be computable — but a named invariant with no evaluation is a sharper object than a bracket, and it supersedes the 6–745 framing above: the bracket was the symptom, the ordinal is the invariant.

Amendment 2 — BB ↔ Ω, with the failed bridge named. Chaitin's Ω and BB share a Turing degree — both equivalent to 0′, the halting problem — but that degree is crowded and the equivalence is not itself informative. They differ in functional form: Ω is a sum weighted by program length, BB a sup over runtime. The natural bridge, a tropical (β → ∞) limit carrying the sum to the sup, was tried and does not close: the β → ∞ limit of Ω selects the shortest halting program, not the busiest beaver. Named and refuted, not left open.

Amendment 3 — a fifth epistemic category: certified. BB(5) = 4098 is a Π₁ fact whose justification is the Coq development that settled it — machine-generated, machine-verified, and read by no human: the trust chain runs through a proof assistant's kernel rather than through a reader. That is distinct from computed (a human-auditable calculation), and it is the only epistemic category in the framework that did not exist when most of the mathematics in it was done. Files in the magnitude taxonomy as a new epistemic slot, with the four-colour theorem as precedent.

Edge in — cosmic topology beyond the horizon ([[N-012]]). A second instance of "determined but uncomputable" arrives from the residues thread: whether the universe is multiply-connected is a determined fact, Σ₁-certifiable (exhibit a matched circle pair) and Π₁ otherwise — BB(745)'s shape exactly. The distinction worth keeping: here the one-sidedness comes from the light cone, not from a theory's proof-theoretic strength. Same certificate-direction axis, different boundary — an edge, not an identity.

77 source lines, no addenda.

generated 2026-10-25the lab index