Pipeline-generated

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.

Normal Moore Spaces, PMEA, and Consistency Strength: Examples

1 · Prerequisites

2 · Summary

Worked examples for the normal Moore space pair. The page computes the stars of the standard metric covers by balls of radius $2^{- n}$ and verifies the two inclusions that make them a development, so that every metric space is a Moore space; and it computes the three-quarter event estimate in the PMEA separation argument, where two good events of measure above three quarters and a two-coordinate difference event of measure one half overlap in a point that separates the two chosen neighbourhoods. The false statement records the relative-consistency refutation of " $Z F C$ proves NMSC": CH yields a normal nonmetrizable Moore space, so assuming $Con (Z F C)$ , $Z F C$ does not prove the normal Moore space conjecture.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-adaptedaudited 2026-09-22Open item page →

Development stars form a countable local base

Example

Let $(X, d)$ be a metric space (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric) with its metric topology (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement). For $n \in N$ let $G_{n} : = {B (x, 2^{- n}) : x \in X},$ the cover by open balls of radius $2^{- n}$ (Open ball, closed ball and sphere in a metric space). The example computes the stars $St (x, G_{n})$ and verifies that $(G_{n})$ is a development, so that every metric space is a Moore space in the sense of Moore spaces and developments.

Facts & Assumptions

Given: A metric space $(X, d)$ , its balls $B (x, r)$ , and the covers $G_{n} = {B (x, 2^{- n}) : x \in X}$ .

[F1]

Star: $St (x, G_{n}) = ⋃ {B (z, 2^{- n}) : x \in B (z, 2^{- n})}$ , and each $G_{n}$ is an open cover because $x \in B (x, 2^{- n})$ and every metric ball is open (Refinements, locally finite families, point-finite families, and star refinements, Open ball, closed ball and sphere in a metric space, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, claim 1).

[L1]

Metric axioms: $d (x, y) = 0$ if and only if $x = y$ , symmetry, and the triangle inequality $d (x, y) \leq d (x, z) + d (z, y)$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

A set is open in the metric topology exactly when each of its points has a ball inside it, and balls are open (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Arbitrary unions and finite intersections of open sets are open, open balls are open and closed balls are closed, claim 1).

[L3]

A space carrying its metric topology is metrizable, and every metrizable space is $T_{3}$ , hence regular $T_{1}$ (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not, In a metric space every closed set is a zero set and a $G_{δ}$ , and the distance function separates a point from a closed set, so every metrizable space is Tychonoff and perfectly normal, claim 4).

[L4]

For every $ε > 0$ some integer $m \geq 1$ satisfies $1 / m < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[L5]

A development is a sequence of open covers whose stars refine every open neighbourhood at each point; a Moore space is regular $T_{1}$ and developable. These stars give a countable local base, also for neighbourhoods that are not open (Moore spaces and developments, Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open).

Verification

technique · direct

1.1

For every $x$ and $n$ one has $B (x, 2^{- n}) \subseteq St (x, G_{n}) \subseteq B (x, 2^{1 - n})$ : the first inclusion holds because $x \in B (x, 2^{- n})$ ; for the second, if $y \in B (z, 2^{- n})$ with $x \in B (z, 2^{- n})$ then $d (x, y) \leq d (x, z) + d (z, y) < 2^{- n} + 2^{- n} = 2^{1 - n}$ by [L1].

givenF1L1

2.1

Hence $(G_{n})$ is a development. Let $U$ be open and $x \in U$ (Neighbourhood of a point and neighbourhood base, with this library's convention that a neighbourhood need not be open). By [L2] there is $ε > 0$ with $B (x, ε) \subseteq U$ ; take $m \geq 1$ with $1 / m < ε$ by [L4] and set $n = m + 1$ . Induction gives $2^{m} \geq m$ , so $2^{1 - n} = 2^{- m} \leq 1 / m < ε$ ; then step 1.1 gives $St (x, G_{n}) \subseteq B (x, 2^{1 - n}) \subseteq B (x, ε) \subseteq U$ .

step 1.1L2L4L5

3.1

Consequently every metric space is developable, and [L3] makes it regular $T_{1}$ , so it is a Moore space; the star family ${St (x, G_{n}) : n \in N}$ is the countable local base at $x$ supplied by step 2.1: each star is open as a union of open balls and contains $x$ , and every neighbourhood contains an open neighbourhood to which step 2.1 applies. If $X$ is empty, the covers are empty and the assertions about points are vacuous.

step 1.1step 2.1L2L3L5∎

Remarks

The star bound doubles the radius. The lower bound shows the star is not smaller than the ball of radius $2^{- n}$ , and the upper bound shows it is contained in the ball of radius $2^{1 - n}$ ; that two-to-one gap is exactly what makes the development property hold with the factor $2$ .
The same computation works with any null sequence of radii, the powers $2^{- n}$ being chosen only for definiteness.

ExampleConstruction: AI-generatedVerification: AI-generatedaudited 2026-09-22Open item page →

The three-quarter event calculation in the PMEA proof

Example

Let $ν$ be a full extension of a fair-coin product measure on $2^{I}$ (PMEA and PMEA-sigma) and let $E, F, D \subseteq 2^{I}$ be sets with $ν (E) > 3 / 4$ , $ν (F) > 3 / 4$ and $ν (D) = 1 / 2$ , where $D = {z : z (i) \neq z (j)}$ is the difference event of two distinct coordinates $i \neq j$ . The example computes that $ν (E \cap F) > 1 / 2$ and $ν (E \cap F \cap D) > 0$ . This is only the measure-theoretic calculation consumed by the separation lemma; the lemma's additional definitions relate its good events to disjoint neighbourhoods.

Facts & Assumptions

Given: A probability $ν$ on the full power set of $2^{I}$ , sets $E, F$ with $ν (E), ν (F) > 3 / 4$ , and a set $D$ with $ν (D) = 1 / 2$ .

[F1]

Probability and complement: $ν (A^{c}) = 1 - ν (A)$ for every $A$ , and $ν (2^{I}) = 1$ (PMEA and PMEA-sigma).

[L1]

Subadditivity for two or three sets: $ν (A \cup B) \leq ν (A) + ν (B)$ , hence for three sets as well (PMEA and PMEA-sigma).

[L2]

For distinct coordinates $i \neq j$ the difference event has $ν ({z : z (i) \neq z (j)}) = 1 / 2$ (PMEA and PMEA-sigma).

Verification

technique · direct

1.1

$ν (E \cap F) > 1 / 2$ : by [F1] and [L1], $1 = ν (E \cup F) + ν ((E \cup F)^{c}) \leq ν (E) + ν (F) + ν (E^{c} \cap F^{c})$ ; hence $ν (E \cap F) = 1 - ν (E^{c} \cup F^{c}) \geq 1 - (ν (E^{c}) + ν (F^{c})) > 1 - (1 / 4 + 1 / 4) = 1 / 2$ , since $ν (E^{c}) < 1 / 4$ and $ν (F^{c}) < 1 / 4$ by [F1].

givenF1L1

2.1

$ν (E \cap F \cap D) > 0$ : the complement of the triple intersection is contained in $E^{c} \cup F^{c} \cup D^{c}$ , which has measure at most $ν (E^{c}) + ν (F^{c}) + ν (D^{c}) < 1 / 4 + 1 / 4 + 1 / 2 = 1$ by [L1] and [F1] (using $ν (D^{c}) = 1 / 2$ ). Hence the triple intersection has positive measure and is nonempty.

step 1.1F1L1L2

3.1

Hence there exists $z \in E \cap F \cap D$ ; every such $z$ lies in both $E$ and $F$ and satisfies $z (i) \neq z (j)$ by the definition of $D$ . This example proves no topological conclusion from the abstract sets $E$ and $F$ : in The PMEA three-quarter separation estimate the separately defined good events and separating open sets give that conclusion.

step 2.1L2∎

Remarks

Strictness matters. Both good events have measure strictly above $3 / 4$ , so the complement of the triple intersection has measure strictly below $1$ ; with $\geq 3 / 4$ the conclusion $ν (E \cap F \cap D) > 0$ could fail.
Only two coordinates are used, through $ν (D) = 1 / 2$ .

False statementConstruction: Literature-sourcedVerification: AI-adaptedaudited 2026-09-22Open item page →

False: ZFC proves the normal Moore space conjecture

Statement

Relative to $Con (Z F C)$ , it is false that $Z F C$ proves the normal Moore space conjecture: $Z F C$ does not prove that every normal Moore space is metrizable.

Facts & Assumptions

Given: The metatheoretic hypothesis $Con (Z F C)$ and the fixed arithmetization of The standard certified provability predicate.

[F1]

$Con (Z F C)$ implies $Con (Z F C + C H)$ (Positive relative consistency of CH and GCH).

[F2]

Weakening, concatenation, and replacement of proved sentence premises by their proofs preserve derivability (Finite support, weakening, and composition of derivations).

[F3]

$Z F C + C H$ proves that there is a normal nonmetrizable Moore space (CH yields a normal nonmetrizable Moore space, Moore spaces and developments).

[F4]

$N M S C$ is the assertion that every normal Moore space is metrizable. [given]

Refutation

technique · direct

1.1

Assume $Con (Z F C)$ . Then $Con (Z F C + C H)$ directly by [F1].

givenF1

2.1

If $Z F C$ proved NMSC, weakening would give the same theorem in $Z F C + C H$ . But [F3] gives in that theory a normal nonmetrizable Moore space, contradicting NMSC; by the proof-composition operations of [F2], these two finite derivations concatenate to a $Z F C + C H$ refutation, contrary to [step 1.1].

step 1.1F2F3F4

3.1

Therefore, assuming $Con (Z F C)$ , no such refutation exists and $Z F C$ does not prove NMSC.

step 2.1discharge-contradiction∎

Remarks

The consistency hypothesis cannot be dropped. The conclusion is a relative statement; $Z F C$ itself cannot prove $Con (Z F C)$ (The standard certified provability predicate).
The failure is not a theorem of $Z F C$ alone. The witness space is produced under CH; under PMEA every normal Moore space is metrizable (PMEA implies the normal Moore space conjecture), so the statement is independent in the usual relative-consistency sense.

Normal Moore Spaces, PMEA, and Consistency Strength: Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Development stars form a countable local base

Example

Facts & Assumptions

Verification

Remarks

The three-quarter event calculation in the PMEA proof

Example

Facts & Assumptions

Verification

Remarks

False: ZFC proves the normal Moore space conjecture

Statement

Facts & Assumptions

Refutation

Remarks

Sources