PlanarCrossSpectrumRigidity
plain-language theorem explainer
Names the planar bipartite rigidity claim for Erdős #661: two equal-size finite planar point sets eventually realize at least order n/√(log n) distinct cross-distances. Combinatorial geometers and RS workers treating the two-channel range spectrum would cite it as the negative (grid-scale) target. It is a bare Prop definition encoding that asymptotic lower bound, not a proved theorem.
Claim. There exists a constant $c>0$ such that for all sufficiently large $n$, every pair of finite planar point sets $P,Q\subset\mathbb{R}^2$ with $|P|=|Q|=n$ realizes at least $c\, n/\sqrt{\log n}$ distinct Euclidean cross-distances.
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question. Two finite planar channels $P$ and $Q$ couple by Euclidean propagation delay; the classical distinct-distance count is the alphabet size of the cross-coupling spectrum (the set of realized pairwise distances between the two sides).
The classical positive direction asks whether that alphabet can be $o(n/\sqrt{\log n})$. The RS reading runs the other way: in a single positive-definite planar carrier, true two-sector orthogonality is unavailable, so the square-grid scale $n/\sqrt{\log n}$ should be rigid as a lower bound. The companion four-space statement records a Lenz-style collapse in which all cross-distances can coincide; that orthogonal two-sector mechanism is not available in one planar carrier.
Point2 is the planar point type; the cross-distance spectrum of two finite sets is the finite set of realized inter-set Euclidean distances. The definition packages the eventual uniform lower bound on the cardinality of that spectrum.
proof idea
No proof: the declaration is a Prop-valued definition. Its body is the claim itself, written as existence of a positive real $c$ and an eventual quantifier over $n\to\infty$ (filter atTop), then universal quantification over equal-cardinality finite planar point sets, asserting the stated multiple of $n/\sqrt{\log n}$ lower-bounds the cardinality of the cross-distance spectrum. Nothing is discharged; the term is the statement to be proved or refuted later.
why it matters
In the Recognition framework this is the explicit negative target for the physicalized Erdős #661: planar two-channel coupling should not thin below the grid scale. The module doc contrasts it with the four-dimensional Lenz collapse, where an orthogonal two-sector mechanism can force all cross-distances equal; that mechanism is unavailable in one planar carrier, which is why RS expects rigidity rather than the classical $o(\cdot)$ thinning.
No downstream theorems currently consume the definition (used_by is empty). It sits as a named interface between combinatorial distance geometry and the RS two-channel reading of range spectra. Closing it (or a quantitative variant) would pin the planar side of the bipartite spectrum story; the four-space fixed-cross-distance companion marks the contrasting richer-carrier regime. It does not itself touch the T0–T8 forcing chain, RCL, or the constants ladder; its role is local to the bipartite spectrum module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.