ConvexLayerScreeningThresholdCertificate
plain-language theorem explainer
There is a finite cardinality threshold N so that every planar point set of size at least N admits first/second convex-layer data screening the residual deep-layer case on every diameter shell. Cite this when assembling the ordered Erdős #132 residual after Conway-type counting. The declaration is a Prop packaging that existential threshold, not a proved numerical bound.
Claim. There exists $N\in\mathbb{N}$ such that for every finite planar point set $A$ with $|A|\ge N$ and every real $\Delta$ that is a diameter shell of $A$, there exist first and second convex-layer data $L$ for $A$ making the low-shell structure of $\Delta$ incompatible with the deep-layer residual case for $\Delta$.
background
The module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity: for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$. Points are elements of the Euclidean plane $\mathbb{R}^2$.
Convex-layer data is an abstract package of two subsets $L_1,L_2\subseteq A$ (first and second layers), kept structural so geometric constructions can be supplied later. Screening the deep case means: if the low-shell structure holds for a chosen diameter shell $\Delta$, then the deep-layer residual is ruled out. That is the local Clemen–Dumitrescu–Liu style convex-layer bridge used in the plan.
proof idea
Definitional packaging only. The certificate is the proposition $\exists N,\forall A,(|A|\ge N\to\forall\Delta,(\mathrm{diameter\ shell}\to\exists L,\mathrm{screens\ deep\ case}))$. There is no tactic proof; the body is the Prop equation itself. Downstream one-line wrappers convert this threshold form to the filter-eventual bridge via Filter.eventually_atTop, and conversely extract some $N$ from an eventual statement.
why it matters
This is the most concrete residual statement of the remaining layer theorem in the ordered Erdős #132 assembly. It feeds convex_layer_screening_from_threshold and the converse, hence the equivalence of thresholded and eventual bridge forms. The live assembly erdos132_from_ordered_conway_and_threshold_convex_layer_screening_live takes a Conway thrackle support bound plus this certificate to conclude the ordered Erdős #132 claim. It also appears as a field of Erdos132OrderedConwayThresholdLayerResidualPack. In the RS reading, bounding shell multiplicity controls recognition-energy occupancy on distance shells; the threshold isolates the geometric layer residual after combinatorial counting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.