occupiedShellCount
plain-language theorem explainer
Counts how many distinct pairwise distances a finite planar point set realizes, i.e. how many ordered distance shells are occupied. Anyone working the RS physicalization of Erdős #132 cites it when bounding shell budgets or entering the low-shell regime. The definition is the cardinality of the ordered distance spectrum.
Claim. For a finite set $A$ of points in the Euclidean plane, the occupied shell count is the number of distinct values of $\mathrm{dist}(p,q)$ among ordered pairs $(p,q)$ drawn from $A$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances, ordered multiplicity is twice the unordered one, so classical thresholds $\le n$ become $\le 2n$.
Points live in $\mathbb{R}^2$ (via the bipartite distance spectrum abbreviation). The ordered distance spectrum of a finite set $A$ is the image of its ordered non-diagonal pair events under the Euclidean distance map. Occupied shell count is simply how many distinct reals appear in that image.
proof idea
Pure definitional wrapper: return the cardinality of the ordered distance spectrum of $A$. No lemmas or tactics beyond evaluating that finset card.
why it matters
Gives the integer shell budget used throughout the module's counting plan. Downstream, LowShellStructure is the regime where occupied shells are at most $|A|/2+2$, forcing convex-layer analysis. PairBudgetPressure and pair_budget_pressure_from_counting use the same count: in a deep-layer residual with diameter shell fixed, all non-diameter shells are supercritical, so at most $|A|/2$ of them exist and occupied shells are at most $|A|/2+1$ (or $+2$ in the structure bound). The companion inequality occupiedShellCount_le_nonDiameter_add_one splits off the diameter shell. This is pure finite accounting inside the RS reading of Erdős #132, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.