Point2
plain-language theorem explainer
Re-exports the ambient point type for planar distance geometry: the real Euclidean plane. Every shell-multiplicity and bipartite spectrum construction in this module is typed over it. The body is a one-line alias of the upstream bipartite-spectrum abbreviation, so all distance and lattice statements share a single plane type.
Claim. Write $\mathrm{Point2}$ for the real Euclidean plane $\mathbb{R}^{2}$, realized as the Euclidean space $\mathbb{R}^{\{0,1\}}$.
background
The module DistanceShellMultiplicity records the Recognition Science reading of Erdős problem #132: a classical pairwise distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
The ambient geometry is the real plane. Upstream, the bipartite distance spectrum module defines the same name as EuclideanSpace ℝ (Fin 2), i.e. $\mathbb{R}^{2}$ with the standard Euclidean structure. Cross-distance alphabets, difference sets, and Gaussian-like lattice carriers are all Finsets of these points.
proof idea
Definitional re-export only: the abbreviation is definitionally equal to the upstream plane type from BipartiteDistanceSpectrum. No proof obligations.
why it matters
Gives a single local name for the plane so shell-multiplicity lemmas and the bipartite spectrum API stay aligned. Downstream consumers include cross-distance and squared-distance alphabets, the cross-difference set, the squared-norm alphabet, approximate containment in a Gaussian-like lattice, and the Erdős #661 positivity interface. In the RS framing this is the visible plane in which two-body recognition shells and their occupancies are counted; it is scaffolding for the physicalization of Erdős #132, not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.