pair_budget_pressure_from_counting
plain-language theorem explainer
In a deep-layer residual planar point set whose diameter is a distance shell, pure ordered-pair counting forces at most |A|/2 non-diameter shells, hence at most |A|/2+1 occupied shells (stated as ≤|A|/2+2). Cited by anyone closing the shell-flux bridge in the RS reading of Erdős #132. Proof chains supercritical shell-count pressure through the total ordered-pair budget and finishes by elementary arithmetic.
Claim. Let $A$ be a finite planar point set and let $\Delta$ be a diameter shell of $A$ (a value in the ordered distance spectrum that is maximal among all realized distances). Then pair-budget pressure holds: whenever $A$ is in the deep-layer residual case relative to $\Delta$, the number of occupied distance shells satisfies $\mathrm{occupied}(A)\le |A|/2+2$.
background
This module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances the ordered multiplicity is exactly twice the unordered one, so classical thresholds scale by two.
A diameter shell $\Delta$ is a value in the ordered distance spectrum of $A$ that dominates every other realized distance. Pair-budget pressure is the structural claim that, absent a second sparse shell, a deep-layer residual configuration is forced into the low-shell regime: occupied shell count at most $|A|/2+2$.
The local accounting uses the ordered distance spectrum, the total ordered-pair budget (at most $|A|^2$), and the count of non-diameter shells. Upstream pressure lemmas already encode that every non-diameter shell in the deep-layer case is supercritical.
proof idea
Assume the deep-layer residual case. Let $S$ be the ordered distance spectrum with the diameter value $\Delta$ filtered out. Apply the non-diameter shell-count pressure lemma to obtain $|S|\cdot(2|A|+1)\le$ total ordered-pair budget. Bound that budget by $|A|^2$ via the all-pairs comparison, then transitively combine. The shell-pressure arithmetic lemma upgrades the product inequality to $|S|\le|A|/2$. Occupied shell count is at most $|S|+1$ by the non-diameter-plus-one comparison (using that $\Delta$ lies in the spectrum). Close with omega.
why it matters
This is the pure finite-accounting half of the shell-flux plan for the RS reading of Erdős #132. Downstream, second_sparse_shell_flux_bridge_from_minimal_geometry splits on whether a second sparse shell already exists; in the residual deep-layer branch it invokes exactly this pressure to feed the low-shell hypothesis into screening. The reduced-to-full component pack likewise installs pair-budget pressure by filtering this theorem.
In framework terms the result is combinatorial scaffolding rather than a forcing-chain landmark (T5–T8, RCL, $\varphi$): it converts supercritical multiplicity into a hard shell-count ceiling so convex-layer analysis can take over. It closes no open axiom; it discharges the pair-budget obligation inside the minimal-geometry package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.