Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 2026-09-06
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.

Shoenfield's limit lemma

Statement

A set, equivalently its characteristic function, is computable in 0 if and only if it is limit computable.

Facts & Assumptions

Given: a set AN.

[L1]

A halting oracle computation has a finite query witness (An oracle computation has a finite query witness).

Proof

technique · direct
1.1

Use the halting-set meaning of 0 fixed in Post's theorem. A query code e specifies an ordinary computation whose halting is in question. Put 0s={es:the computation coded by e halts within s steps}. Bounded simulation makes membership in 0s uniformly decidable in (e,s). These sets are finite and increasing, and their union is 0: a genuinely halting computation enters once s exceeds both its code and its halting time; a nonhalting computation never enters.

givenconstruct
2.1

If AT0, fix M0 computing χA. Define g(x,s) by simulating at most s oracle-machine transitions of M(x), answering each query by the decidable set 0s. Return the output if it halts with output in {0,1} within the cutoff, and return 0 otherwise. Each stage halts, so g is total computable and bit-valued even when an incorrect oracle sends M into a loop or an unintended output. No time-efficiency bound on this finite simulation is asserted.

step 1.1construct
3.1

For fixed x, the true run has a finite transition length r and a finite query set F by L1. All negative answers on F are correct at every stage. Each positive answer becomes permanently correct by step 1.1; take s0r beyond the finitely many corresponding entry stages. For every ss0, L1 gives exactly the true run with oracle 0s, and the cutoff does not interrupt it. Thus g(x,s)=χA(x) eventually. An empty F requires only the time cutoff, and s0 is an existence bound, not a claimed computable modulus.

step 1.1step 2.1L1
4.1

Conversely, let total computable h(x,s) converge eventually to χA(x). For each (x,s), effectively form the ordinary program that computes h(x,s), searches t=s+1,s+2,, and halts upon finding h(x,t)h(x,s). Its halting is a 0 question. Ask these questions for s=0,1, until receiving a negative answer. Eventual constancy ensures termination; a negative answer means that all later values equal the current value, which must therefore be χA(x). Output it. This computes A in 0 and proves the reverse implication.

givenconstruct

Depends on

Used by

Dependency tree · two levels

7 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