DiameterShellExistsEventually
plain-language theorem explainer
For all sufficiently large finite planar point sets, the ordered pairwise-distance spectrum is nonempty and therefore has a maximum (a diameter shell). Discrete geometers and RS workers building the Hopf–Pannwitz bridge cite this as the pure bookkeeping half of that split. The declaration is a named proposition packaging the filter-eventually statement; existence itself is proved downstream by a short cardinality argument.
Claim. Eventually in cardinality $n\to\infty$, every finite set $A\subset\mathbb{R}^2$ with $|A|=n$ admits a real $\Delta$ that lies in the ordered pairwise-distance spectrum of $A$ and is maximal among all distances in that spectrum (a diameter shell).
background
The 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 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 double.
Points live in the Euclidean plane (Point2). A diameter shell for a finite set $A$ is a real $r$ that belongs to the ordered distance spectrum of $A$ and dominates every other spectrum value. The present declaration only asserts eventual existence of such an $r$; sparsity of diameter shells is a separate geometric claim.
proof idea
Definitional packaging, not a proof. The body is the Mathlib filter statement that, eventually as $n\to\infty$ along atTop, every finite planar set of cardinality $n$ has some real $\Delta$ satisfying the maximum-distance predicate. No lemmas are applied here; the actual existence argument appears in the downstream theorem that unfolds this name and supplies a concrete threshold $n\ge 2$.
why it matters
This is the maximum-existence half of the Hopf–Pannwitz component pack, which splits the classical straight-line thrackle bridge into (i) diameter-shell existence and (ii) diameter-shell sparsity. Downstream, diameter_shell_exists_eventually_holds discharges the proposition by finite bookkeeping (nonempty finite ordered spectrum has a max), and HopfPannwitzComponentPack records both components together. The doc-comment stresses the separation: genuine geometry sits in the sparsity bound, not in maximum existence. In the RS reading of Erdős #132, diameter shells are the coarsest two-body recognition-energy shells; naming their eventual existence keeps the combinatorial ledger clean before geometric constraints enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.