ConvexLayerScreeningBridge
plain-language theorem explainer
Names the global convex-layer screening property: every sufficiently large finite planar point set admits first/second convex-layer data that screens the low-shell residual deep-layer case at every diameter shell. Anyone closing the constructive Erdős #132 residual cites this bridge. The body is a pure Prop packaging an eventual (filter-atTop) quantifier; no proof is attached here.
Claim. Eventually as $n\to\infty$, for every finite set $A\subset\mathbb{R}^2$ with $|A|=n$ and every diameter distance $\Delta$ of $A$, there exist first/second convex-layer data $L$ for $A$ such that $L$ screens the deep-layer case of the low-shell residual at shell $\Delta$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count and the classical bound $\le n$ becomes $\le 2n$.
A diameter shell is a distance value realizing the diameter of the finite set. Convex-layer data package first- and second-layer containers on that set. Screening the deep case means those layers rule out the residual low-shell configuration in which a deep layer would still carry excess multiplicity.
The local goal is the remaining layer-flux theorem named by the plan: large configurations must admit layer data that kill that deep residual.
proof idea
Definition only: the right-hand side is the Prop $\forall^{\infty} n,;\forall A\ (:\mathrm{Finset}\ \mathrm{Point2}),\ |A|=n\Rightarrow\forall\Delta,\ \mathrm{IsDiameterShell}(A,\Delta)\Rightarrow\exists L,\ \mathrm{ConvexLayerScreensDeepCase}(A,\Delta,L)$. No tactics or lemmas fire at this site. Downstream wrappers convert it to/from a finite threshold certificate and to/from the sharper no-deep-layer target by unfolding the filter and supplying empty or concrete layer bookkeeping.
why it matters
This is the exact remaining layer-flux theorem named in the plan for the RS reading of Erdős #132. Downstream, it is equivalent both to a finite-threshold certificate and to the low-shell no-deep-layer target; the no-deep-layer form keeps the residual honest (layer containers are bookkeeping; the content is the contradiction itself).
It is one conjunct of the constructive live residual: a Conway thrackle endpoint-charge certificate together with this bridge proves Erdős #132. Threshold and converse lemmas (convex_layer_screening_from_threshold, ..._from_no_deep_layer, and the two iff theorems) route all current residual closures through this name.
In the broader RS ledger it sits in the mathematics spine that physicalizes distance shells as recognition-energy shells, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.