orderedShellMultiplicity
plain-language theorem explainer
Ordered multiplicity of a Euclidean distance value r on a finite planar point set A counts ordered pairs of distinct points at distance exactly r. Discrete geometers and RS workers cite it when restating Erdős #132 shell occupancy in ordered-pair language. The body is a one-line filter-and-card on the ordered non-diagonal pair event set.
Claim. For a finite set $A\subset\mathbb{R}^2$ and $r\in\mathbb{R}$, the ordered shell multiplicity of $r$ on $A$ is $\#\{(p,q)\in A\times A: p\neq q,\,\|p-q\|=r\}$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical pairwise distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Lean works with ordered pairs for bookkeeping; for any positive distance the ordered count is exactly twice the usual unordered multiplicity, so classical thresholds $\le n$ become $\le 2n$.
Points live in the Euclidean plane (Point2 is $\mathbb{R}^2$). The ambient event set is the finite collection of ordered non-diagonal pairs drawn from $A$. Filtering that set by the predicate $\mathrm{dist}(p,q)=r$ isolates one distance shell; its cardinality is the ordered occupancy of that shell.
Upstream geometry is ordinary Euclidean distance on the plane. No continuum or ledger structure is required at this definition; those enter only when shell counts are later compared to recognition budgets.
proof idea
Definitional, not a proof. Under classical choice, take the finite set of ordered non-diagonal pair events on $A$, retain those pairs whose Euclidean distance equals the given $r$, and return the cardinality of the filtered finset. No lemmas are applied beyond Finset.filter and Finset.card.
why it matters
This is the basic occupancy counter for the whole Distance Shell Multiplicity development. Downstream, diameter sparsity is stated as ordered multiplicity at most $2|A|$ (DiameterShellOrderedMultiplicityBound, DiameterConwayThrackleBound); equality with the ordered diameter edge set is definitional; single-shell counts are bounded by the total ordered-pair budget; positivity and supercriticality lemmas feed the deep-layer case analysis and the non-diameter shell-count pressure inequality used in the low-shell regime of the Erdős #132 plan.
In RS language the same integer is the occupancy of a two-body recognition-energy shell. The ordered normalization keeps the classical thrackle and Hopf–Pannwitz counting steps aligned with Lean finset arithmetic while preserving the factor-of-two translation to unordered multiplicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.