sum_orderedShellMultiplicity_eq_budget
plain-language theorem explainer
Ordered distance shells partition the ordered pair-event budget: summing shell multiplicities over the spectrum recovers the total number of ordered off-diagonal pairs. Anyone proving shell-count pressure bounds in the Erdős #132 physicalization cites this identity. The proof is a one-shot fiberwise card decomposition of the ordered pair set under the distance map.
Claim. For every finite planar point set $A\subset\mathbb{R}^2$, $$\sum_{r\in S(A)} m_{\mathrm{ord}}(A,r)=B_{\mathrm{ord}}(A),$$ where $S(A)$ is the ordered distance spectrum, $m_{\mathrm{ord}}(A,r)$ is the ordered multiplicity of distance $r$, and $B_{\mathrm{ord}}(A)$ is the total ordered pair-event budget (cardinality of ordered off-diagonal pairs in $A$).
background
This module physicalizes Erdős problem #132 inside Recognition Science: a classical pairwise distance value becomes a two-body recognition-energy shell, and its multiplicity is shell occupancy. The development works with ordered pairs for Lean simplicity; for any positive distance the ordered multiplicity is exactly twice the unordered one, so classical thresholds $\le n$ become $\le 2n$.
Points are Point2, i.e. the Euclidean plane $\mathbb{R}^2$. The ordered pair-event set is the finite collection of ordered off-diagonal pairs from $A$. The ordered distance spectrum is the image of that set under $(p,q)\mapsto|p-q|$. Ordered shell multiplicity at radius $r$ counts how many ordered pairs realize distance $r$. The total ordered pair-event budget is the cardinality of the ordered pair-event set.
Upstream, the spectrum is defined as that image finset; the present theorem is the elementary partition identity that makes later occupancy bookkeeping legitimate.
proof idea
Work classically. Let $f$ send an ordered pair to its Euclidean distance. The image of the ordered pair-event finset under $f$ is exactly the ordered distance spectrum, so $f$ maps the pair set into the spectrum. Apply Finset.card_eq_sum_card_fiberwise to that map: the cardinality of the pair set equals the sum, over spectrum radii, of the sizes of the fibers. Unfolding the definitions of ordered shell multiplicity and total ordered pair budget, and symmetrizing the equality, yields the claim. No geometric input beyond the definitions is used.
why it matters
This is the budget-conservation identity for the RS reading of Erdős #132: shells partition recognition events rather than merely labeling distances. Downstream, non_diameter_shell_count_pressure multiplies the number of non-diameter occupied shells by the deep-layer lower bound $2|A|+1$ and compares to the total budget; that comparison is only meaningful once the sum of multiplicities is known to equal the budget. The identity therefore underwrites the finite-counting pressure behind the low-shell regime in the module's proof plan, including uniqueness and nonnegativity facts about the diameter shell and the second-sparse-shell flux bridge. It is pure discrete geometry, not a forcing-chain step (T0–T8), but it is the counting backbone of the distance-shell physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.