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.
Splitting a stationary set concentrated on regular cardinals
Statement
In ZFC, if is regular uncountable and is a stationary subset of the regular uncountable cardinals below , then has a partition into stationary sets.
Facts & Assumptions
Removing the trace preserves a stationary remainder: Removing its trace from a stationary set preserves stationarity.
Clubs are ranges of normal enumerations: Clubs on regular uncountable cardinals have normal increasing enumerations of full cardinal length.
The diagonal intersection of clubs is club: The diagonal intersection of kappa clubs is club.
Closure points form a club: Every self-map of kappa has a club of closure points.
Unboundedly many stationary fibres yield a partition: Stationary tails of a regressive map yield kappa stationary pieces.
Proof
Given: The objects and hypotheses in the statement.
Let , stationary. For each use AC to choose a club disjoint from , and let be its normal enumeration. Such clubs exist since alpha is regular uncountable and is not in the trace.
For each coordinate consider the domain . Suppose no coordinate has stationary sets for every . Choose a failing threshold and avoiding club , so whenever .
Let and let be the club of closure points of . Choose and then above alpha. For every , diagonal membership of gamma and closure at alpha give . Since alpha is a nonzero limit, continuity gives . Strict increase implies by ordinal induction, so in fact . This contradicts , since .
Consequently some has all stationary tail domains. Its coordinate map on is regressive and the fibre lemma partitions into kappa stationary sets. Add to one piece; this preserves stationarity and disjointness and gives the desired partition of S.
Depends on
Used by
Dependency tree · two levels
15 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
- Lietz, Theorem 5.14 case 2 and Claim 5.18, pp.44–45, with the domain restricted to the stationary set (standard reference, not scraped)