SparseShell
plain-language theorem explainer
A finite planar point set has a sparse shell at distance r when r lies in its ordered pairwise distance spectrum and the ordered multiplicity of r is at most twice the set's cardinality. This is the ordered-pair rewrite of the classical "unordered multiplicity ≤ n" bound used in Erdős distance problems. Anyone working the RS formalization of Erdős #132, the Hopf–Pannwitz diameter bridge, or the second-sparse-shell flux argument cites this predicate. The body is a plain conjunction of spectrum membership and the multiplicity inequality.
Claim. For a finite set $A$ of points in the Euclidean plane and a real $r$, call $r$ a sparse shell of $A$ when $r$ belongs to the ordered pairwise distance spectrum of $A$ and the ordered multiplicity of shell $r$ satisfies $m_{\mathrm{ord}}(A,r)\le 2|A|$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Lean works with ordered pairs for bookkeeping; for any positive distance the 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 the non-diagonal ordered pair events under Euclidean distance. Ordered shell multiplicity counts how many such ordered pairs realize a fixed distance $r$.
Upstream, the spectrum is built from the bipartite distance spectrum infrastructure; the multiplicity predicate is the local counting companion used throughout the shell-flux and diameter arguments.
proof idea
Definitional abbreviation, not a proved theorem. The predicate is the conjunction of two atomic conditions: membership of $r$ in the ordered distance spectrum of $A$, and the inequality that ordered shell multiplicity of $r$ is at most twice the cardinality of $A$. No lemmas are applied; downstream results unfold or pattern-match on this Prop.
why it matters
SparseShell is the atomic sparsity predicate for the whole ordered formalization of Erdős #132. The global statement Erdos132Ordered asserts that every sufficiently large finite planar set admits two distinct sparse shells. HopfPannwitzOrderedDiameterBound and DiameterShellSparseBound package the classical straight-line thrackle / Hopf–Pannwitz input as "the diameter shell is sparse," supplying the first sparse shell. ExistsSecondSparseShell and SecondSparseShellFluxBridge ask for a second sparse shell after the diameter is removed; DeepLayerCase is the residual case in which no non-diameter occupied shell has yet been shown sparse, which the later geometry bridge must rule out. The companion theorem orderedShellMultiplicity_supercritical_of_not_sparse converts failure of SparseShell into a strict supercritical multiplicity bound. In RS language this is shell-occupancy control on two-body recognition-energy shells, feeding the distance-spectrum side of the forcing picture rather than the T5–T8 chain directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.