Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Acceptable numberings are computably intertranslatable

Statement

If (αe)e∈N and (βe)e∈N are acceptable numberings of the partial computable functions, then there exist total computable functions tα→β,tβ→α:N→N such that for every index e, βtα→β(e)=αe,αtβ→α(e)=βe.

Facts & Assumptions

Given: Two acceptable numberings (αe) and (βe).

[L1]

The fixed machine coding defines an acceptable numbering, by The fixed machine coding gives an acceptable numbering.

[L2]

An acceptable numbering is universal and has a total computable hard-wiring operation, by Universal and acceptable numberings.

Proof

technique · direct
1.1L1L2givenconstruct

By [L1], let (φe) denote the standard acceptable numbering coming from the fixed machine coding. Because α is universal by [L2], the partial function (e,x)↦φe(x) has some α-index u. Because α is acceptable, [L2] supplies a total computable hard-wiring map sα, and then tφ→α(e):=sα(u,e) satisfies αtφ→α(e)(x)≃αu(⌜e,x⌝seq)=φe(x). So φ translates computably into α. The same argument gives a computable translator tφ→β from φ into β.

2.1L1L2step 1.1construct

Because φ is universal and α is acceptable, the same argument with the roles reversed gives a total computable translator tα→φ with φtα→φ(e)=αe. Likewise there is tβ→φ with φtβ→φ(e)=βe.

3.1step 1.1step 2.1algebra

Compose the translators through the hub numbering φ: tα→β:=tφ→β∘tα→φ,tβ→α:=tφ→α∘tβ→φ. Then βtα→β(e)=φtα→φ(e)=αe, and similarly αtβ→α(e)=βe.

4.1step 3.1∎

Therefore any two acceptable numberings are computably intertranslatable.

Depends on

Used by

Dependency tree · two levels

11 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