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.

No inner measurable implies Fleissner's HYP

Statement

$Z F C$ plus "there is no inner model with a measurable cardinal" proves HYP with the parameters needed by Fleissner (Fleissner's HYP covering interface, Dodd-Jensen covering supplies Fleissner HYP data).

Facts & Assumptions

Given: The hypothesis that no inner model contains a measurable cardinal.

[F1]

That hypothesis supplies the Dodd-Jensen covering and square package and, from it, a singular strong limit $κ$ of cofinality $ω$ with $2^{κ} = κ^{+}$ and a nonreflecting stationary $E \subseteq {δ < κ^{+} : cf (δ) = ω}$ (Dodd-Jensen covering supplies Fleissner HYP data).

[F2]

HYP is the conjunction of clauses (1a), (1b), (2), (3a), (3b) for some $κ, (κ_{n}), E$ (Fleissner's HYP covering interface).

Proof

technique · direct

1.1

Assume no inner model contains a measurable cardinal. By [F1] there are $κ, (κ_{n})$ and $E$ with $2^{κ} = κ^{+}$ , $2^{κ_{n}} < κ$ for all $n$ , $\sup_{n} κ_{n} = κ$ , $E$ stationary in $κ^{+}$ inside ${δ < κ^{+} : cf (δ) = ω}$ , and $E$ nonreflecting.

givenF1

2.1

These objects satisfy every clause of [F2], so HYP holds with exactly the parameters, namely $κ, (κ_{n})_{n \in ω}$ and the nonreflecting stationary $E$ , that the Fleissner construction consumes.

step 1.1F2∎

Remarks

This is a repackaging item. It records that the parameters produced by the covering route are the parameters HYP asks for; no new mathematics beyond the identification of the clauses is claimed.

Depends on

Used by

NMSC gives an inner model with a measurable cardinal Theorem

Dependency tree · two levels

12 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)