Separability of the existing rooted GHP metric

A finite net approximates the entire compact carrier, sends its probability measure to the net, and sends its root to the chosen covering point. Rounded distance and mass arrays, together with the finite index of this root, give countably many codes. Equal codes control the actual rooted GHP distance.

The finite approximation costs at most three radii. Matching rooted finite codes costs at most four radii: the common-source gluing contributes three, and correcting the measure in the same target carrier contributes one. Thus two approximations and the code comparison cost ten radii.

This proves second countability for the existing metric quotient, without introducing another metric or discarding points of zero mass. The root need not lie in the measure support. The finite-net and coding arguments adapt Freezing2/Geometry/GHPSeparability.lean and GHPFiniteCoding.lean in igor-kortchemski/uniform-attachment-freezing-scaling-limits, commit 8bace72d36cdf7d250414f3d98acfaa415de23d9 (Apache-2.0).

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

Countable rounded distance, mass and root data determine a rooted class to any accuracy.

instance BGW.MetricMeasure.RootedMeasuredGHSpace.instSecondCountableTopology : SecondCountableTopology RootedMeasuredGHSpace

The topology of the existing rooted GHP metric quotient is second countable.

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

The existing rooted GHP metric has a countable dense subset.