shell_pressure_arithmetic

The module physicalizes Erdős problem #132: classical distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds of the form ≤ n become ≤ 2n.

Pair-budget pressure is the finite-accounting half of that story. With |A|=n points one has at most n² ordered pairs. If every non-diameter shell is forced to carry at least 2n+1 ordered events (the supercritical floor), the number of such shells cannot exceed n/2. This lemma isolates that counting inequality from geometry.

Upstream name collisions (shell scales, event counts) are not used here; the statement is pure natural-number arithmetic.

Split on n = 0: the hypothesis collapses to k·1 ≤ 0, so k = 0 = n/2.

For n > 0, assume toward contradiction that k ≰ n/2, hence k ≥ n/2 + 1. Integer division gives n < 2(n/2 + 1). Multiply by n > 0 to get n² < 2(n/2 + 1)·n. Rearrange by nlinarith to 2(n/2 + 1)·n ≤ (n/2 + 1)(2n + 1), so n² < (n/2 + 1)(2n + 1). Multiply the lower bound on k by (2n+1) and chain inequalities to n² < k(2n+1), contradicting the hypothesis.

This is the arithmetic engine under pair_budget_pressure_from_counting, which states that in a deep-layer residual case all non-diameter shells are supercritical, so there are at most |A|/2 of them and thus at most |A|/2 + 1 occupied shells total.

In the RS reading of Erdős #132, that bound is the pair-budget half of shell-pressure control: recognition energy cannot support too many distinct two-body distance shells once each shell is forced above the 2n+1 ordered-event floor. The lemma closes the pure counting step so the geometric diameter-shell hypotheses can be discharged separately.

It does not itself invoke the forcing chain (T0–T8), RCL, or φ-ladder mass formulas; it is infrastructure mathematics that those physical claims rely on when they talk about shell occupancy budgets.