TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22

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.

HYP produces a normal nonmetrizable Moore space

Statement

$Z F C + H Y P$ proves that there is a normal nonmetrizable Moore space (Fleissner's HYP covering interface, Fleissner's construction of a normal nonmetrizable Moore space from level data).

Facts & Assumptions

Given: Witnesses $κ, (κ_{n})_{n \in ω}, E$ for HYP and fixed ladders $(δ_{i})_{i \in ω}$ for $δ \in E$ (Fleissner's HYP covering interface).

[F1]

HYP asserts that $κ$ is an infinite cardinal, that $(κ_{n})_{n \in ω}$ is an increasing sequence of cardinals, and the conjunction of clauses (1a), (1b), (2), (3a), (3b): $\sup_{n} κ_{n} = κ$ ; $2^{κ_{n}} < κ$ for every $n$ ; $2^{κ} = κ^{+}$ ; $E \subseteq {δ < κ^{+} : cf (δ) = ω}$ is stationary in $κ^{+}$ ; and $E \cap β$ is not stationary in $β$ for every $β < κ^{+}$ with $cf (β) > ω$ (Fleissner's HYP covering interface, Cardinal (initial ordinal) and cardinality).

[F2]

Lemma 1 from the same hypotheses: for every $β < κ^{+}$ there is $m_{β} : E \cap β \to ω$ such that $δ_{i} \neq η_{i}$ for all distinct $δ, η \in E \cap β$ and all $i \geq \max (m_{β} (δ), m_{β} (η))$ (Ladder separation from HYP).

[F3]

The construction of Fleissner's construction of a normal nonmetrizable Moore space from level data converts exactly the data of [F1] together with [F2] into a normal nonmetrizable Moore space (Moore spaces and developments, Metrizable spaces are collectionwise normal).

Proof

technique · direct

1.1

Assume HYP. Then $κ$ is infinite, $(κ_{n})$ is increasing, and clauses (1a), (1b), (2), (3a) of [F1] hold for the given $κ$ , $(κ_{n})$ , and $E$ .

givenF1

2.1

The separation conclusion of [F2] holds for the fixed ladders. Its proof uses clause (3b) at limit ordinals of uncountable cofinality and uses clause (3a) to obtain an automatic successor club at countable-cofinality stages.

step 1.1F1F2

3.1

Steps 1.1 and 2.1 put all hypotheses of the construction of [F3] at the given parameters, so there is a normal nonmetrizable Moore space.

step 1.1step 2.1F3∎

Remarks

HYP is used only through [F2]. The source says so explicitly ("we will not use (3b) directly, but rather the following consequence"), and the construction of [F3] is stated with the separation conclusion as an hypothesis, so the formal dependency is exact.
The case $κ = ω$ is covered by the same item. When HYP holds with $κ = ω$ the clause (1b) is literal cardinal arithmetic on finite ordinals and the separation conclusion is supplied by Ladder separation from HYP like every other instance; the CH case with nonreflecting failure is treated separately in CH yields a normal nonmetrizable Moore space.

Depends on

Used by

NMSC gives an inner model with a measurable cardinal Theorem

Dependency tree · two levels

52 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

William G. Fleissner, If all normal Moore spaces are metrizable, then there is an inner model with a measurable cardinal (standard reference, not scraped)