diameter_shell_exists_eventually_holds
plain-language theorem explainer
For every finite planar point set of cardinality at least 2, the ordered pairwise distance spectrum is nonempty and therefore attains a maximum, which is a diameter shell. Anyone assembling the ordered Hopf–Pannwitz diameter bound from its existence and sparsity halves will cite this. The argument is pure finitary bookkeeping: two distinct points give a pair event, hence a nonempty spectrum, hence a max.
Claim. There exists $N\in\mathbb{N}$ such that for every finite set $A\subset\mathbb{R}^2$ with $|A|\ge N$, there is a real $\Delta$ that is a diameter shell of $A$: $\Delta$ belongs to the ordered distance spectrum of $A$ and is at least every other value in that spectrum.
background
This module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell, and its 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$).
The ordered pair events of a finite planar set $A$ are the off-diagonal product pairs. The ordered distance spectrum is the image of those pairs under Euclidean distance. A diameter shell is a value in that spectrum that is maximal among all realized distances.
The proposition being proved asserts that diameter-shell existence holds eventually in cardinality: for all large enough $n$, every $n$-point planar set admits some diameter shell. The module doc separates this bookkeeping claim from the genuine geometric content of Hopf–Pannwitz (the sparsity bound on diameter shells).
proof idea
Unfold the eventually-at-top statement and rewrite it as an explicit threshold. Take threshold $N=2$. For any finite planar set $A$ with $|A|=n\ge 2$, cardinality forces two distinct points $a,b\in A$. Their ordered pair lies in the ordered pair-event set, so the ordered distance spectrum is nonempty (it contains $\mathrm{dist}(a,b)$). Let $\Delta$ be the maximum of that finite nonempty spectrum. Membership of the max and the universal upper bound $\mathrm{le_max}'$ show $\Delta$ is a diameter shell.
why it matters
The result discharges the existence half of the ordered Hopf–Pannwitz package. Downstream, hopf_pannwitz_ordered_from_diameter_sparsity quotes the doc line: since diameter-shell existence is now proved, Hopf–Pannwitz reduces to the diameter-sparsity theorem, and packages this theorem with a sparsity hypothesis into the full ordered diameter bound.
In the RS reading of Erdős #132, diameter shells are the extremal two-body recognition-energy shells. Isolating pure maximum-existence from sparsity keeps the geometric thrackle content cleanly on the sparsity side. No forcing-chain landmark (T5–T8) is invoked; the lemma is combinatorial infrastructure for the distance-shell multiplicity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.