uncomputables
plain-language theorem explainer
The uncomputables definition enumerates the halting problem, busy beaver function, and Kolmogorov complexity. Researchers deriving physical models of computation cite it to connect Recognition Science ledger universality to the Church-Turing thesis. The declaration is a direct list construction with an attached comment invoking diagonal arguments from self-reference.
Claim. The uncomputables are the halting problem (whether program $P$ halts on input $x$), the busy beaver function (maximum steps for an $n$-state Turing machine), and Kolmogorov complexity (shortest program for string $s$).
background
The module derives the Church-Turing thesis from Recognition Science by showing that the ledger simulates any physical process via sequences of updates. The eight-tick structure supplies a universal gate set. Upstream results include the structure for meta-realization in UniversalForcingSelfReference, which records properties required for self-reference instances, and the collision-free predicate in OptionAEmpiricalProgram.
proof idea
The definition directly constructs the list of three named problems. An attached comment sketches the diagonal argument for halting undecidability and restates it in ledger terms where self-prediction defeats the purpose.
why it matters
This entry catalogs computational limits that follow from ledger universality in the Church-Turing derivation. It supports the paper proposition on the physical basis of universal computation. No downstream theorems depend on it, leaving open the embedding of these limits into the full forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.