Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Size and rank bounds below an inaccessible

Statement

In ZFC let kappa be inaccessible. Then Vα<κ for every α<κ, every xVκ has size less than kappa, and every set of fewer than kappa elements of Vκ belongs to Vκ. For cardinals μ,ν<κ, μν<κ, with 00=1. The strong-limit cardinals below kappa contain a club subset of kappa.

Facts & Assumptions

Given: ZFC. Supplied the cardinal-square proof and small-union estimate locally, identifying AC for simultaneous injections; then proved the rank, exponent and strong-limit club assertions with all zero and limit cases.

[F1]

Inaccessible and Mahlo cardinals: Kappa is regular uncountable and strong limit; club uses closure at nonzero limit accumulation points.

[F2]

The cumulative hierarchy: V grows by power sets at successors and unions at limits.

[F3]

Membership rank under Foundation: Ranks are suprema of member ranks plus one, and rank below kappa means membership in V_kappa.

[F4]

The Axiom of Choice: AC permits well-ordering sets, cardinal comparisons and simultaneous selection of injections for a set family.

Proof

1.1

We first justify the small-union estimate used here. For every infinite cardinal theta, θ×θ=θ: by induction on infinite cardinals order pairs by their maximum coordinate, then lexicographically. An initial segment ending at coordinates below γ+1<θ has size at most (γ+1)×(γ+1)<θ, by the induction hypothesis at γ+1 (or by finite counting). This well-order has type at most theta, since otherwise its first theta elements would be a proper initial segment of size theta. The reverse bound uses the injection ξ(ξ,0). Consequently for fewer than kappa sets of size below kappa, regularity bounds the set of their cardinalities and the index cardinal below a common infinite cardinal η<κ. Such an eta exists because a strong-limit cardinal is a limit cardinal: if kappa were the successor of eta, Cantor diagonalization would give 2ηκ. AC selects injections of the sets into eta, embedding their disjoint union into η×η. Its size is therefore below kappa.

F1F4
2.1

Induct on α<κ. The empty V_0 is small. At a successor, Vα+1=2Vα<κ by strong limit. At a nonzero limit alpha there are fewer than kappa earlier levels, so step 1.1 bounds their union below kappa. If xVκ, it is a subset of some earlier V level, hence has size below kappa.

F1F2step 1.1
3.1

If YVκ and Y<κ, Replacement collects the ranks of its members; regularity bounds their supremum plus one below kappa. Thus the supremum of their ranks plus one, namely rank(Y), is below kappa, so YVκ. For empty Y the rank is zero.

F1F3step 2.1
4.1

For μ,ν<κ, graphs inject the set of functions νμ into P(ν×μ). Step 1.1 bounds the product size by some infinite η<κ, so μν2η<κ. This also covers finite cardinals; more explicitly μ0=1, 0ν=0 for positive nu and 1ν=1.

F1F4step 1.1step 3.1
5.1

Let C be the set of infinite strong-limit cardinals below kappa. It is unbounded: above a given bound start with an infinite cardinal θ0<κ larger than it, put θn+1=2θn and δ=supnθn<κ by regularity. Cantor diagonalization makes the sequence strictly increasing. Its supremum is a cardinal: a bijection of delta with a smaller ordinal would inject a larger theta_n into a smaller cardinal. For every cardinal μ<δ some theta_n exceeds mu, hence 2μθn+1<δ. Thus delta is in C. If delta<kappa is a nonzero limit accumulation point of C, it is similarly a cardinal, and for every cardinal mu<delta there is ρCδ above mu, giving 2μ<ρ<δ. Thus delta is in C, proving closure. No enumeration choices are needed in this last uniquely defined iteration.

F1F4step 4.1

Depends on

Used by

Dependency tree · two levels

14 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