crossDifferenceSet
plain-language theorem explainer
The cross-difference set of two finite planar point sets P and Q is the finite set of all vectors q − p. Workers on the bipartite distance spectrum (Erdős #661 in RS form) cite it as the raw vector alphabet before squared norms. The body is a one-line image of the Cartesian product under subtraction.
Claim. For finite $P, Q \subset \mathbb{R}^2$, define the cross-difference set $Q - P := \{ q - p : p \in P,\ q \in Q \} \subset \mathbb{R}^2$ as a finite set of planar vectors.
background
The module treats the physicalized form of Erdős problem #661: two finite planar channels $P$ and $Q$ coupled by Euclidean propagation delay, with the classical distance count read as 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 expects square-grid rigidity instead, since true two-sector orthogonality is unavailable in a single positive-definite planar carrier.
Points live in Point2, the Euclidean plane $\mathbb{R}^2$. The cross-difference set is the intermediate object that turns the bipartite pair $(P,Q)$ into a single finite set of displacement vectors before any norm or spectrum is taken. Upstream norm machinery (GoldenInt field norm, action $L^2$ norms) is ambient infrastructure and is not used in the definition itself.
proof idea
Definitional, not a proof. Under classical choice, form the Cartesian product $P \times Q$ and push it forward by the map $(p,q) \mapsto q - p$. The result is the finite image set of all cross-differences. No lemmas are applied beyond Finset product and image.
why it matters
This is the raw carrier for the bipartite spectrum pipeline. Downstream, the squared-norm alphabet is exactly the image of this set under squared Euclidean norm: every subsequent cardinality or rigidity statement about cross-distances factors through these vectors. It sits at the start of the RS reading of Erdős #661, where the question is whether the cross-coupling alphabet can beat the square-grid $n/\sqrt{\log n}$ scale. Without a clean $Q-P$ object, the later inverse-theorem and rigidity targets (planar cross-spectrum rigidity, fixed cross-distance in four-space) have nothing to act on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.