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.
Clubs are ranges of normal enumerations
Statement
In ZFC, any unbounded , with regular uncountable, has a unique increasing enumeration . The set is closed iff this enumeration is normal. Consequently the range of a strictly increasing is club iff is normal.
Facts & Assumptions
Normal ordinal functions: Normality is strict increase and continuity at nonzero limits.
; and ; for a limit ordinal the value is an infinite cardinal with , so it is regular; and every cofinal subset of has cardinality at least , a value that is attained: A cofinal subset of regular kappa has size kappa.
Proof
Given: The objects and hypotheses in the statement.
The inherited ordinal order enumerates by an ordinal , successively taking the least unused point. Unboundedness and regularity force , hence . The least-unused rule also proves uniqueness.
If is closed and is limit, is a limit point of , hence lies in . Strict increase and least-unused enumeration force . Thus is normal.
Conversely, if is normal and is a nonzero limit point of , the indices of the points in form an initial segment with no last element. (They cannot be all kappa since C is unbounded.) Continuity gives , so is closed. Finally, a strictly increasing map on kappa has unbounded range: a bounded range cannot contain kappa distinct ordinals. It is the increasing enumeration of its range, giving the last equivalence.
Depends on
- Normal ordinal functions
- $\operatorname{cf}(\alpha) \le \alpha$; $\operatorname{cf}(0) = 0$ and $\operatorname{cf}(\alpha + 1) = 1$; for a limit ordinal $\lambda$ the value $\operatorname{cf}(\lambda)$ is an infinite cardinal with $\operatorname{cf}(\operatorname{cf}(\lambda)) = \operatorname{cf}(\lambda)$, so it is regular; and every cofinal subset of $\lambda$ has cardinality at least $\operatorname{cf}(\lambda)$, a value that is attained
Used by
Dependency tree · two levels
21 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, Lemma 14.4, p.80 (standard reference, not scraped)
- Welch, Lemma 2.12 and Exercise 2.5, p.20 (standard reference, not scraped)