IsDiameterShell
plain-language theorem explainer
A real number r is a diameter shell of a finite planar point set A when it appears in the ordered pairwise-distance spectrum and is maximal among those distances. Anyone counting diameter edges, thrackles, or convex-layer screening for the RS form of Erdős #132 cites this predicate. The body is a two-clause Prop abbreviation: membership plus a universal upper bound.
Claim. For a finite set $A$ of points in the plane and a real $r$, $r$ is a diameter shell of $A$ when $r$ belongs to the ordered pairwise Euclidean distance spectrum of $A$ and every distance in that spectrum is at most $r$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum layer. The ordered distance spectrum of a finite set $A$ is the finite set of Euclidean lengths realized by ordered non-diagonal pairs from $A$. A diameter shell is simply the maximum value in that spectrum, packaged as a predicate on $(A,r)$ rather than as an extracted real.
Downstream diameter geometry (crossing bounds, Conway thrackle structure on diameter edges, convex-layer screening) all quantify over pairs $(A,\Delta)$ satisfying this predicate, so the definition is the common gate for every diameter-specific counting argument in the file.
proof idea
Pure definitional abbreviation: no tactics and no lemmas. The Prop is the conjunction of spectrum membership of $r$ with the statement that every spectrum value is $\le r$. Uniqueness and nonnegativity of the diameter value are proved separately (isDiameterShell_unique, diameter_shell_nonneg).
why it matters
This predicate is the diameter hypothesis threaded through the module's main counting and screening results. It appears in DiameterConwayThrackleBound (ordered thrackle bound $\le 2|A|$ on the diameter shell, the Hopf–Pannwitz target), in DiameterEdgeSupportFormsConwayThrackle (correct unordered-support Conway condition), and in the cross-distance convenience lemma diameter_ordered_edges_cross_distances_le.
It also gates the global convex-layer program: ConvexLayerScreeningBridge and ConvexLayerScreeningThresholdCertificate quantify over diameter shells $\Delta$ of large finite sets, screening low-shell residual deep-layer configurations. In the RS reading, the diameter is the outermost two-body recognition-energy shell; controlling its multiplicity is the first step toward the ordered form of Erdős #132 (sparse shells diverge, second-sparse flux bridges). The definition itself closes no open question, but every diameter thrackle or layer-flux certificate is stated relative to it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.