Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

An aleph omega plus one scale on an infinite set of successor alephs

Statement

Assume AC. There is an infinite B⊆ω∖{0,1} and a sequence (sα)α<ℵω+1 in ∏n∈Bℵn which is strictly increasing and cofinal modulo finite sets. In particular the true cofinality of this reduced product is ℵω+1. The assertion chooses an infinite coordinate subset; it does not assert the same cofinality on the full sequence of successor alephs.

Facts & Assumptions

Given: AC. Put N=ω∖{0,1}, μ=ℵω and λ=ℵω+1.

[F1]

There is a strict eventual λ-chain in ∏n∈Nℵn satisfying (∗)κ for every uncountable regular κ<μ (A long chain with club continuity below aleph omega).

[F2]

On countably many coordinates, (∗)κ for uncountable regular κ gives the κ bounding-projection property (Strongly increasing subsequences force a bounding projection).

[F3]

The ℵ1 projection property and regular length greater than ℵ1 give an exact least bound with positive limit values. Additional projection properties force corresponding eventual lower bounds on coordinate cofinalities; exactness restricts to positive supports (Bounding projections produce an exact upper bound with large coordinate cofinalities).

[F6]

A specified transfinite recursion determines its sequence (Transfinite recursion).

[F7]

A scale is a strict cofinal chain of regular length under the ideal comparisons (Reduced products, true cofinality and scales).

[A1]

AC supplies simultaneous cofinal enumerations and choices of witnesses in set-sized products (The Axiom of Choice).

Proof

1.1F4F6F7A1

We first give the cofinal-suborder transfer used below. Suppose an eventual-comparison product P has a strict cofinal regular λ-chain (pξ)ξ<λ, and j:Q→P preserves and reflects weak and strict comparisons and has a cofinal image. Every family of fewer than λ elements in P has a strict bound: choose for each member a weakly dominating chain term, bound these indices below λ by F4 and take a later term. To build a chain in j[Q], recurse through η<λ, strictly bounding all earlier chosen image elements together with pη by this rule, then choosing an image element weakly above that strict bound. A1 fixes a choice function on the nonempty witness subsets before the F6 recursion. The new image element strictly exceeds every predecessor and pη; hence the image chain is strict and cofinal in P, and reflection makes its preimage a strict cofinal chain in Q. No cofinal family of size less than λ exists in either order: in P the strict bound just constructed contradicts cofinality, and a cofinal family in Q would map to one in P. Thus this procedure transfers precisely the regular true cofinality λ. It uses no assertion that a ceiling map preserves strict inequalities.

1.2F1F2F3F4F5

Take the chain f from F1. F2 gives all its uncountable regular projection properties below μ, in particular at ℵ1. By F5, λ is regular and greater than ℵ1, so F3 gives an exact least bound v with positive limit values. The function a(n)=ℵn is a pointwise bound; leastness gives v≤∗a. Set h(n)=min⁡{v(n),a(n)}, so h=∗v and h remains positive and limit-valued everywhere. Exactness and all eventual coordinate-cofinality conclusions are unchanged. Apply the ℵ2 conclusion and discard its finite exceptional set, leaving infinite N′⊆N, with c(n)=cf⁡(h(n))≥ℵ2>ℵ1 for every n∈N′. For all these coordinates c(n)≤ℵn<μ: a cofinal subset of h(n)≤ℵn has size at most ℵn. Further, for each finite k, the ℵk+1 cofinality bound holds outside a finite set (using ℵ1 when k=0). Hence c(n)>ℵk eventually. In particular c tends to μ in the sense of eventually exceeding every smaller cardinal. Restriction to N′ preserves exactness by F3.

2.1step 1.1step 1.2F4F7A1

Every fξ<∗h, since fξ<∗fξ+1≤∗h. After restriction to N′, reset its finitely many failure coordinates to zero to obtain f~ξ∈∏n∈N′h(n). These resets preserve strict comparisons. Given g in that product, exactness gives g<∗fξ=∗f~ξ for some ξ, so the reset chain is cofinal. By F4 and A1 choose increasing cofinal maps en:c(n)→h(n). The map E(t)(n)=en(t(n)) from ∏c(n) into ∏h(n) preserves and reflects pointwise comparisons at every coordinate, hence also eventual weak and strict comparisons. Its image is cofinal: for each g take the least γn<c(n) with g(n)≤en(γn), which exists by cofinality. Apply step 1.1 to obtain true cofinality λ on ∏c(n) modulo finite sets.

2.2

Put D=ran⁡(c↾N′). Each d∈D is a regular cardinal by F4, at least ℵ2 and less than μ. Each fiber {n:c(n)=d} is finite: choose finite k with d≤ℵk; step 1.2 gives c(n)>ℵk outside a finite set. Consequently the preimage of a finite subset of D is finite. Conversely if E⊆D is infinite, its preimage is infinite, because the image of a finite set cannot be infinite and c is onto D. For u∈∏d∈Dd, define R(u)(n)=u(c(n)). Its comparison failure sets are exactly the preimages of those on D; thus R preserves and reflects eventual weak and strict comparisons. Its image is cofinal: for t∈∏c(n) put

T(d)=sup⁡{t(n)+1:n∈N′, c(n)=d}.

Every fiber is nonempty and finite, and its values are below the infinite cardinal d, so T(d)<d and t(n)<T(c(n)) at each coordinate. Thus T∈∏D and t<R(T) pointwise. Finally D is unbounded in μ by step 1.2, so it is infinite. [step 1.2, F4, F5]

3.1step 1.1step 1.2step 2.1step 2.2F5F7

Apply the transfer of step 1.1 to the cofinal embedding R of step 2.2 and the strict cofinal chain of step 2.1. This gives a scale of length λ on ∏D modulo finite sets, with no shorter cofinal family. Each d∈D is a unique ℵk with finite k≥2, by F5 and the bound ℵ2≤d<μ. Set B={k≥2:ℵk∈D}. The bijection k↦ℵk from infinite B to D carries finite sets to finite sets in both directions and carries product functions to product functions. Reindexing the scale therefore preserves its strict comparisons and cofinality, giving the stated sequence (sα)α<ℵω+1 on B. This proves the assertion, including its true cofinality claim. QED.

Depends on

Used by

Dependency tree · two levels

38 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