ConvexLayerScreensDeepCase
plain-language theorem explainer
Defines the local screening property: given a finite planar set, a diameter distance, and first/second convex-layer data, low-shell structure on that diameter forces the residual deep-layer case to fail. Combinatorial geometers working the Clemen–Dumitrescu–Liu layer bridge for Erdős #132 cite it as the per-configuration predicate. The body is a one-line Prop abbreviation, not a proved implication.
Claim. For a finite planar point set $A$, a real distance $\Delta$, and an abstract first/second convex-layer package on $A$, the package screens the deep-layer residual when: if $A$ has low-shell structure at $\Delta$, then the deep-layer case at $\Delta$ does not hold.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count (so classical $\le n$ becomes $\le 2n$). Points live in the plane as Point2.
ConvexLayerData is an intentionally structural package: two finite layers $L_1,L_2\subseteq A$, without yet fixing the geometric construction of convex layers. The screening predicate only needs those handles.
Locally one fixes a diameter shell $\Delta$ (a distance realizing the diameter of $A$). Low-shell structure and the deep-layer residual case are the two competing regimes for how that diameter can be realized; screening means the layer package rules the deep residual out once low-shell structure is present.
proof idea
No proof obligation: the declaration is a definitional abbreviation of a Prop. It packages the implication "low-shell structure at $\Delta$ implies not deep-layer case at $\Delta$" under an unused layer-data parameter, so downstream global statements can quantify over existence of suitable ConvexLayerData while keeping the screening condition a single named predicate.
why it matters
This is the local Clemen–Dumitrescu–Liu-style convex-layer bridge named in the plan. Downstream, ConvexLayerScreeningBridge lifts it to a global asymptotic: for all large enough $n$, every $n$-point set and every diameter shell admits layer data that screens the low-shell residual deep-layer case. ConvexLayerScreeningThresholdCertificate is the concrete finite-$N$ form of the same claim.
In the RS reading, shell multiplicity is occupancy of a two-body recognition-energy shell. Closing the layer-flux gap is the remaining combinatorial step toward the ordered-distance multiplicity bound that physicalizes Erdős #132. The definition itself does not invoke the forcing chain (T5–T8) or RCL; it sits entirely on the geometric side of that physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.