non_diameter_shell_count_pressure
plain-language theorem explainer
In a deep-layer residual configuration, every occupied non-diameter distance shell carries at least 2|A|+1 ordered pair events. Multiplying that lower bound by the number of such shells therefore cannot exceed the total ordered-pair budget. Anyone closing the finite-counting half of the Erdős #132 physicalization cites this inequality. The proof is a short filter-and-sum comparison using supercriticality on each non-diameter shell.
Claim. Let $A$ be a finite planar point set and $\Delta\in\mathbb{R}$. If $(A,\Delta)$ is a deep-layer case (every occupied non-diameter shell fails to be sparse), then $$\bigl|\{r\in\mathrm{Spec}^{\mathrm{ord}}(A): r\neq\Delta\}\bigr|\cdot(2|A|+1)\le B^{\mathrm{ord}}(A),$$ where $\mathrm{Spec}^{\mathrm{ord}}(A)$ is the ordered distance spectrum and $B^{\mathrm{ord}}(A)$ is the total ordered-pair event budget of $A$.
background
This module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so the classical threshold $\le n$ becomes $\le 2n$.
A point is an element of the Euclidean plane $\mathbb{R}^2$. The ordered distance spectrum of a finite set $A$ is the finite set of realized positive pairwise distances counted with ordered (off-diagonal) pairs. The ordered shell multiplicity at radius $r$ is the number of ordered pairs at that distance; summing multiplicities over the spectrum recovers the total ordered-pair budget.
A deep-layer case is a residual configuration in which no occupied non-diameter shell has yet been shown sparse. The companion fact DeepLayerCase.supercritical upgrades that: every occupied non-diameter shell then has multiplicity strictly larger than $2|A|$, hence at least $2|A|+1$. The diameter shell $\Delta$ is the unique maximal-distance shell and is excluded from the pressure count here.
proof idea
Work classically. Let $S$ be the ordered spectrum filtered to radii $r\neq\Delta$. For each $r\in S$, membership in the spectrum plus $r\neq\Delta$ and the deep-layer hypothesis give supercriticality, so Nat.succ_le_of_lt yields $2|A|+1\le$ ordered multiplicity at $r$.
A four-step calc finishes: $|S|\cdot(2|A|+1)$ equals the constant sum of $2|A|+1$ over $S$; that sum is $\le$ the sum of ordered multiplicities over $S$ by the pointwise bound; the $S$-sum is $\le$ the full-spectrum sum by subset monotonicity of nonnegative summands; the full sum equals the total ordered-pair budget by the identity sum_orderedShellMultiplicity_eq_budget.
why it matters
This is the checked finite-counting pressure behind the low-shell regime in the Erdős #132 plan. Downstream, pair_budget_pressure_from_counting quotes it to obtain the pair-budget component of the final plan: 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 total.
In Recognition Science language the shells are two-body recognition-energy levels; the budget is a hard combinatorial resource on ordered pair events. The inequality forces any surviving deep-layer configuration into a sparse shell count, which later geometry bridges are meant to rule out. It does not itself invoke the forcing chain (T0–T8) or the J-cost, but it supplies the arithmetic bottleneck those geometric steps need once the configuration has been reduced to a deep-layer residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.