NoDeepLayerCaseInLowShellRegime
plain-language theorem explainer
Residual geometric target for the ordered Erdős #132 program: for all large enough planar point sets, a diameter shell together with low-shell structure forbids a deep-layer case (some non-diameter occupied shell must be sparse). Final assembly theorems cite it as the last classical geometry input beside diameter sparsity. Packaged as an eventual-atTop proposition; not proved in this declaration.
Claim. Eventually as $n\to\infty$, for every finite $A\subset\mathbb{R}^2$ with $|A|=n$ and every diameter distance $\Delta$ of $A$: if $A$ has low-shell structure at $\Delta$, then $A$ is not a deep-layer case at $\Delta$ (i.e., some occupied non-diameter shell is sparse).
background
The module physicalizes Erdős problem #132: classical distance values become two-body recognition-energy shells, and shell occupancy is multiplicity. Ordered pairs are used for Lean bookkeeping, so the classical bound $\le n$ becomes $\le 2n$ on ordered multiplicity.
Points live in the Euclidean plane (Point2). A diameter shell marks a realized maximum pairwise distance $\Delta$. A deep-layer case is the residual obstruction in which every occupied non-diameter shell fails sparsity; the later geometry bridge must rule those cases out. Low-shell structure is the finite-accounting regime left after the module's reductions, in which only this residual deep-layer possibility remains.
Upstream, deep-layer cases are recorded as structures asserting no second sparse shell; supercriticality of all non-diameter occupied shells follows. This definition names the sharp contradiction target those reductions leave.
proof idea
Definition of a proposition, not a proved theorem. The body is the filter statement ∀ᶠ n in atTop quantifying over finite planar sets of cardinality $n$, diameter shells $\Delta$, and the low-shell hypothesis, concluding negation of the deep-layer case. No tactics, no lemmas applied; it packages the residual geometric claim for downstream assembly and equivalence lemmas.
why it matters
Exact final contradiction target left by the finite accounting reductions: in the low-shell regime the residual deep-layer case cannot occur. Downstream, it is the live geometry input in every major ordered-Erdős-#132 assembly: from final components (diameter existence, Hopf–Pannwitz sparsity, and this target), from diameter sparsity, from Hopf–Pannwitz, and from several legacy thrackle routes.
It is equivalent to the structural convex-layer screening bridge: the ConvexLayerData fields are bookkeeping, and the mathematical content is exactly this proposition. That keeps the residual honest. In the RS reading, forbidding deep layers on large sets forces sparse non-diameter recognition-energy shells, which is the physical content of the #132 multiplicity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.