Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27
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.

The completion of Q under the usual metric is R

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice (ACω)). Regard Q (The rationals as equivalence classes of pairs of integers) as the subset Q^ of R that is the image of the canonical embedding q↦q^ (The rationals embed densely in the reals), carrying the subspace metric dQ(p,q)=∣p^−q^∣ inherited from the usual metric of R (The absolute value makes R a metric space: d(x,y)=∣x−y∣ is a metric, its open balls are the intervals (x−r,x+r), and it is unbounded, Isometry, isometric embedding, and the subspace metric on a subset). Let ι:Q→R be that embedding.

Then ((R,dR),ι) is a completion of (Q,dQ) (A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace). Consequently, by uniqueness of completions (A completion is unique up to a unique isometry fixing the original space, and uniformly continuous maps into complete spaces extend through it), for every completion ((Y^,d^),j) of (Q,dQ) there is exactly one continuous φ:R→Y^ with φ∘ι=j, and it is an isometry. In this sense R is the completion of Q.

Facts & Assumptions

Given: The Axiom of Countable Choice; Q with the metric dQ inherited from R through ι:q↦q^; a real x; a real r>0.

[A1]

Countable Choice has the meaning fixed in The Axiom of Countable Choice (ACω).

[L1]

q↦q^ is an injective, order-preserving embedding of ordered fields, and strictly between any two reals lies a rational (The rationals embed densely in the reals).

[L3]
[L5]

Density: A is dense in X when every ball around every point of X meets A (Interior, closure, boundary, limit point, isolated point and dense subset of a metric space).

[L6]

A completion is a complete space together with an isometric embedding with dense image, and under Countable Choice two completions are related by a unique compatible isometry (A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace, A completion is unique up to a unique isometry fixing the original space, and uniformly continuous maps into complete spaces extend through it).

Verification

technique · direct
1.1

dQ is a metric on Q and ι is an isometric embedding into (R,dR): by construction dR(ι(p),ι(q))=∣p^−q^∣=dQ(p,q), and ι is injective.

L1L2L3
1.2

(R,dR) is complete.

L4
1.3

ι[Q] is dense in R: for a real x and a real r>0 the ball B(x,r) is the interval (x−r,x+r), which is nonempty and has x−r<x+r, so it contains a rational; hence every ball around every real meets ι[Q].

L1L2L5
2.1

So the complete space (R,dR), together with the isometric embedding ι whose image is dense, is a completion of (Q,dQ).

step 1.1step 1.2step 1.3L6
3.1

By [A1] and uniqueness of completions, any other completion ((Y^,d^),j) of (Q,dQ) receives exactly one continuous φ:R→Y^ with φ∘ι=j, and that φ is an isometry.

step 2.1A1L6∎

Remarks

  • This is the metric statement of what the construction pages did by hand. This library builds R out of Cauchy sequences of rationals on its own page, and the general construction of Every metric space has a completion, constructed as the equivalence classes of its Cauchy sequences follows the same plan for an arbitrary metric space: classes of Cauchy sequences, with the distance read off as a limit. The present item is the observation that, run on Q, that plan reaches a space isometric to the R already in hand, and that no separate verification of "which complete space it is" is needed once uniqueness is available.
  • Density is the whole of the third condition, and it is exactly the Archimedean fact. That every interval of positive length contains a rational is The rationals embed densely in the reals; without it Q would sit inside R as a complete-looking but small subspace, and R would not be a completion of it but merely a complete space containing it.
  • The metric is the one written above and no other. Completions are taken with respect to a named metric (A completion of a metric space: a complete metric space together with an isometric embedding onto a dense subspace), and a different metric on Q would in general have a different completion; nothing here is a statement about Q as a bare field or as a bare topological space.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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