FixedCrossDistanceInFourSpace
plain-language theorem explainer
Names the property that two finite point sets in Euclidean 4-space have a single common cross-distance: every pair from opposite channels is exactly distance r. Discrete geometers and anyone tracking the RS reading of Erdős #661 would cite it as the Lenz-style collapse available once the carrier is four-dimensional. The body is a one-line existential Prop, not a proved theorem.
Claim. For finite $P,Q\subset\mathbb{R}^4$, the predicate holds iff there exists $r\in\mathbb{R}$ such that $d(p,q)=r$ for every $p\in P$ and $q\in Q$.
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question: finite planar channels $P$ and $Q$ coupled by Euclidean delay, with the classical distinct-distance count 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 targets the opposite rigidity in a single positive-definite planar carrier.
Point4 is the Euclidean space $\mathbb{R}^4$. The present definition lifts the bipartite fixed-distance idea into that richer carrier. The doc-comment frames it as Lenz-style collapse: all cross-distances between the two finite channels coincide. In the plane that orthogonal two-sector mechanism is unavailable, which is why #661 is hard there.
Sibling material in the module tracks squared and unsquared cross-distance alphabets, cardinality bounds relative to pair counts, and a planar rigidity target. This Prop is the four-space contrast case, not a planar statement.
proof idea
Definitional, not a proof. The body is the Prop $\exists r:\mathbb{R},;\forall p\in P,;\forall q\in Q,;\mathrm{dist},p,q=r$, using the Mathlib Euclidean distance on EuclideanSpace ℝ (Fin 4). No lemmas are applied; no tactics run.
why it matters
It records the geometric mechanism the module contrasts with planar #661 rigidity: in $\mathbb{R}^4$ one can arrange two finite channels with a single common cross-distance (Lenz-type configuration), whereas the module doc argues that true two-sector orthogonality is unavailable in one positive-definite planar carrier, so the square-grid $n/\sqrt{\log n}$ scale should be rigid. No downstream theorems currently consume it (used_by is empty); it sits as a named target and contrast predicate beside PlanarCrossSpectrumRigidity and Erdos661Positive. It does not itself invoke the forcing chain (T0–T8), RCL, or phi-ladder mass formulae; its role is combinatorial geometry inside the RS reading of the bipartite spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.