Alphabeta Math
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 rational metric space is not metacompact

Facts & Assumptions

Given: The atom space UQ< in its model, the open cover U={B(c,1/2):cA}, and a supposed point-finite open refining cover.

[F1]

The model is a ZFA model in which every set has a finite support; an element of the model has a finite support EA fixed by the automorphisms used below (Corson's ordered-rational permutation model, Permutation groups, stabilizers, supports, and normal filters).

[F2]

UQ< is universal and ultrahomogeneous for finite ordered rational metric spaces: every finite such space embeds in it, and every finite partial isometry preserving the order extends to an automorphism of the whole space. [given, source]

[L1]

Every member of a refinement of U has diameter at most 1: if VB(c,1/2) and x,yV, then d(x,y)<1 by the triangle inequality. The radius-1/2 balls form an open cover (Open ball, closed ball and sphere in a metric space, 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, Metric space: d(x,y)=0 iff x=y, symmetry, and the triangle inequality; pseudometric and ultrametric).

[L2]

If V is open and aV, then some positive-radius metric ball about a is contained in V; shrinking the radius to 1/m for a sufficiently large integer m1 preserves the inclusion (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).

Proof

technique · contradiction
1.1

Suppose U has a point-finite open refining cover V. Since V is a set of the model, fix a finite support EA of V by [F1]. Enlarge E by one atom if necessary, so that E is nonempty, without destroying the support property. Let D be the diameter of E.

assume-contraL1F1
2.1

By universality in [F2], choose aAE such that e<a and d(a,e)=D+4 for every eE. Fix an arbitrary integer n1. Since V covers A, choose VV with aV; by [L2], choose an integer m1 with B(a,1/m)V, and put K:=nm.

step 1.1F2L2
3.1

Extend E{a}, using [F2], by points a0<<a3K=a such that d(ai,e)=D+4 for eE and d(ai,aj)=ij/K for 0i,j3K. These prescriptions form a finite ordered rational metric space: the old-to-new distances are constant and exceed the diameter of both E and the new chain. Ultrahomogeneity then extends the partial isometry fixing E and sending ai to ai+1 for 0i<3K to an automorphism φ. Since E supports V, every φj(V) belongs to V.

step 2.1F2F1
4.1

The points a3Kn+1,,a3K lie in B(a,1/m)V, because their distances from a=a3K are all strictly less than n/K=1/m. Hence aφj(V) for every 0j<n.

step 2.1step 3.1
5.1

By [L1], V has diameter at most 1. Consequently, if aiV, then i2K. Let L be the least index with aLV. Step 4.1 gives 2KL3Kn+1. For 0j<n, one has aL+jφj(V). Moreover, if Ki<L+j, then aiφj(V): otherwise aij=φj(ai) would lie in V, while 0ij<L, contradicting the minimality of L.

L1step 3.1step 4.1
6.1

The members φj(V) for 0j<n are pairwise distinct. Indeed, for j<j<n, the point aL+j belongs to φj(V), whereas step 5.1, applied with i=L+j<L+j, shows that it does not belong to φj(V). Thus, for every n1, the map jφj(V) injects n into {WV:aW}. The set on the right is therefore not finite, contradicting point-finiteness at a. Hence U has no point-finite open refining cover, so the space is not metacompact and, a fortiori, not paracompact.

step 4.1step 5.1discharge-contradiction

Depends on

Used by

Dependency tree · two levels

24 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