occupiedShellCount_le_nonDiameter_add_one
plain-language theorem explainer
When a distance value Δ lies in the ordered pairwise distance spectrum of a finite planar set A, the occupied shell count is at most one plus the number of spectrum values other than Δ. Finite-geometry and RS pair-budget arguments cite this as pure shell accounting. The proof is a short Finset identity: erasing Δ and adding one recovers the full spectrum cardinality, then omega closes after unfolding occupancy.
Claim. Let $A$ be a finite set of points in the plane and let $\Delta\in\mathbb{R}$ belong to the ordered pairwise distance spectrum of $A$. Then the number of occupied distance shells of $A$ is at most one plus the number of spectrum distances strictly different from $\Delta$.
background
This module is the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. The development works with ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is twice the unordered multiplicity, so classical thresholds scale by two.
Points are the planar type Point2 imported from the bipartite distance spectrum layer. The ordered distance spectrum of a finite set $A$ is the Finset of realized pairwise distances (ordered non-diagonal pair events). Occupied shell count is the number of distinct such shells that actually appear. The hypothesis only requires that $\Delta$ occurs in that spectrum; uniqueness or diameter character of $\Delta$ is not used here.
proof idea
Tactic proof under classical logic. Unfold the occupied-shell-count definition. Establish the Finset identity that the cardinality of the spectrum with $\Delta$ filtered out, plus one, equals the full spectrum cardinality: rewrite by Finset.filter_ne', then apply Finset.card_erase_add_one at the membership hypothesis. The target inequality then reduces to a numeric comparison that omega discharges.
why it matters
Feeds the downstream theorem on pair-budget pressure from counting, whose doc-comment states that 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. This lemma supplies the elementary “non-diameter count plus one” half of that accounting when a distinguished spectrum value (typically the diameter shell) is present.
In the RS reading, each shell is a two-body recognition-energy level; bounding occupied shells is the combinatorial pressure that forces the low-shell regime in the Erdős #132 physicalization. It is pure finite combinatorics, not a forcing-chain step (T0–T8), but it is the counting hinge the pair-budget component of the final plan rests on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.