crossDistSqSpectrum
plain-language theorem explainer
The squared Euclidean distances realized between two finite planar point sets form a finite real alphabet (the cross-distance spectrum). Discrete geometers and Recognition Science two-channel analyses cite it as the raw alphabet whose cardinality is the Erdős #661 count. The definition is the image of the Cartesian product under squared distance, taken classically so the Finset API applies.
Claim. For finite sets $P,Q\subset\mathbb{R}^2$, the squared cross-distance spectrum is the finite set $\{\|p-q\|^2:p\in P,\,q\in Q\}\subset\mathbb{R}$.
background
The 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 distinct-distance count is the alphabet size of the cross-coupling spectrum. In RS terms the positive #661 direction asks whether that alphabet can be $o(n/\sqrt{\log n})$; the physical reading instead targets rigidity of the square-grid scale in a single positive-definite planar carrier.
Points live in the Euclidean plane: Point2 is $\mathbb{R}^2$ as EuclideanSpace $\mathbb{R}$ (Fin 2). Squared distances are preferred for algebraic cleanliness; the unsquared alphabet carries the same asymptotic information because distances are nonnegative. The spectrum is the set of realized values, not a multiset, so multiplicity is discarded at this layer.
proof idea
Definitional construction, not a proof. Under classical choice, form the Cartesian product of the two finsets and take the image under the map $(p,q)\mapsto \mathrm{dist}(p,q)^2$. The result is a Finset $\mathbb{R}$ of squared cross-distances. No lemmas beyond the Mathlib Finset product/image API are required.
why it matters
This alphabet is the object whose cardinality Erdős #661 bounds. Downstream, the trivial packing bound states that the spectrum has at most one value per source-detector pair: its card is at most $|P|\cdot|Q|$. That lemma unfolds this definition and applies the standard image-card inequality on the product.
In the RS framing the same alphabet is the two-channel coupling spectrum. The module's rigidity program (planar cross-spectrum rigidity, fixed cross-distance in four-space, the positive Erdős #661 stance) treats this set as the observable whose growth cannot fall below the square-grid scale when true two-sector orthogonality is unavailable in a single positive-definite planar carrier. It is scaffolding for that discrete-geometry / RS bridge, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.