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.
The local-GCH Hartogs dichotomy
Statement
Work in ZF. Suppose and . If , then is well-orderable and . Otherwise .
Facts & Assumptions
Local GCH absorbs sums and squares: Under the hypotheses, absorbs its square and two copies; the power set absorbs its square.
Power-set fibres force well-orderability: An injection well-orders .
Hartogs: an ordinal that does not inject into a given set: No injection exists, and every smaller ordinal embeds.
Hessenberg: for every infinite cardinal , proved in ZF from the canonical well-order of : An infinite well-ordered cardinal absorbs its square in ZF.
The Schröder-Bernstein theorem: Opposite injections yield a bijection.
Proof
Given: The objects and hypotheses in the statement.
Put and . Suppose . Then . Strictness holds because would embed into . For the last bijection, , using the omega shift. Local GCH therefore gives .
Singleton injection in the first coordinate and square absorption give , while using one fixed point of . Thus , and the fibre lemma well-orders .
Let be the least ordinal equipotent with this well-orderable . Hartogs is an infinite initial ordinal: an equipotent smaller ordinal would contradict its least-nonembedding property. Moreover . Both and embed in , so injects into , and the reverse injection is immediate. Hence .
If instead does not inject into , its least nonembedding ordinal satisfies . Since injects into by singletons, every ordinal embedding into embeds into , so . This yields the second branch.
Depends on
- Local GCH absorbs sums and squares
- Power-set fibres force well-orderability
- Hartogs: an ordinal that does not inject into a given set
- Hessenberg: $\kappa \otimes \kappa = \kappa$ for every infinite cardinal $\kappa$, proved in ZF from the canonical well-order of $\kappa \times \kappa$
- The Schröder-Bernstein theorem
Used by
- Specker’s two-local-GCH theorem Theorem
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
- Caicedo, Some choiceless results (5), Lemma 2 and subsequent Hartogs equality (standard reference, not scraped)