Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-07
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 XN, the following are equivalent:

  1. X is computably dominated.
  2. Every YTX satisfies YttX.

Facts & Assumptions

Given: an oracle X; for the forward direction, YTX via a functional Φ; for the reverse direction, the stated universal truth-table property.

Proof

technique · direct
1.1

Assume X is computably dominated. For ΦX(n)=χY(n), let t(n) be the running time of this halting computation. Then t is total and X-computable, hence has a computable dominator b.

givenconstruct
1.2

Conversely, suppose every YTX is truth-table reducible to X. Toward a contradiction, let fTX be total and not dominated by any total computable function. Fix an effective enumeration (Θe)eN of the bit-output oracle functionals and a computable pairing function e,k.

givenassume-contra
2.1

Truncate ΦZ(n) after b(n) steps for every oracle Z, returning 0 if it has not halted with a bit. This is total on every oracle and agrees with ΦX because t(n)b(n); hence YttX.

step 1.1construct
2.2

Let D(e,k,s) mean that, for every σ2s, the finite-oracle computation Θeσ(e,k) halts within s steps with a bit and without querying a position at least s. This is decidable. Define YTX by first computing s=f(k) and then setting χY(e,k)={1ΘeX(e,k),D(e,k,s),0,¬D(e,k,s). When D(e,k,s) holds, the displayed oracle computation halts within the tested bound, so this definition gives a total X-computable set.

step 1.2construct
3.1

If Θe is total on every oracle, the compactness search in An everywhere-total functional has a computable use bound yields, for each k, some s satisfying D(e,k,s). Thus the least such value qe(k) is a total computable function. Since f has no computable dominator, some k satisfies f(k)>qe(k). The predicate D persists at larger bounds, so step 2.2 gives χY(e,k)=1ΘeX(e,k). Hence no everywhere-total bit functional Θe computes Y from X.

step 2.2givencontradiction
4.1

By Truth-table reduction, step 3.1 says Y̸ttX, contradicting the assumed universal property because YTX. Therefore every total fTX has a computable dominator, so X is computably dominated.

step 3.1discharge-contradiction
5.1

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 fTX has a computable bound b(n). 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 u(n); then the finite maximum of Ψσ(n)+1 over σ2u(n) is a computable strict dominator of f.

step 4.1construct
6.1

Steps 2.1 and 4.1 establish the two implications.

step 2.1step 4.1

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