TwoChannelRangeExperiment
plain-language theorem explainer
Packages a bipartite planar range setup: two finite point sets in the Euclidean plane, called sources and detectors. Anyone working the RS reading of Erdős #661 (cross-coupling alphabet size) cites this carrier. It is a bare structure definition; the physical readout is the separate cross-coupling spectrum map.
Claim. A two-channel range experiment is a pair of finite sets $S, D \subset \mathbb{R}^2$ (sources and detectors) in the Euclidean plane. Its physical readout is the cross-coupling spectrum: the finite set of Euclidean distances $\{\|s-d\| : s\in S,\, d\in D\}$.
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; the classical distinct-distance count becomes the alphabet size of the cross-coupling spectrum.
Point2 is the Euclidean plane $\mathbb{R}^2$ (as EuclideanSpace ℝ (Fin 2)). Sources and detectors are finite subsets of that plane. The companion map sends an experiment to crossDistSpectrum of its two point sets, i.e. the unordered set of realized source–detector distances.
The RS reading contrasts with the positive Erdős direction: in a single positive-definite planar carrier, true two-sector orthogonality is unavailable, so the square-grid $n/\sqrt{\log n}$ scale is expected to be rigid rather than improvable to $o(n/\sqrt{\log n})$.
proof idea
No proof: this is a structure declaration with two fields (sources and detectors as finite planar point sets). The associated spectrum definition is a one-line wrapper applying the in-module cross-distance spectrum to those two fields.
why it matters
Gives the typed carrier for the bipartite distance spectrum program in this module: the physicalized form of Erdős #661. Downstream siblings (cross-spectrum cardinality bounds, planar cross-spectrum rigidity, fixed cross-distance in four-space, the positive Erdős #661 statement) all speak about experiments of this shape.
In RS terms the object is a two-channel coupling on the visible plane; the alphabet of Euclidean delays is the recognition content of the experiment. The module’s target is rigidity of the square-grid scale, not the classical $o(n/\sqrt{\log n})$ improvement. No forcing-chain landmark (T5–T8) is discharged here; the declaration only sets the geometric stage.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.