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.
Cofinality , and regular and singular cardinals
Definition
Let be an ordinal (Ordinal (von Neumann)). The cofinality of is
cofinal range meaning that is a cofinal subset of (Cofinal subset of an ordinal): every satisfies for some . That such a least ordinal exists, and that a witnessing map of that length may be taken strictly increasing, is For every ordinal there is a least ordinal admitting a map with cofinal range, and that map may always be taken strictly increasing, and both are theorems of ZF. So is defined at every ordinal, without any choice principle.
Regular and singular. An infinite cardinal — a cardinal (Cardinal (initial ordinal) and cardinality) with (Cardinal sum , product and exponentiation , and why they are written apart from the ordinal operations), for instance any (The successor cardinal , the alephs , the beths , successor and limit cardinals, and the identifications and ) — is
- regular when ;
- singular when .
The two cases are exhaustive by definition, and by ; 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 ↗ singular means exactly , since always holds.
Remarks
Why regularity is defined for cardinals and not for ordinals. The definition of applies to every ordinal, and it must, because the construction quantifies over maps into of every length. But is an uninteresting condition on a general ordinal: it fails at and at for reasons that have nothing to do with size, and it holds only at , at , and at infinite cardinals, where it is exactly the regularity defined above and so fails at every singular one. Calling an ordinal regular would therefore say nothing new, which is why the words are attached to cardinals here.
What a singular cardinal is, in one sentence. A cardinal that is reachable from below by fewer than steps: there is a strictly increasing family of ordinals below , indexed by an ordinal strictly shorter than , whose supremum is . That is exactly the failure of regularity, and is regular in ZF; assuming the Axiom of Choice every successor aleph is regular; , so is singular, and under choice it is the least singular infinite cardinal exhibits a cardinal for which it happens.
Why being a regular cardinal is a theorem and not part of the definition. Regularity is defined through , so building " is regular" into the definition would make the definition refer to itself. The statement is true, and it is ; 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 ↗; it is recorded here as the item that discharges the naming obligation of this definition, and nothing above depends on it.
Only one notion of "cofinal" exists in this library. Cofinal subset of an ordinal introduces cofinal subsets, because the boundedness theorem for needs them, and deliberately introduces neither the cofinality function nor the regular/singular vocabulary. Both are introduced here, and the definition above is written in exactly that item's terms, so no second notion is created.
Depends on
For every ordinal there is a least ordinal admitting a map with cofinal range, and that map may always be taken strictly increasing
Cofinal subset of an ordinal
Ordinal (von Neumann)
Cardinal (initial ordinal) and cardinality
Cardinal sum , product and exponentiation , and why they are written apart from the ordinal operations
The successor cardinal , the alephs , the beths , successor and limit cardinals, and the identifications and