PairBudgetPressure
plain-language theorem explainer
Pair-budget pressure packages the finite-accounting claim that a deep-layer residual planar set (no second sparse shell yet found) has at most |A|/2 + 2 occupied distance shells. Shell-flux bridge packs and the Erdős #132 physicalization cite it as a named hypothesis. It is a one-field Prop structure; the inequality is proved later by pure counting of supercritical shells.
Claim. For a finite planar point set $A$ and a real $\Delta$, pair-budget pressure holds when: whenever $A$ is in the deep-layer residual case relative to $\Delta$ (every occupied non-diameter shell is supercritical), the number of occupied ordered distance shells satisfies $\mathrm{occ}(A)\le |A|/2+2$.
background
This module physicalizes Erdős problem #132 inside Recognition Science: a classical pairwise Euclidean distance becomes a two-body recognition-energy shell, and shell multiplicity is occupancy. The development works with ordered non-diagonal pairs on Point2 (planar points), so classical unordered bounds scale by two (threshold $\le n$ becomes $\le 2n$).
A diameter shell is a distinguished maximal distance $\Delta$. A shell is sparse when its ordered multiplicity stays below the supercritical threshold. The deep-layer residual case is the surviving configuration in which no occupied non-diameter shell has yet been shown sparse: every such shell is supercritical. That case is exactly what later geometry must rule out or force into a low-shell regime.
Pair-budget pressure is the named interface for that low-shell consequence: deep layer implies few occupied shells.
proof idea
No proof body: this is a Prop-valued structure with a single field. The field is an implication from the deep-layer residual hypothesis to the numerical bound $\mathrm{occupiedShellCount}(A)\le |A|/2+2$. Downstream, pair_budget_pressure_from_counting fills the field by finite accounting: under a diameter shell, deep layer makes every non-diameter shell supercritical, so there are at most $|A|/2$ of them, hence only a handful of occupied shells in total.
why it matters
In the shell-flux plan for the RS reading of Erdős #132, this is the pure pair-budget component. ShellFluxComponentPack and ShellFluxReducedComponentPack list it as a standalone classical bridge target. The theorems second_sparse_shell_flux_bridge_from_components and second_sparse_shell_flux_bridge_from_minimal_geometry consume it: when the configuration has not already exited via a second sparse shell, pair-budget pressure supplies the low-shell hypothesis that screening needs.
Physically, supercritical shells are expensive two-body recognition channels; bounding their count is finite ledger work before geometry closes the residual deep layer. It does not itself invoke the forcing chain (T5–T8) or the RCL; it is combinatorial pressure feeding the multiplicity bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.