ExistsSecondSparseShell
plain-language theorem explainer
Predicate that a finite planar point set carries some sparse distance shell at a radius other than a fixed diameter value. Anyone working the shell-flux bridge for the RS reading of Erdős #132 cites it as the exit branch of the layer-flux alternative. It is a pure Prop abbreviation: an existential over radii with the sparse-shell property.
Claim. For a finite set $A$ of points in the plane and a real $\Delta$, there exists $r\in\mathbb{R}$ with $r\neq\Delta$ such that the pairwise-distance shell of $A$ at radius $r$ is sparse.
background
The module physicalizes Erdős problem #132: classical distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so the classical bound $\le n$ becomes $\le 2n$.
Points live in the plane via the bipartite distance-spectrum abbreviation. A sparse shell is a radius whose ordered occupancy is low enough to meet the Erdős-type threshold. The diameter shell is the unique maximal-distance shell; $\Delta$ is that distinguished radius once it has been identified.
The surrounding development isolates residual deep-layer configurations in which no non-diameter occupied shell has yet been proved sparse. This predicate names the complementary exit: a second sparse shell already exists.
proof idea
Pure definitional Prop. Unfolds to the existential $\exists r,, r\neq\Delta\land\mathrm{SparseShell}(A,r)$. No tactics, no lemmas, no proof body beyond the formula.
why it matters
This is the exit branch of the layer-flux alternative: once in the low-shell regime, either a second sparse shell is present or only a residual deep-layer case remains. The tautological split theorem builds the alternative by case-splitting on this predicate.
Deep-layer screening is the structure whose single field maps every residual deep-layer case to this predicate; the later geometry bridge must discharge those cases. The minimal-geometry package closes the full second-sparse-shell flux bridge by the same case split: if the predicate already holds, done; otherwise finite pair-budget pressure feeds screening.
In the RS frame this is the combinatorial half of turning distance-shell occupancy into a recognition-energy flux statement, sitting under the broader distance-shell multiplicity development rather than under T0–T8 forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.