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.
Computable domination characterizes truth-table reducibility
Statement
For , the following are equivalent:
- is computably dominated.
- Every satisfies .
Facts & Assumptions
Given: an oracle ; for the forward direction, via a functional ; for the reverse direction, the stated universal truth-table property.
Proof
Assume is computably dominated. For , let be the running time of this halting computation. Then is total and -computable, hence has a computable dominator .
Conversely, suppose every is truth-table reducible to . Toward a contradiction, let be total and not dominated by any total computable function. Fix an effective enumeration of the bit-output oracle functionals and a computable pairing function .
Truncate after steps for every oracle , returning if it has not halted with a bit. This is total on every oracle and agrees with because ; hence .
Let mean that, for every , the finite-oracle computation halts within steps with a bit and without querying a position at least . This is decidable. Define by first computing and then setting When holds, the displayed oracle computation halts within the tested bound, so this definition gives a total -computable set.
If is total on every oracle, the compactness search in An everywhere-total functional has a computable use bound yields, for each , some satisfying . Thus the least such value is a total computable function. Since has no computable dominator, some satisfies . The predicate persists at larger bounds, so step 2.2 gives Hence no everywhere-total bit functional computes from .
By Truth-table reduction, step 3.1 says , contradicting the assumed universal property because . Therefore every total has a computable dominator, so is computably dominated.
This argument also justifies the function-valued shorthand in the cited source theorem without upgrading the set-valued hypothesis by fiat. Once step 4.1 gives domination, the running time of any natural-valued computation of has a computable bound . Truncating at that bound gives an everywhere-total natural-valued functional . Apply An everywhere-total functional has a computable use bound to obtain a computable use bound ; then the finite maximum of over is a computable strict dominator of .
Steps 2.1 and 4.1 establish the two implications.
Depends on
Used by
Dependency tree · two levels
6 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
- Ludovic Patey, Computability Theory, Theorem 5.12 (standard reference, not scraped)