Residual Complement of the Canonical Completion Image

Abstract

A countable perfect metric space has a negligible image in its completion.

Theorem 1.1 (The canonical completion image has residual full-measure complement).

$$\begin{gathered} \forall N,\mu , \\ [\mathrm{MetricSpace}(N)],[\mathrm{Countable}(N)],[\mathrm{PerfectSpace}(N)], \\ [\mathrm{NoAtoms}(\mu )],[\mathrm{IsProbabilityMeasure}(\mu )], \\ \mathrm{DenseRange}(co{e}_N)\wedge \\ \mathrm{PerfectSpace}(\mathrm{Completion}(N))\wedge \\ \mathrm{IsMeagre}(\mathrm{range}(co{e}_N))\wedge \\ \mu (\mathrm{Completion}(N)\setminus \mathrm{range}(co{e}_N))=1. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S0/Naming/Conservation/CompletionEmbeddingResidual.completion_embedding_residual_full_measure (✓ std3). ∎

Source. Repository-derived.

Commentary.

The absence of isolated points is assumed for N and proved for its completion. Density alone is clause (i), already carried by the frozen CompletionEmbeddingDense declaration.

The proof transfers preperfectness through the canonical embedding. Its dense closure is the whole completion, so the completion is a perfect space. Countability then writes the image as a countable union of nowhere-dense singletons.

An atomless measure assigns zero measure to the countable image. Probability normalization therefore gives measure one to its complement.

This declaration discharges clauses (ii) and (iii). It does not claim coverage of the residual atom. D5-T0032 remains open because the existing formalization receipt is misbound and may be corrected only through the receipt-correction door.

References

• Truth anchor: D5/S0/Naming/Conservation/CompletionEmbeddingResidual.completion_embedding_residual_full_measure
• Dependency: D5/S0/Naming/CompletionEmbeddingDense