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.
V=L refutes the normal Moore space conjecture
Statement
refutes the normal Moore space conjecture: it proves that there is a normal nonmetrizable Moore space (CH yields a normal nonmetrizable Moore space, Moore spaces and developments).
Facts & Assumptions
Given: The axiom over .
GCH gives the continuum hypothesis at : the instance at the infinite cardinal says , since and has cardinality (Cantor's theorem: , Fleissner's HYP covering interface); this is the form of CH consumed by CH yields a normal nonmetrizable Moore space.
proves that a normal nonmetrizable Moore space exists (CH yields a normal nonmetrizable Moore space).
Proof
Assume . By [F1] both AC and GCH hold.
By [F2], GCH gives , i.e. CH.
By [F3], applied under CH, there is a normal nonmetrizable Moore space.
A normal Moore space that is not metrizable is a counterexample to the normal Moore space conjecture, so refutes it.
Depends on
Used by
Nothing in the library uses this result yet.
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
- Fleissner, Normal nonmetrizable Moore space from continuum hypothesis or nonexistence of inner models with measurable cardinals (standard reference, not scraped)