dist_le_of_diameter_shell
plain-language theorem explainer
Every pairwise Euclidean distance in a finite planar point set is at most the diameter-shell value, including the zero self-distance. Anyone bounding cross-distances among diameter edges in the ordered-pair form of Erdős #132 cites this. The proof splits on whether the two points coincide, then either uses nonnegativity of the diameter or spectrum membership.
Claim. Let $A$ be a finite set of points in $\mathbb{R}^2$, and let $\Delta\in\mathbb{R}$ be a diameter shell of $A$: $\Delta$ lies in the ordered pairwise distance spectrum of $A$ and is maximal among those distances. Then for all $x,y\in A$, $\mathrm{dist}(x,y)\le\Delta$.
background
This module physicalizes Erdős problem #132: a classical distance value is a shell in the set of pairwise Euclidean distances; in RS it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so for a positive distance the ordered multiplicity is twice the unordered one (classical threshold $\le n$ becomes $\le 2n$).
Points live in $\mathbb{R}^2$ via the bipartite distance-spectrum abbreviation. The ordered distance spectrum is the image of ordered non-diagonal pair events under Euclidean distance. A diameter shell is a spectrum value that dominates every other spectrum value: it is the maximum realized pairwise distance in the ordered normalization.
The companion nonnegativity fact records that any such diameter value is $\ge 0$, since it is a distance between two points of $A$.
proof idea
Classical case split on whether the two points coincide.
If they are equal, rewrite the distance as $0$ and apply diameter-shell nonnegativity to get $0\le\Delta$.
If they differ, exhibit the distance as a member of the ordered spectrum: the ordered pair sits in the filtered product of $A\times A$ (non-diagonal), and the spectrum is the image of that set under distance. The second conjunct of the diameter-shell hypothesis then yields $\mathrm{dist}\le\Delta$.
why it matters
Local lemma that turns the abstract maximum-distance predicate into a usable pairwise bound. Its sole downstream consumer is the convenience bundle that all four cross-distances between two ordered diameter edges are $\le\Delta$ (and both edge lengths equal $\Delta$). That bundle is the geometric engine for the ordered-pair form of Erdős #132: sufficiently large finite planar sets carry two distinct sparse distance shells.
In the RS reading, diameter control is the first step toward treating shells as recognition-energy levels with occupancy bounds. The result itself is pure planar geometry; the framework link is the module's physicalization of shell multiplicity, not a forcing-chain step (T0–T8) or the RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.