Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-09
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.

Branches through countable normal trees of limit height

Statement

If T is countable and normal of nonzero countable limit height δ, every node lies on a branch cofinal in δ. There is a countable collection of such branches covering T. The construction works in ZF, with no use of Choice.

Facts & Assumptions

Given: Such T and δ, and an arbitrary tT.

[F1]

Normality gives an extension at every strictly higher level below the tree height. Normal and splitting trees

[F2]

Natural-number recursion defines the unique orbit of a function on a set from a specified initial state. The recursion theorem

[F3]

Every node has a unique predecessor of every smaller height, and two predecessors of a common node are comparable. Strict order increases height. Tree predecessors and compatibility

Proof

1.1

Fix surjections e:ωT and d:ωδ. They exist by countability: δ is infinite, and T has nodes at arbitrarily high levels below δ, so it too is infinite. Only these two witnesses are fixed. Define γ0=d(0) and γn+1=max{γn+1,d(n+1)}. The successor of every ordinal below the limit δ is still below δ, so recursion gives a strictly increasing sequence in δ. It is cofinal since γnd(n). The nonautonomous rule is a recursion on the state (n,γn).

givenF2
2.1

Starting at t0=t, let βn=max{γn,ht(tn)+1}<δ and take tn+1=e(k) for the least k for which tn<Te(k) and ht(e(k))=βn. The candidate set is nonempty by normality. Recursion on (n,tn) supplies this sequence, and its heights are cofinal because ht(tn+1)γn. Least natural indices require no choice function.

F1F2step 1.1
3.1

Put bt={sT:n sTtn}. It contains t and is a chain: if sTtn and uTtm, both lie below tmax{n,m}, so they are comparable. Its heights are cofinal by step 2.1.

F3step 2.1
4.1

If s can be adjoined to bt while retaining a chain, choose n with ht(tn)>ht(s), possible by cofinality and the limit-height hypothesis. Comparability with tn and strict increase of height force s<Ttn, hence sbt. Thus bt is maximal and is a cofinal branch.

F3step 3.1
5.1

The same fixed e,d determine bt uniquely for each tT. Replacement therefore forms B={bt:tT}. The sequence nbe(n) is onto B, so it is countable, and tbt proves that it covers T. The construction includes the root and every prescribed node; no last level exists at the limit height.

step 1.1step 2.1step 3.1step 4.1

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