DiameterShellOrderedMultiplicityBound
plain-language theorem explainer
Named proposition packaging the ordered diameter-shell occupancy bound: for all large enough planar n-point sets, any diameter distance is realized by at most 2n directed pairs. It is the quantitative core of the module's Erdős #132 physicalization after switching to ordered pairs. Downstream sparse-shell bridges and thrackle-based diameter theorems cite it as the occupancy hypothesis. The body is a pure Prop definition, not a proved statement.
Claim. Eventually as $n\to\infty$, for every finite $A\subset\mathbb{R}^2$ with $|A|=n$ and every $\Delta\in\mathbb{R}$ that is a diameter shell of $A$ (membership in the ordered pairwise-distance spectrum, and maximality among spectrum values), the ordered shell multiplicity of $\Delta$ satisfies $\mathrm{mult}^{\mathrm{ord}}(A,\Delta)\le 2|A|$.
background
The module records the Recognition Science reading of Erdős problem #132. Classically a 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. The development works with ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is exactly twice the usual unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
Points live in the Euclidean plane (Point2). The ordered distance spectrum of a finite set $A$ is the multiset of distances between ordered pairs of distinct points. A real $\Delta$ is a diameter shell of $A$ when it belongs to that spectrum and is maximal among spectrum values. Ordered shell multiplicity counts directed pairs realizing a fixed distance.
The present declaration does not assert a theorem; it names the asymptotic bound proposition that later results either assume or discharge.
proof idea
Definitional packaging only: the right-hand side is the filter statement "eventually in $n$ at infinity, every $n$-point planar finset whose $\Delta$ is a diameter shell has ordered multiplicity at most $2n$." No tactics, no lemmas, no reduction. Downstream proofs either inhabit this Prop (from thrackle and no-disjoint-diameter-edge hypotheses) or consume it as a hypothesis to build the sparse-shell bridge.
why it matters
This Prop is the stripped quantitative content of diameter sparsity in the ordered-pair convention. It is discharged by diameter_ordered_bound_from_thrackle_components, whose doc-comment states that Hopf–Pannwitz ordered multiplicity follows from no-disjoint-diameter-edges plus the ordered thrackle bound. It is consumed by diameter_shell_sparse_from_ordered_bound, which lifts the ordered multiplicity bound to the sparse-shell bridge used elsewhere in the module.
In the RS framing, diameter shells are the highest two-body recognition-energy shells of a planar configuration; bounding their occupancy is the first step toward the sparse-shell divergence and flux-bridge results that sit later in the same file. The declaration therefore sits between classical discrete-geometry input (thrackle / Hopf–Pannwitz) and the module's physicalized Erdős #132 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.