How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The busy beaver function eventually dominates every total computable function
Statement
For every total computable function , with inputs and outputs encoded by their canonical binary numerals, there exists such that
Facts & Assumptions
Given: A total computable function , with inputs and outputs encoded by their canonical binary numerals.
Under the canonical binary-numeral encodings from the Statement, some deterministic Turing machine halts on every input and outputs the binary numeral , by Computable and partial computable functions and Partial functions computed by a machine under fixed encodings.
is the maximum halting time on blank input among all machines whose chosen code has length at most , by The step-count busy beaver function relative to the chosen machine coding.
The chosen machine code records a finite transition table in a finite tuple of binary words, by A fixed effective binary encoding of deterministic one-tape Turing machines.
Proof
By [L1], choose a deterministic machine that, on input , halts with output . For each , build a new machine that has the binary digits of hard-wired into a straight-line prefix of its finite control, using one additional state per written digit and then handing control to a fixed simulation of . On blank input, writes the binary numeral for onto its tape, runs on that input until halts with output , and then runs a fixed binary-counter routine for iterations before halting. Therefore halts on the blank input, and its total running time is strictly greater than .
Write . The construction in step 1.1 uses at most states and a fixed tape alphabet, for constants depending only on and the fixed routines. In the concrete code of [L3], this gives transition triples, and every state numeral in those triples has length . The self-delimiting tuple encoding therefore gives constants such that . Since , the right-hand side is , so there exists such that whenever . For those , the machine is among the competitors counted by .
If , then step 2.1 puts inside the size budget for , and step 1.1 gives a halting time larger than . By [L2], the maximum is therefore at least that halting time, so . Thus eventually dominates .
Depends on
Used by
Dependency tree · two levels
10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Adam Yedidia and Scott Aaronson, A Relatively Small Turing Machine Whose Behavior Is Independent of Set Theory (standard reference, not scraped)