LemmaStatement: 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.

Corson's Stone obstruction is ordinal boundable

Statement

The sentence asserting that there is a rational-valued metric space with an open cover having no point-finite open refining cover is an atom-blind boundable sentence in the sense of Boundable sentences over an atom set, with the explicit absolute bound $ω + 41$ of the source's Lemma 5.

Facts & Assumptions

Given: Corson's model and the covering failure certified in Corson's rational metric space is not metacompact.

[F1]

A formula $φ (\vec{x})$ is boundable when a fixed absolutely defined ordinal $α$ makes ZFA prove $φ (\vec{x}) \leftrightarrow φ^{V_{α} (⋃ \vec{x})} (\vec{x})$ ; its existential closure is then a boundable sentence (Boundable sentences over an atom set).

[F2]

The metric space is the ordered rational Urysohn space of Corson's ordered-rational permutation model, its metric is rational-valued, and its open cover has no point-finite refinement (Corson's rational metric space is not metacompact, Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric, Metacompactness: every open cover has a point-finite open refinement).

[L1]

With the standard set encodings, $ω \in V_{ω + 1} (\emptyset)$ , and successively constructing $(ω, +)$ , $Z$ , $(Z, +)$ , $Q$ , and $(Q, +)$ puts $(Q, +)$ in $V_{ω + 30} (\emptyset)$ . [source, Corson Lemma 5]

[L2]

With Kuratowski ordered pairs, each $(x, y)$ for $x, y \in X$ lies in $V_{2} (X)$ , so the set $X \times X$ of all those pairs lies in $V_{3} (X)$ , not necessarily in $V_{2} (X)$ . The larger stated bounds remain valid: the pure rational codebook from [L1] dominates this one-level correction, so a function $d : X \times X \to Q$ lies in $V_{ω + 33} (X)$ ; a family of subsets of $X$ lies in $V_{2} (X)$ ; an ordered triple $(X, d, U)$ lies in $V_{ω + 37} (X)$ ; and a function from a natural number into an open cover of $X$ lies in $V_{ω + 41} (X)$ . [L1, source, Corson Lemma 5]

Proof

technique · direct

1.1givenF1F2

Let $Cov (X, d, U)$ say that $d$ is a rational-valued metric on $X$ and $U$ is an open cover in its metric topology. Let $Ref (X, d, U, V)$ say that both $U$ and $V$ satisfy $Cov$ and that $V$ refines $U$ . Let $Inj (f, Y, Z)$ say that $f$ is an injection from $Y$ into $Z$ . These are formulas built only from equality, membership, the carried sets, and the fixed pure rational codebook.

2.1step 1.1

Define $Φ (X, d, U)$ to be $Cov (X, d, U)$ together with the assertion that for every $V \in P (P (X))$ , if $Ref (X, d, U, V)$ , then some $x \in X$ has the following property: for every $n \in ω$ there is $f \subseteq n \times V$ such that $Inj (f, n, V)$ and $x \in f (m)$ for every $m < n$ . Thus $Φ$ says exactly that $U$ has no point-finite open refining cover.

3.1step 2.1L1L2

The bounds [L1]-[L2] contain every object quantified in step 2.1: candidate covers and refinements lie in the second relative level over $X$ , while every finite injection witnessing arbitrarily many members through $x$ lies below level $ω + 41$ . Expanding the displayed definitions therefore gives the ZFA theorem $Φ (X, d, U) \leftrightarrow Φ^{V_{ω + 41} (X \cup d \cup U)} (X, d, U)$ .

3.2step 1.1step 2.1

The formula is atom-blind: its base sort $X$ is used only opaquely through the carried metric, subsets, covers, and finite function graphs; its atomic tests are equality and membership together with the fixed pure rational parameter, and it never tests whether an element of $X$ is an atom or inspects its internal membership structure.

4.1step 3.1step 3.2F1F2∎

By [F1] and step 3.1, the existential closure $\exists X \exists d \exists U Φ (X, d, U)$ is boundable with the fixed absolute bound $ω + 41$ ; step 3.2 supplies the atom-blind typed certificate, and [F2] supplies a witness in Corson's model.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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

Samuel Corson, The Independence of Stone's Theorem from the Boolean Prime Ideal Theorem (standard reference, not scraped)