diameter_shell_nonneg
plain-language theorem explainer
If Δ is a diameter shell of a finite planar point set A (the maximum of its ordered pairwise distance spectrum), then Δ ≥ 0. Anyone who bounds pairwise distances by the diameter, or treats shells as two-body recognition energies in the Erdős #132 physicalization, cites this. The proof pulls a realizing ordered pair out of the spectrum image and applies nonnegativity of Euclidean distance.
Claim. Let $A$ be a finite set of points in the plane and $\Delta \in \mathbb{R}$. If $\Delta$ lies in the ordered pairwise distance spectrum of $A$ and is maximal among all values in that spectrum, then $0 \leq \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 positive distances ordered multiplicity is twice the unordered count and classical thresholds scale by two.
Points are planar (Point2). The ordered distance spectrum of a finite set $A$ is the multiset of Euclidean distances over ordered non-diagonal pairs. A real $r$ is a diameter shell of $A$ when it belongs to that spectrum and dominates every other spectrum value: it is the maximum pairwise distance realized in $A$.
The claim is the elementary positivity fact for that maximum: a diameter value is a genuine distance, hence nonnegative.
proof idea
Term-mode under classical logic. The first conjunct of the diameter-shell hypothesis says $\Delta$ is in the ordered distance spectrum, which is an image of pairwise distances. Finset.mem_image.mp yields an ordered pair whose distance equals $\Delta$. Rewrite along that equality and finish with dist_nonneg.
why it matters
Feeds dist_le_of_diameter_shell, which states every pairwise distance in $A$ (including the zero diagonal) is at most the diameter. That bound is the basic comparison step for shell multiplicity arguments in the RS reading of Erdős #132: shells are two-body recognition-energy levels, and the diameter is the top occupied level.
Within the module it sits next to uniqueness of the diameter value and the sparse-shell divergence / flux-bridge material. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is pure metric scaffolding so later recognition-energy comparisons stay well-typed and nonnegative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.