orderedShellMultiplicity_supercritical_of_not_sparse
plain-language theorem explainer
An occupied distance shell that fails the sparse-shell bound is supercritical: its ordered multiplicity strictly exceeds twice the point-set cardinality. Discrete geometers and RS workers on the Erdős #132 physicalization cite this when turning non-sparseness into a strict occupancy lower bound. The proof is a one-line unfolding of the sparse-shell predicate plus negation of the inequality.
Claim. Let $A$ be a finite planar point set and $r\in\mathbb{R}$. If $r$ lies in the ordered distance spectrum of $A$ and the shell at $r$ is not sparse (ordered multiplicity is not $\le 2|A|$), then the ordered multiplicity satisfies $2|A| < m_{\mathrm{ord}}(A,r)$.
background
This module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean distance set; physically it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is exactly twice the usual unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
Points are elements of the Euclidean plane $\mathbb{R}^2$. The ordered distance spectrum of a finite set $A$ is the image of non-diagonal ordered pair events under Euclidean distance. Ordered shell multiplicity counts the ordered pairs realizing a fixed distance $r$. A sparse shell is an occupied shell whose ordered multiplicity is at most $2|A|$ (the ordered rewrite of classical unordered multiplicity $\le n$).
proof idea
Pure definitional logic. Sparse shell means spectrum membership together with ordered multiplicity $\le 2|A|$. Unfold that predicate at the non-sparseness hypothesis; with spectrum membership already given, the remaining conjunct fails, so Nat.not_le yields the strict inequality $2|A| <$ ordered multiplicity. No geometric lemmas are invoked.
why it matters
Feeds the deep-layer case analysis in the same module. A deep-layer case is a configuration in which no non-diameter occupied shell has yet been shown sparse; the companion theorem then concludes every such non-diameter shell is supercritical. That supercritical occupancy is the quantitative pressure the later geometry bridge must use to rule deep-layer cases out, closing the RS reading of Erdős #132. The result sits in the mathematics layer on discrete geometric constraints for recognition shells, not on the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.