totalOrderedPairBudget_le_all_pairs

The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. For Lean simplicity the development counts ordered pairs. For any positive distance, ordered multiplicity is exactly twice the unordered multiplicity, so classical thresholds of the form $\le n$ become $\le 2n$.

Point2 is the planar point type from the bipartite distance spectrum. Ordered pair events are the non-diagonal elements of the Cartesian product $A\times A$. The total ordered pair budget is the cardinality of that filtered product: every genuine two-body event is one such ordered pair. This lemma only needs that global counting bound, not the metric structure of the shells.

Classical mode is opened for Finset filtering. Unfold the budget and the ordered-event definition to expose $((A\times A).\mathrm{filter},(p,q)\mapsto p\neq q).\mathrm{card}$. A one-line calc applies Finset.card_filter_le (any filter is at most the ambient set) and then simp rewrites the product cardinality as $|A|\cdot|A|$. No metric or shell hypothesis is used.

This is the crude global ceiling that later pair-budget pressure arguments refine. Downstream, pair_budget_pressure_from_counting quotes it as pure finite accounting: in a deep-layer residual case all non-diameter shells are supercritical, so there are at most $|A|/2$ of them and hence at most $|A|/2+1$ occupied shells. That pressure step is part of the RS physicalization of Erdős #132 (distance-shell multiplicity). The bound itself is metric-free; it only licenses comparing a single shell's ordered occupancy against the whole ordered event pool, which the next lemmas in the module exploit.