isDiameterShell_unique

The module physicalizes Erdős problem #132: a classical distance value becomes a two-body recognition-energy shell, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.

Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. The ordered distance spectrum of a finite set $A$ is the multiset of Euclidean distances over ordered pairs from $A$. A real $r$ is a diameter shell of $A$ when $r$ belongs to that spectrum and every spectrum value is $\le r$: i.e., $r$ is a maximum pairwise distance.

Uniqueness of that maximum is elementary order theory, but it must be recorded before later lemmas can speak of "the" diameter of $A$.

One-line term proof by antisymmetry of $\le$ on $\mathbb{R}$. Write $h_1,h_2$ for the two diameter-shell hypotheses. The second conjunct of $h_2$ applied to the spectrum-membership of $\Delta_1$ yields $\Delta_1 \le \Delta_2$. Symmetrically, the second conjunct of $h_1$ applied to membership of $\Delta_2$ yields $\Delta_2 \le \Delta_1$. Antisymmetry of the real order then forces $\Delta_1 = \Delta_2$.

This is bookkeeping uniqueness inside the RS physicalization of Erdős #132 (distance shells as two-body recognition-energy shells). No downstream consumers are wired yet (used_by is empty), but sibling lemmas such as nonnegativity of the diameter and the bound that every pairwise distance is at most the diameter presuppose a unique diameter value. The result lets later multiplicity and sparseness statements (sparse shells, flux bridges) refer to a single diameter shell without case-splitting on which maximum was chosen. It does not itself touch the forcing chain T0–T8 or the Recognition Composition Law; it is pure planar-distance infrastructure for the Erdős physicalization.