SparseShellsDiverge
plain-language theorem explainer
Names the proposition that sparse distance shells diverge with set size: the worst-case count of shells with ordered multiplicity at most twice the cardinality tends to infinity as n does. Anyone pursuing the RS shell-flux reading of Erdős #132 would cite this as the stronger target. It is a bare Prop definition via Tendsto of an sInf, not a proved theorem.
Claim. The number of sparse ordered distance shells diverges: as $n\to\infty$, $$\inf_{|A|=n}\#\{r:\,m_{\mathrm{ord}}(A,r)\le 2|A|\}\to+\infty,$$ where the infimum runs over finite point sets $A\subset\mathbb{R}^2$, the spectrum is the ordered pairwise Euclidean distance multiset, and $m_{\mathrm{ord}}$ is ordered shell multiplicity.
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 whose multiplicity is shell occupancy. Lean works with ordered pairs, so for positive distances ordered multiplicity is twice the unordered count and the classical threshold $\le n$ becomes $\le 2n$.
Points live in Point2, the Euclidean plane $\mathbb{R}^2$. The ordered distance spectrum of a finite set $A$ is the list of pairwise distances from ordered pairs; ordered shell multiplicity at radius $r$ counts how many ordered pairs realize $r$. A shell is sparse when that multiplicity is at most $2|A|$.
Upstream scaffolding supplies the plane type and the spectrum/multiplicity extractors used in the filter. The diameter-shell uniqueness and nonnegativity lemmas in the same module isolate the largest shell before counting the remaining sparse ones.
proof idea
No proof: this is a def of a Prop. The body is the Mathlib filter statement that the real sequence sending $n$ to the infimum, over all $n$-point planar sets, of the number of spectrum radii whose ordered multiplicity is $\le 2n$, tends to $+\infty$ along atTop. The set comprehension and sInf encode the worst-case sparse-shell count; Tendsto ... atTop atTop is the divergence claim.
why it matters
Doc-comment frames this as the stronger RS target suggested by the shell-flux reading: sparse shells should not merely exist, their number should diverge. The module records the RS physicalization of Erdős #132; the next sibling notes a missing bridge that, once the diameter shell is peeled off, shell-flux conservation forces at least one further sparse shell. That bridge would be a finite-step step toward discharging this divergence Prop.
In the broader framework the shells are two-body recognition-energy levels, so unbounded sparse occupancy structure is a combinatorial shadow of recognition composition on planar configurations. No downstream theorem yet consumes the name (used_by is empty); it stands as the named open target rather than a proved link in T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.