Separability of the whole-space GHP metric

Each measured isometry class has a representative, a finite net covering its entire carrier, and the exact pushforward of its measure to that net. Rounded distance and atomic-weight arrays form countably many codes. Equal codes control the finite measured spaces and hence the original classes. This constructs a countable basis for the existing GHP topology without discarding zero-mass points or assuming a Polish-space result.

Adapted from Freezing2/Geometry/GHPSeparability.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

theorem BGW.MetricMeasure.MeasuredGHSpace.exists_countable_discretization (δ : ℝ) (hδ : 0 < δ) : ∃ (β : Type) (x : Encodable β) (F : MeasuredGHSpace → β), ∀ (p q : MeasuredGHSpace), F p = F q → dist p q ≤ δ

Countable finite data reconstruct a compact measured isometry class to any prescribed GHP accuracy.

instance BGW.MetricMeasure.MeasuredGHSpace.instSecondCountableTopology : SecondCountableTopology MeasuredGHSpace

The exact GHP topology on the source's whole-space measured-isometry quotient is second countable.

theorem BGW.MetricMeasure.MeasuredGHSpace.separableSpace : TopologicalSpace.SeparableSpace MeasuredGHSpace

In particular, the genuine GHP metric has a countable dense subset.