convex_layer_screening_from_threshold
plain-language theorem explainer
A finite-threshold certificate for convex-layer screening implies the filter-eventual form of the same statement. Anyone packaging the remaining layer-flux step of the ordered Erdős #132 argument cites this direction. The proof unpacks the existential N and rewrites eventual membership in atTop as a concrete tail bound.
Claim. If there exists a finite $N$ such that every finite point set $A\subset\mathbb{R}^2$ with $|A|\ge N$ and every diameter shell $\Delta$ of $A$ admits convex first/second-layer data screening the low-shell residual deep-layer case, then the same screening property holds for all sufficiently large cardinalities $n$ (in the filter sense $\forall^{\infty} n$ at $+ fty$).
background
This module physicalizes Erdős problem #132: classical pairwise distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
Two equivalent packagings of the remaining convex-layer flux theorem appear here. The threshold certificate asks for an explicit finite $N$ beyond which every configuration of size at least $N$ with a diameter shell admits first/second-layer data that screens the low-shell residual deep-layer case. The bridge form states the same claim as an eventual property along atTop: for all large enough cardinalities $n$, every $n$-point set with a diameter shell admits such screening data.
Diameter shells are the unique maximal-distance shells of a finite planar set. Convex-layer data package the outer convex layers used to control residual deep-layer flux in the ordered-shell argument.
proof idea
Term-mode unpacking of the two Prop aliases. Destructure the threshold certificate to a witness $N$ and its universal quantification. Unfold the bridge definition and rewrite Filter.eventually_atTop to an existential tail. Reuse the same $N$, then for any $n\ge N$ and any set $A$ with $|A|=n$, feed $|A|\ge N$ into the threshold hypothesis (via rewriting the cardinality equality) and discharge the diameter-shell hypothesis unchanged. No geometric lemmas are invoked; the step is pure filter bookkeeping.
why it matters
This is one half of the equivalence between the eventual bridge and the concrete threshold certificate (convex_layer_screening_iff_threshold). Downstream, the live Erdős #132 assembly erdos132_from_ordered_conway_and_threshold_convex_layer_screening_live takes the threshold form as an explicit hypothesis alongside a Conway thrackle support bound, then routes through the bridge-based assembly. In the RS reading, closing convex-layer screening removes the residual deep-layer flux obstruction on ordered distance-shell multiplicities. The declaration itself is pure logic glue; the geometric content lives in whatever supplies the threshold certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.