TheoremStatement: Literature-sourcedProof: Literature-sourcedPipeline-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.

Dodd-Jensen covering supplies Fleissner HYP data

Statement

In $Z F C$ , if there is no inner model with a measurable cardinal, then the Dodd-Jensen covering and square package (The Dodd-Jensen covering and square package) supplies a singular strong limit cardinal $κ$ of cofinality $ω$ with $2^{κ} = κ^{+}$ and a nonreflecting stationary set $E \subseteq {δ < κ^{+} : cf (δ) = ω}$ . Consequently HYP holds (Fleissner's HYP covering interface).

Facts & Assumptions

Given: The hypothesis that there is no inner model with a measurable cardinal, and the Dodd-Jensen covering and square package for the core model $K$ that this hypothesis supplies.

[F1]

The package: $Cov (V, K)$ ; GCH and square in $K$ ; an uncountable strong limit cardinal $κ$ of countable cofinality with $2^{κ} = κ^{+}$ and $□_{κ}$ ; $♢_{κ^{+}} (W)$ for $W = {α < κ^{+} : cf (α) = ω}$ ; and a stationary $E \subseteq W$ with $□_{κ} (E)$ (The Dodd-Jensen covering and square package).

[F2]

If $C$ is club in an ordinal $β$ of uncountable cofinality, then the set $acc (C)$ of its limit points is also club in $β$ ; closedness gives $acc (C) \subseteq C$ . The uncountable-cofinality qualification is essential: a club of order type $ω$ can have no limit points below its supremum. Here " $α$ is a limit point of $C_{β}$ " means $α = \sup (C_{β} \cap α)$ (Cardinal (initial ordinal) and cardinality).

[L1]

A cardinal $κ$ is a strong limit exactly when $2^{λ} < κ$ for every $λ < κ$ ; if in addition $cf (κ) = ω$ , then there is an increasing sequence of cardinals $(κ_{n})_{n \in ω}$ cofinal in $κ$ (Cardinal (initial ordinal) and cardinality, The successor cardinal $κ^{+}$ , the alephs $ℵ_{α}$ , the beths $ℶ_{α}$ , successor and limit cardinals, and the identifications $ℵ_{0} = ω$ and $ℵ_{1} = ω_{1}$ ).

[L2]

A $Σ_{1}$ -definable choice from the given data, e.g. $κ_{n} : = {(\sup_{m \leq n} 2^{γ_{m}})}^{+}$ for a fixed cofinal $ω$ -sequence $(γ_{n})$ in $κ$ , is legitimate, since a single sequence is chosen once and the rest is defined by a formula; only the initial choice of $(γ_{n})$ uses the axiom of choice (The Axiom of Choice).

Proof

technique · direct

1.1

Assume there is no inner model with a measurable cardinal; by [F1] the package provides $κ$ with $2^{κ} = κ^{+}$ , $□_{κ}$ , $♢_{κ^{+}} (W)$ and a stationary $E \subseteq W$ with $□_{κ} (E)$ .

givenF1

2.1

Clause (2) of HYP holds: $2^{κ} = κ^{+}$ by step 1.1.

step 1.1

2.2

Clause (1) of HYP holds: $κ$ is an uncountable strong limit of countable cofinality by step 1.1, so [L1] and [L2] give an increasing sequence $(κ_{n})$ of cardinals cofinal in $κ$ with $2^{κ_{n}} < κ$ for every $n$ .

step 1.1L1L2

2.3

$E$ is stationary in $κ^{+}$ : it is stationary in $κ^{+}$ as a subset of $W$ by step 1.1, and $E \subseteq W \subseteq κ^{+}$ . Hence clause (3a) of HYP holds.

step 1.1

2.4

Clause (3b) holds. Suppose towards a contradiction that $E \cap β$ is stationary in some $β < κ^{+}$ with $cf (β) > ω$ . Let $⟨ C_{α} ⟩$ witness $□_{κ} (E)$ . By [F2], $acc (C_{β})$ is club in $β$ , so stationarity gives $α \in E \cap acc (C_{β})$ . But clause (iii) of $□_{κ} (E)$ says that every limit point of $C_{β}$ lies outside $E$ , a contradiction. Hence $E \cap β$ is nonstationary for every such $β$ , exactly as required by the local HYP interface.

step 1.1F2

3.1

By steps 2.1, 2.2, 2.3 and 2.4 the objects $κ, (κ_{n})_{n \in ω}, E$ satisfy clauses (1a), (1b), (2), (3a) and (3b) of the local interface. Thus HYP holds, with $κ$ singular of cofinality $ω$ and $E$ nonreflecting at every uncountable-cofinality stage as asserted.

step 2.1step 2.2step 2.3step 2.4∎

Remarks

The covering theorem is a declared input. Statements 1-2 of the package are the Dodd-Jensen covering theorem and the fine-structure of $K$ ; this item derives the HYP clauses from them and does not reprove them. The exact citations are in The Dodd-Jensen covering and square package.
Where the conclusion is used. HYP is the hypothesis of the construction of a normal nonmetrizable Moore space recorded elsewhere on this page, and hence of the inner-model lower bound for the normal Moore space conjecture.

Depends on

Used by

No inner measurable implies Fleissner's HYP Theorem

Dependency tree · two levels

29 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

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