TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22‡ rests on unproved material (inherited)

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.

‡ Rests on 2 statements not proved in this library, by way of the results it cites. This item cites no such statement directly; it depends on results that do. The unproved premises it inherits are ‡ Under choice, every metric space has a σ-discrete basis and ‡ Under choice, a regular T₁ space with a σ-locally-finite basis has a compatible normal sequence. Each is recorded with a citation to the literature and is not established here, because the track that would prove it has not yet been developed in this library. Everything else in this proof is proved here.

A strongly compact cardinal gives the NMSC consistency upper bound

Statement

$Con (Z F C + there is a strongly compact cardinal)$ implies $Con (Z F C + N M S C)$ , where NMSC is the normal Moore space conjecture. No ground-model implication and no actual strongly compact cardinal is asserted (Strong compactness and the product-measure extension interface).

Facts & Assumptions

Given: The metatheoretic assumption $Con (Z F C + a strongly compact cardinal)$ .

[F1]

The published product-measure interface: $Con (Z F C + a strongly compact cardinal)$ implies $Con (Z F C + P M E A)$ , the PMEA sentence being exactly the full-domain extension axiom of PMEA and PMEA-sigma (Strong compactness and the product-measure extension interface).

[F2]

$Z F C + P M E A$ proves NMSC (PMEA implies the normal Moore space conjecture).

[F3]

If an arithmetic base $B$ verifies a total code map $r$ and $\forall p ({Prf}_{U} (p, ⌜ ⊥ ⌝) \to {Prf}_{T} (r (p), ⌜ ⊥ ⌝))$ , then $B ⊢ Con (T) \to Con (U)$ (Formal consistency transfer from a verified reduction).

[F4]

Both theories are formulated over $Z F C$ with $A C$ explicit (The Axiom of Choice).

Proof

technique · direct

1.1

Assume $Con (Z F C + a strongly compact cardinal)$ .

given

1.2

Put $T_{0} : = Z F C + P M E A$ and $U : = Z F C + N M S C$ . By [F2], fix a finite $T_{0}$ -proof $q$ of NMSC. Define $r$ on codes of $U$ -proofs by scanning the finite proof, copying logical and ZFC axiom lines and inference steps, and replacing every use of the added NMSC axiom by the fixed proof $q$ , with line references renumbered. This is a total primitive-recursive code map. The chosen arithmetic proof checker verifies by induction on the length of the input proof that every copied line remains valid and every replaced line is the conclusion of $q$ ; hence it verifies ${Prf}_{U} (p, ⌜ ⊥ ⌝) \to {Prf}_{T_{0}} (r (p), ⌜ ⊥ ⌝)$ for every $p$ .

F2F3F4construct

2.1

By [F1] the theory $Z F C + P M E A$ is consistent.

step 1.1F1

2.2

Apply [F3] to the verified map $r$ of [step 1.2]. It gives $Con (T_{0}) \to Con (U)$ , that is, $Con (Z F C + P M E A) \to Con (Z F C + N M S C)$ .

step 1.2F3

3.1

Chaining steps 1.1, 2.1 and 2.2 gives the displayed implication, under the metatheoretic consistency assumption only.

step 2.1step 2.2∎

Remarks

Three distinct claims are kept apart. "PMEA implies NMSC" is a theorem of $Z F C$ ; the consistency transfer is metatheoretic; and the strongly compact cardinal is assumed only inside the consistency hypothesis.
AC is used in the supplier, in the random-real construction and in the cardinal arithmetic; it is declared as a dependency and no choice-free reading is claimed.

Depends on

Used by

The consistency-strength sandwich for NMSC 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

D. H. Fremlin, Real-valued-measurable cardinals (standard reference, not scraped)