LowShellStructure
plain-language theorem explainer
A finite planar point set is in the low-shell regime when its number of occupied pairwise-distance shells is at most half the cardinality plus two. This is the gate hypothesis for convex-layer screening in the RS treatment of Erdős #132: once few shells remain, either a second sparse shell appears or only a residual deep-layer obstruction is left. It is a bare Prop structure with a single inequality field, not a proved theorem.
Claim. For a finite set $A$ of points in the plane and a real parameter $\Delta$, the configuration has low-shell structure when the number of occupied pairwise Euclidean distance shells satisfies $\mathrm{occupiedShellCount}(A) \le |A|/2 + 2$.
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 classical thresholds $\le n$ become $\le 2n$.
Points live in Point2 (the bipartite planar point type from the distance-spectrum infrastructure). An occupied shell is a realized positive pairwise distance value; the count of such shells is the radial spectrum size of $A$. The real parameter $\Delta$ is the diameter-shell scale against which sparsity and deep-layer residuals are later judged.
Low-shell structure marks the regime in which ordinary shell-counting no longer supplies a second sparse shell by itself, so convex-layer geometry must take over. Downstream packages treat it as the hypothesis that forces the layer-flux alternative: second sparse shell present, or only a deep-layer obstruction remains.
proof idea
No proof body: this is a Prop-valued structure definition. It packages a single field, the inequality that the occupied shell count is at most half the set cardinality plus two. Downstream theorems and certificates simply assume or discharge an instance of this structure rather than unfolding a construction.
why it matters
This is the regime gate for the finite accounting reductions toward Erdős #132 in Recognition Science. Downstream, PointwiseNoDeepLayerCaseInLowShellRegime and NoDeepLayerCaseInLowShellRegime assert that under low-shell structure (and a diameter shell) the residual deep-layer case cannot occur; PointwiseDeepLayerScreeningCertificate and ConvexLayerScreensDeepCase turn the same hypothesis into a Clemen–Dumitrescu–Liu style convex-layer screen that either kills the deep layer or produces the missing second sparse shell.
The flux-bridge theorems second_sparse_shell_flux_bridge_from_components and second_sparse_shell_flux_bridge_from_minimal_geometry (and the packs ShellFluxComponentPack, ShellFluxMinimalGeometryPack) thread low-shell structure into the global second-sparse-shell bridge. In RS terms the shells are recognition-energy shells; controlling their multiplicity is the combinatorial half of the physicalized #132 target. The definition itself closes no open geometric question; it names the hypothesis those screening lemmas need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.