StartingPreparation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Starting-pair preparation in every ambient dimension

This is prep:starting-pairs. It preserves the original distances in the classical-plane alternative, and fixes the Frostman gap and pair before choosing the later coarse partition parameter.

theorem OAI.Falconer.prepared_original_pair_or_positive_distance line 15