orderedDistanceSpectrum
plain-language theorem explainer
For a finite planar point set A, the ordered distance spectrum is the finite set of all Euclidean distances realized by ordered pairs of distinct points. It is the basic carrier of shell data in the RS reading of Erdős #132: each positive distance is a two-body recognition-energy shell. The definition is a one-line image of the ordered non-diagonal pair events under the distance map.
Claim. For a finite set $A$ of points in the Euclidean plane, the ordered distance spectrum is the finite set $\{ d(p,q) : p,q \in A,\, p \neq q \} \subset \mathbb{R}$.
background
This module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean distance set; in RS it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity. For any positive distance, ordered multiplicity is exactly twice the unordered multiplicity, so classical thresholds of the form $\le n$ become $\le 2n$.
Points live in Point2, the Euclidean plane $\mathbb{R}^2$. The upstream helper orderedPairEvents A is the finite set of ordered pairs $(p,q)\in A\times A$ with $p\neq q$. The spectrum is that set pushed forward by the Euclidean distance map. Diameter shells and sparse-shell predicates are later defined by quantifying over membership in this spectrum.
proof idea
Definitional one-liner under classical choice: take the image of orderedPairEvents A under the map $(p,q)\mapsto \mathrm{dist}(p,q)$. No lemmas are applied; the body is exactly that image construction.
why it matters
This is the ambient finite set of occupied distance shells for the whole DistanceShellMultiplicity development. Downstream, IsDiameterShell A r asserts that $r$ lies in the spectrum and is maximal among spectrum members; dist_le_of_diameter_shell then bounds every pairwise distance by that diameter. DeepLayerCase quantifies over spectrum members other than the diameter when demanding that no second sparse shell has been found. Existence of a diameter for large $|A|$ (diameter_shell_exists_eventually_holds) is pure bookkeeping on a nonempty finite spectrum. Occupancy counts, non-diameter pressure lemmas, and the four-point/local-meeting bridges all read distances from this set. In the RS framing it is the discrete support of two-body recognition-energy shells underlying the Erdős #132 physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.