Point2
plain-language theorem explainer
The ambient space for planar two-channel range experiments is ordinary Euclidean 2-space over the reals. Anyone working the physicalized Erdős #661 spectrum (cross-distance alphabets between finite source and detector sets) cites this carrier. It is a one-line type synonym for Mathlib's Euclidean space on Fin 2.
Claim. Write $\mathrm{Point}_2$ for the real Euclidean plane $\mathbb{R}^2$ (equivalently, the Mathlib Euclidean space over $\mathbb{R}$ indexed by a 2-element type).
background
The module physicalizes Erdős problem #661 as a two-channel range-spectrum question: two finite planar sets $P$ and $Q$ (sources and detectors) are coupled by Euclidean propagation delay, and the classical distinct-distance count becomes the alphabet size of the cross-coupling spectrum.
In that setting every point lives in a single positive-definite planar carrier. The abbreviation simply names that carrier as real Euclidean 2-space, so later definitions (cross-distance spectra, cross-difference sets, Gaussian-like lattices) can quantify over finite subsets of the plane without repeating the ambient type.
Upstream, the sibling module DistanceShellMultiplicity re-exports the same planar point type, keeping shell-multiplicity and bipartite-spectrum language aligned.
proof idea
Pure abbreviation: the name is definitionally equal to Mathlib's EuclideanSpace ℝ (Fin 2). No proof obligations.
why it matters
Every object in the bipartite-distance-spectrum development is typed over this plane: squared and unsquared cross-distance alphabets, the cross-difference set $Q-P$, the squared-norm alphabet, approximate containment in a Gaussian-like lattice, and the positive Erdős #661 statement itself. The module doc frames the RS reading: true two-sector orthogonality is unavailable in one positive-definite planar carrier, so the square-grid $n/\sqrt{\log n}$ scale should be rigid rather than $o(n/\sqrt{\log n})$. Naming the carrier once keeps that rigidity target geometrically fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.