crossDistSqSpectrum_card_le_pairs
plain-language theorem explainer
For any two finite planar point sets, the number of distinct squared Euclidean cross-distances is at most the product of the set sizes. Combinatorialists and anyone framing Erdős #661 as a bipartite range alphabet cite this as the trivial ceiling. The argument is a one-step image-cardinality bound after unfolding the spectrum definition.
Claim. For finite $P,Q\subset\mathbb{R}^2$, if $S=\{\|p-q\|^2:p\in P,\,q\in Q\}$ denotes the set of squared Euclidean cross-distances, then $|S|\le |P|\cdot|Q|$.
background
The module treats Erdős problem #661 in physicalized form: two finite planar channels coupled by Euclidean propagation delay, with the classical distance count read as the alphabet size of the cross-coupling spectrum. The positive Erdős direction asks whether that alphabet can be $o(n/\sqrt{\log n})$; the RS reading expects square-grid scale rigidity in a single positive-definite planar carrier.
Points live in the Euclidean plane (Point2 is $\mathbb{R}^2$ with the standard inner-product norm). The squared cross-distance spectrum of finite $P,Q$ is the image of the product $P\times Q$ under $(p,q)\mapsto|p-q|^2$. Squaring is harmless for alphabet cardinality questions and keeps the values algebraic over the coordinate field.
The present claim is only the trivial combinatorial upper bound: at most one spectrum value per ordered source-detector pair.
proof idea
After classical (needed for finset image reasoning), unfold the spectrum to the image of $P\times Q$ under squared distance. Apply Finset.card_image_le: the cardinality of any image is at most the cardinality of the domain. Then simplify the product cardinality to $|P|\cdot|Q|$. No geometry beyond the definition of the map is used.
why it matters
This is the baseline ceiling in the bipartite-distance-spectrum package that records the physicalized Erdős #661 question. Every nontrivial claim in the module (positive little-o constructions, planar cross-spectrum rigidity, fixed-distance constraints in four-space) is measured against this product bound: without it there is no scale against which "small alphabet" or "rigid grid scale" can be stated.
In RS terms the two channels are source and detector sectors linked by Euclidean delay; the spectrum alphabet is the discrete set of coupling lengths. The module doc contrasts the Erdős little-o target with the RS expectation that true two-sector orthogonality is unavailable in one positive-definite planar carrier, so the $n/\sqrt{\log n}$ square-grid scale should be rigid. The present lemma only supplies the universal combinatorial lid, not that rigidity.
No downstream theorems currently depend on it in the graph; it is infrastructure for the sibling spectrum and rigidity statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.