DeepLayerScreening
plain-language theorem explainer
Deep-layer screening packages the claim that a residual deep-layer configuration on a finite planar point set cannot persist: if every occupied non-diameter distance shell fails to be sparse, a second sparse shell must still exist. Anyone assembling the shell-flux bridge for the RS reading of Erdős #132 cites this interface. It is a Prop-structure with a single implication field, not a proved lemma.
Claim. For a finite planar point set $A$ and a real threshold $\Delta$, deep-layer screening holds when the following implication is true: if $A$ is a deep-layer case relative to $\Delta$ (every occupied distance shell other than $\Delta$ fails to be sparse), then there exists a second sparse shell at some distance $r \neq \Delta$.
background
This module physicalizes Erdős problem #132: classical pairwise Euclidean distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. The development works with ordered non-diagonal pairs in a finite set of planar points (Point2), so positive-distance ordered multiplicity is twice the unordered count and the classical bound $\le n$ becomes $\le 2n$.
A diameter shell is a distinguished extremal occupied distance $\Delta$. A sparse shell is an occupied distance whose ordered multiplicity stays below the RS threshold. A deep-layer case is the residual situation in which no occupied non-diameter shell has yet been shown sparse: every $r$ in the ordered distance spectrum with $r \neq \Delta$ fails sparseness. The complementary exit predicate is existence of some second sparse shell after the diameter is removed.
Screening is the geometric obligation that such residual cases cannot survive: the deep-layer hypothesis must force a second sparse shell. Downstream certificates attach this obligation to low-shell structure and finite pair-budget pressure.
proof idea
No proof body: this is a Prop-structure definition. It records a single field, an implication from the deep-layer residual (no occupied non-diameter shell is sparse) to existence of a second sparse shell at some distance other than the diameter. Downstream packs and certificates supply the geometric hypotheses that discharge the field; the structure itself only names the screening obligation.
why it matters
This is the named Deep-Layer Screening interface in the shell-flux proof plan for the RS reading of Erdős #132. The pointwise certificate asks for screening under a diameter shell plus low-shell structure. The component, reduced-component, and minimal-geometry packs each carry a screening field; the two flux-bridge theorems close SecondSparseShellFluxBridge by filtering those packs and splitting on exit versus residual case.
In the residual branch, finite pair-budget pressure yields the low-shell bound that screening consumes, so the residual cannot persist. That closes the missing geometric step between ordered shell multiplicity and the second-sparse-shell flux bridge. It is local discrete geometry on planar distance shells, not a forcing-chain (T0–T8) identity, but it is the bottleneck lemma shape the multiplicity module is built to discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.