convex_layer_screening_iff_threshold
plain-language theorem explainer
The eventual (filter-at-top) and finite-threshold formulations of convex-layer screening are logically equivalent. Anyone closing the remaining layer-flux step in the RS physicalization of Erdős #132 cites this to switch statement shapes freely. The proof is just the pairing of the two one-direction conversion lemmas already proved in-module.
Claim. The following are equivalent: (i) for all sufficiently large $n$, every finite planar point set $A$ with $|A|=n$ and diameter shell $\Delta$ admits first/second convex-layer data that screens the low-shell residual deep-layer case; (ii) there exists a finite threshold $N$ such that every planar set with at least $N$ points and diameter shell $\Delta$ admits such screening data.
background
This module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Convex-layer screening is the remaining layer-flux claim in that program. The bridge form asserts that eventually (in the filter atTop on cardinality) every large finite planar set whose diameter realizes a shell $\Delta$ carries first/second convex-layer data screening the low-shell residual deep-layer case. The threshold certificate is the concrete dual: exhibit a single finite $N$ after which every configuration of size at least $N$ has the same property.
Both directions between these props are already established in-module: a threshold certificate yields the eventual bridge, and conversely the eventual bridge supplies some threshold via the standard characterization of Filter.eventually_atTop.
proof idea
Term-mode Iff constructor. The forward direction is the existing lemma that converts the eventual bridge into a threshold certificate (unfold the bridge, rewrite by eventually_atTop, unpack the witness $N$). The reverse direction is the existing lemma that converts a threshold certificate into the eventual bridge (unpack $N$, unfold the bridge, rewrite by eventually_atTop). No new arithmetic or geometry is introduced.
why it matters
In the RS reading of Erdős #132, convex-layer screening is named as the exact remaining layer-flux theorem: large configurations must admit first/second layer data that kill the residual deep-layer low-shell case. Having both the filter form and the finite-$N$ form, and knowing they are equivalent, lets later arguments choose whichever packaging is convenient (asymptotic language versus an explicit certificate).
No downstream consumers are wired yet (used_by is empty), so this is presently a local hygiene lemma inside DistanceShellMultiplicity. It does not itself discharge the screening claim; it only identifies the two target shapes that a future proof of screening must hit. Framework landmarks T0–T8, RCL, and the mass ladder are not directly invoked here; the link is combinatorial geometry feeding the recognition-energy shell story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.