Alphabeta MathHow 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.
Cofinality strata and stationary costationary sets
Example
In ZFC, is club, whereas and are disjoint stationary sets, neither containing a club.
Facts & Assumptions
Countable unions of at most countable sets, assuming : Countable choice makes every countable union of at most countable sets at most countable.
Hessenberg: for every infinite cardinal , proved in ZF from the canonical well-order of : In ZF every infinite well-ordered cardinal satisfies for cardinal multiplication.
Regular cofinality strata are stationary: is stationary when lambda is infinite regular and .
Verification
Given: The objects and hypotheses in the statement.
In ZFC omega-one and omega-two are regular: a cofinal family of at most omega ordinals below omega-one has countable union; a cofinal family of at most omega-one ordinals below omega-two has union of size at most . Both would contradict the cardinality of the ambient ordinal. For the second union, AC chooses injections of its at most aleph-one members into omega-one, so the union injects into the product of the index set with omega-one. These estimates use countable choice and infinite well-ordered cardinal multiplication.
Every nonzero countable limit has cofinality omega: enumerate it and take successive finite maxima to obtain a cofinal sequence; a finite subset cannot be cofinal in a limit. Thus is exactly the nonzero limits, a closed unbounded set.
Apply the stratum theorem at omega-two with lambda equal to omega and omega-one. The resulting stationary sets are disjoint since an ordinal has only one cofinality. A club contained in either would miss the other, contradicting stationarity.
Depends on
- Regular cofinality strata are stationary
- The club filter is never an ultrafilter
- Hessenberg: $\kappa \otimes \kappa = \kappa$ for every infinite cardinal $\kappa$, proved in ZF from the canonical well-order of $\kappa \times \kappa$
- Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
32 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
- Vasey, Example 14.13(6) and Corollary 15.4, pp.82–84 (standard reference, not scraped)