Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31
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.

Under choice, every metrizable space has w(X)=d(X)

Statement

Assuming choice, every metrizable space satisfies w(X)=d(X) under the raw convention.

Facts & Assumptions

Given: The Axiom of Choice, a metric inducing the topology of X, and a dense set D of least cardinality κ=d(X).

[L2]

The rationals are countably infinite and lie densely between reals (Q is countably infinite, The rationals embed densely in the reals).

Proof

technique · direct
1.1

Suppose first that κ is infinite. The family B={B(d,q):d∈D, q∈Q, q>0} has cardinality at most κ⋅ℵ0=κ by [L2] and [L3]. It is a basis: if x∈U with U open, choose ε>0 with B(x,ε)⊆U, choose d∈D with d(x,d)<ε/3, and then by [L2] choose a positive rational q with d(x,d)<q<ε−d(x,d). Thus x∈B(d,q)⊆B(x,ε)⊆U. Hence w(X)≤κ=d(X).

givenL2L3
1.2

Suppose κ is finite. If D=∅, density forces X=∅ and both raw invariants are 0. Otherwise X=D: if x∉D, the finitely many positive distances d(x,a) for a∈D have a positive minimum, and a smaller ball about x misses D, contradicting density. A finite metric space is discrete, since at each point a ball smaller than all distances to the other finitely many points is a singleton. The singleton family is a basis of size ∣X∣, and every basis of a discrete space must contain each singleton; also every dense set must contain every point. Therefore w(X)=∣X∣=d(X)=κ.

given
2.1

Step 1.1 handles infinite density and step 1.2 handles finite density; combining the resulting upper bound with [L1] gives w(X)=d(X) in every case.

step 1.1step 1.2L1∎

Depends on

Used by

Dependency tree · two levels

76 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