convex_layer_screening_threshold_from_bridge
plain-language theorem explainer
The filter-eventual form of convex-layer screening implies an explicit finite cardinality threshold. Anyone working the thresholded layer-flux certificate in the RS reading of Erdős #132 cites this direction. The argument unpacks eventual membership in the cofinite filter and reindexes from exact cardinality to the inequality N ≤ |A|.
Claim. If, for all sufficiently large $n$, every finite planar point set $A$ with $|A|=n$ admits first/second convex-layer data that screens the residual deep-layer case for every diameter shell $\Delta$, then there exists a finite threshold $N$ such that the same screening holds for every configuration with at least $N$ points and every diameter shell.
background
This module physicalizes Erdős problem #132 inside Recognition Science. Classically a distance value is a shell in the pairwise Euclidean spectrum; here it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
A diameter shell is a distance value realized as the diameter of a finite planar set $A$. Convex-layer data packages the first and second convex layers of $A$. The screening predicate asserts that this layer data rules out the residual deep-layer obstruction for low-shell flux.
Two equivalent package forms appear. The bridge is the filter-eventual statement: the screening property holds for all large enough exact cardinalities. The threshold certificate is the concrete existential form: some finite $N$ works for every set with $|A|\ge N$. This lemma converts the former into the latter.
proof idea
Term-mode unpacking of the filter quantifier. Unfold the bridge hypothesis, rewrite with Filter.eventually_atTop to obtain a witness $N$ and a tail predicate $hN$, then refine the threshold certificate at that same $N$. For an arbitrary set $A$ with $N\le|A|$ and diameter shell $\Delta$, instantiate $hN$ at cardinality $|A|$, the inequality hypothesis, the set $A$, the reflexivity proof of $|A|=|A|$, and $\Delta$. No geometric content is added; the step is pure reindexing of quantifiers.
why it matters
This is one half of the equivalence between the eventual bridge and the thresholded certificate. Downstream, convex_layer_screening_iff_threshold packages both directions so either formulation may be used interchangeably.
In the module plan the convex-layer screening bridge is the remaining layer-flux theorem: every large enough finite set admits first/second layer data screening the low-shell residual deep-layer case. The threshold form is the most concrete statement of that claim, the one a combinatorial argument would actually exhibit. Closing the equivalence keeps the RS physicalization of Erdős #132 free to switch between asymptotic and finite-$N$ language without gaps.
The result sits entirely inside the combinatorial geometry layer of the monolith; it does not itself invoke the forcing chain (T0–T8), the Recognition Composition Law, or the mass ladder, but it supplies the shell-occupancy control those physical readings rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.