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.
Condensation bounds a constructible real
Example
If and , the hull-and-collapse proof produces a countable ordinal such that .
Facts & Assumptions
Given: Ambient ZF and a constructible real .
Canonical L-hulls are elementary and small makes the hull of the countable seed elementary and countably infinite.
Condensation for constructible levels identifies the transitive collapse of that hull with .
What the collapse fixes fixes every transitive subset of the hull pointwise and computes collapsed ordinals as order types.
Constructible subsets appear before successor cardinals gives the general conclusion ; the calculation below exhibits its sharper witness .
Verification
Choose a nonzero limit with and form . F1 gives and a bijection between and . In particular every natural number belongs to , not merely the set as one element.
Collapse by to using F2. Since is transitive, F3 fixes every natural number. The map is an isomorphism onto the transitive set : if , surjectivity gives with , and relation reflection gives ; conversely implies . Since and there, . Hence . This includes the empty real.
The collapse is a bijection, so is countable. Since , the ordinal is countable and therefore . Thus the hull calculation proves the claimed bound and, consistently with F4, yields . No ambient Choice is used.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
14 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, Set Theory, Theorem 7.15 and Claim 7.16, p.59 (standard reference, not scraped)