crossDistSpectrum
plain-language theorem explainer
The cross-distance spectrum of two finite planar point sets is the finite set of Euclidean distances realized between a point of the first set and a point of the second. Anyone citing the bipartite Erdős distinct-distances problem or the RS two-channel range experiment uses this alphabet as the raw observable. It is defined by taking the image of the Cartesian product under the Euclidean distance map; the construction is classical and noncomputable only because real distance is.
Claim. For finite $P,Q\subset\mathbb{R}^2$, the cross-distance spectrum is the finite set $\{\|p-q\|:p\in P,\,q\in Q\}\subset\mathbb{R}_{\ge 0}$.
background
The ambient module physicalizes Erdős problem #661 as a two-channel range-spectrum question: two finite planar channels are coupled by Euclidean propagation delay, and the classical distance count is the alphabet size of the cross-coupling spectrum. Points live in Point2, the Euclidean plane $\mathbb{R}^2$ (as EuclideanSpace ℝ (Fin 2)).
The doc-comment distinguishes this unsquared alphabet from its squared sibling: squaring is often cleaner algebraically, but both alphabets carry the same asymptotic information away from sign issues because distance is nonnegative. Downstream, a two-channel range experiment packages sources and detectors in the visible plane and reads out exactly this cross-coupling alphabet.
proof idea
Pure definition, not a proof. Under classical choice, form the Cartesian product of the two finite sets and push it forward by the map $(p,q)\mapsto \mathrm{dist}(p,q)$. The result is a finite set of reals. No lemmas are invoked beyond Mathlib's Finset.product, Finset.image, and Euclidean dist.
why it matters
This is the raw observable for the module's RS reading of Erdős #661. The positive formulation asks whether two $n$-point planar channels can have cross-distance alphabet $o(n/\sqrt{\log n})$; the negative RS target (planar cross-spectrum rigidity) asserts a matching lower bound at the square-grid scale. Both propositions quantify the cardinality of this spectrum, and the two-channel range experiment structure exposes it as the physical readout.
In framework terms the construction sits in the mathematics layer that supports discrete geometric constraints on recognition channels: a single positive-definite planar carrier cannot supply true two-sector orthogonality, so the grid-scale lower bound is the expected rigid outcome. The definition itself settles no open question; it names the alphabet those questions count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.