orderedShellMultiplicity_le_budget
plain-language theorem explainer
Any single Euclidean distance shell of a finite planar point set holds at most as many ordered off-diagonal pairs as the whole set admits. Anyone bounding shell occupancy for the RS reading of Erdős #132 cites this. The proof is a one-line filter-cardinality inequality after unfolding the two definitions.
Claim. For every finite set $A$ of points in the plane and every real $r$, the ordered multiplicity of the distance shell at radius $r$ is at most the total ordered off-diagonal pair budget of $A$: $\#\{(p,q)\in A\times A: p\neq q,\,\|p-q\|=r\}\le\#\{(p,q)\in A\times A: p\neq q\}$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical pairwise distance value is a shell in the Euclidean distance multiset; RS reads it as a two-body recognition-energy shell whose occupancy is the shell multiplicity. Lean works with ordered pairs for bookkeeping. For any positive distance the ordered multiplicity is exactly twice the unordered one, so classical bounds of the form $\le n$ become $\le 2n$.
Point2 is the planar point type imported from the bipartite distance-spectrum layer. The ordered shell multiplicity at radius $r$ counts ordered off-diagonal pairs in a finite set $A$ whose Euclidean separation equals $r$. The total ordered pair budget is simply the count of all ordered off-diagonal pairs in $A$ (no distance filter). Both quantities are realized as Finset.card of an appropriate filter of the product set.
proof idea
Term-mode, classical. Unfold both orderedShellMultiplicity and totalOrderedPairBudget to expose the underlying filtered finsets, then apply the standard library fact Finset.card_filter_le: the cardinality of any filter of a finset is at most the cardinality of the ambient finset. No geometric content is used; the inequality is pure set counting.
why it matters
This is the elementary occupancy ceiling that every later shell-multiplicity argument in the module rests on: a single recognition-energy shell cannot outrun the global ordered-pair budget. The module frames the whole development as the RS physicalization of Erdős #132 (distance shells as two-body recognition shells). Sibling notions such as sparse shells, diameter shells, and the ordered Erdős-#132 statement all need a uniform upper bound of this shape before they can compare shell occupancy to $2|A|$ or to divergence criteria. No downstream consumers are wired yet (used_by is empty), so the lemma currently anchors the local counting layer rather than a named parent theorem. It does not itself invoke the forcing chain (T5–T8), RCL, or the mass ladder; it is pure discrete geometry supporting that physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.