totalOrderedPairBudget
plain-language theorem explainer
For a finite planar point set, the total ordered pair budget is the number of ordered pairs of distinct points. It is the global two-body ledger capacity against which every distance-shell occupancy is measured. Anyone proving shell-count or multiplicity bounds in the RS reading of Erdős #132 cites it. The body is a one-line card of the filtered product of the set with itself.
Claim. For a finite set $A$ of points in the Euclidean plane, the total ordered pair budget of $A$ is the cardinality of the set of ordered pairs $(p,q)$ with $p,q\in A$ and $p\neq q$.
background
The module physicalizes Erdős problem #132: a classical distance value becomes a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used 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 live in the Euclidean plane (Point2). The ordered non-diagonal pair events of a finite set $A$ are the product $A\times A$ with the diagonal removed. The budget defined here is simply the cardinality of that event set: the total number of ordered two-body interactions available to be partitioned among distance shells.
Upstream, the event set is the filtered product construction; the budget is the global capacity that every shell-multiplicity comparison and every partition identity refers to.
proof idea
Pure definition: unfold to the cardinality of the ordered non-diagonal pair-event finset. No lemmas, no tactics beyond the classical filter on the product.
why it matters
This is the global capacity constant in the finite-counting half of the Erdős #132 physicalization. Downstream it is the right-hand side of the shell partition identity (sum of ordered shell multiplicities equals the budget), the trivial upper bound on any single shell's multiplicity, and the resource that non-diameter shells consume at rate at least $2|A|+1$ in deep-layer cases. Those counting inequalities feed the pair-budget pressure structure used to bound the number of occupied shells by $|A|/2+1$. In RS language it is the total two-body ledger capacity against which recognition-energy shells compete; it does not itself invoke $\varphi$, the eight-tick octave, or the forcing chain, but it is the combinatorial substrate those later bridges sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.