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

A long chain with club continuity below aleph omega

Statement

Assume AC. Put μ=ℵω, λ=μ+=ℵω+1, N=ω∖{0,1} and P=∏n∈Nℵn. Every family in P of cardinality less than λ has a strict eventual upper bound in P.

There is a strictly <∗ increasing sequence (fδ)δ<λ in P with (∗)κ for every uncountable regular κ<μ. More precisely, whenever δ<λ and cf⁡(δ)=κ++ for such a κ, there is a club Eδ⊆δ for which sup⁡ξ∈Eδfξ<∗fδ, with the supremum taken pointwise. The strong-increase assertion means every unbounded set of indices contains an order-type-κ subsequence that is pointwise strictly increasing outside the union of two individual finite exceptional sets.

Facts & Assumptions

Given: AC and the cardinals and product just defined; eventual comparison means comparison at all but finitely many n∈N.

[F1]

Club continuity at cofinality κ++ gives (∗)κ when κ is uncountable regular, κ++<λ and the sequence has regular length λ (Club continuity produces strongly increasing subsequences).

[F4]

Specified transfinite rules recurse on well-orders (Transfinite recursion).

[A1]

AC supplies choice functions on nonempty sets of witnesses (The Axiom of Choice).

Proof

1.1F2F3A1

If H⊆P has size ρ<μ, set b(n)=sup⁡{u(n)+1:u∈H} when ℵn>ρ, and b(n)=0 otherwise. At a large coordinate, each successor is below the infinite cardinal ℵn, and F2–F3 place the supremum below ℵn. Only finitely many coordinates have ℵn≤ρ, since sup⁡nℵn=μ. Thus b∈P and u<∗b for each u∈H. The empty family gives b=0 and imposes no comparisons. If instead ∣H∣=μ, take a bijection q:μ→H and let Hj=q[ℵj], so H=⋃j<ωHj and each ∣Hj∣<μ. The preceding formula gives a bound bj for each subfamily and a bound b for the countable family {bj:j<ω}. For u∈Hj, compose u<∗bj<∗b outside the union of the two finite failure sets. AC ensures these cardinalities and the indicated enumeration; thus every family of size less than μ+ has a strict bound.

1.2F2F4A1

For each nonzero limit δ<λ, F2 gives a cofinal sequence of length θ=cf⁡(δ). Turn it into a continuous increasing sequence in δ: at successor stages choose a value above both the preceding value and the next cofinal-sequence term, and at nonzero limits take the supremum of earlier values. Each intermediate supremum is below δ because fewer than cf⁡(δ) terms were used, by F2. Successor choices are possible because δ is a limit. The range is unbounded and closed in δ, hence is a club Eδ of order type θ; closure follows because every nonzero limit point below δ occurs at a limit index of the continuous sequence. F4 supplies the recursion, and A1 chooses these clubs simultaneously from their nonempty witness sets. Also fix by A1 a choice function on the nonempty subsets of the set P for use in choosing bounds.

2.1step 1.1step 1.2F2F3F4

Recursively set f0=0. At every 0<δ<λ, the previous functions form a family of size at most ∣δ∣<λ, so step 1.1 and the choice function of step 1.2 specify a strict eventual bound uδ∈P. If cf⁡(δ)=κ++ for an uncountable regular κ<μ, put vδ(n)=sup⁡ξ∈Eδfξ(n) at coordinates with ℵn>κ++, and put vδ(n)=0 at the others; then set fδ(n)=max⁡{uδ(n),vδ(n)}+1. The large-coordinate supremum is below ℵn because ∣Eδ∣=κ++<cf⁡(ℵn) by F2–F3. Its successor is still below that infinite cardinal. At all other stages put fδ=uδ. Distinct cardinals have distinct double successors, so the special rule is unambiguous. Every value lies in P, and F4 implements this specified recursion through λ. For every ξ<δ we have fξ<∗uδ≤fδ, proving strict increase.

3.1step 1.1step 2.1F1F3

Fix any uncountable regular κ<μ. By F3 it is ℵj for some positive finite j, so κ++=ℵj+2<μ<λ, and λ is regular by F3. At each index δ of that cofinality, step 2.1 used the special rule, giving sup⁡ξ∈Eδfξ(n)=vδ(n)<fδ(n) whenever n>j+2. The other coordinates form a finite set. This is the required club-continuity premise with bounding index exactly δ. The countably infinite coordinate set and strict chain from step 2.1 meet F1's remaining hypotheses. F1 gives (∗)κ for this same chain. As κ was arbitrary, all stated properties hold simultaneously. QED.

Depends on

Used by

Dependency tree · two levels

36 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