no_deep_layer_from_pointwise
plain-language theorem explainer
Pointwise absence of deep-layer configurations under low-shell diameter hypotheses upgrades to the eventual large-n form required by the Erdős #132 assembly. Anyone wiring the distance-shell multiplicity contradiction would cite this bridge. The argument is a one-line filter_upwards: the universal statement over all finite point sets immediately yields the cofinite-cardinality version.
Claim. If every finite planar point set $A$ and every diameter-shell distance $\Delta$ with low-shell structure satisfies $\neg$ deep-layer case, then eventually (for all sufficiently large $n$) every $n$-point set obeys the same conclusion: no diameter shell $\Delta$ with low-shell structure can be a deep-layer case.
background
This module physicalizes Erdős problem #132: classical pairwise Euclidean distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity, so the classical multiplicity bound $\le n$ becomes $\le 2n$.
A diameter shell is a distance value $\Delta$ realized as the diameter of a finite planar point set $A$. Low-shell structure packages the sparse-shell hypotheses under which the residual deep-layer case is the last geometric obstruction. The pointwise no-deep-layer predicate asserts that obstruction never occurs for any finite $A$ and any such $\Delta$. The eventual form restricts to cofinitely many cardinalities $n=|A|$, which is exactly what the Erdős #132 assembly consumes after finite accounting reductions.
The eventual predicate is the sharp geometric target left by those reductions; the pointwise form is the cleaner classical statement when small finite exceptions are unnecessary.
proof idea
Term-mode proof via filter_upwards on the atTop filter. After introducing the cardinality $n$, an $n$-point set $A$, a candidate diameter shell $\Delta$, and the low-shell hypothesis, the goal is exactly an instance of the pointwise predicate. Apply the hypothesis $h$ directly to $A$ and $\Delta$; the cardinality hypothesis is unused because the pointwise statement already quantifies over all finite sets.
why it matters
Closes the last packaging step between the classical geometric no-deep-layer statement and the eventual theorem the Erdős #132 assembly actually calls. Downstream, no_deep_layer_from_pointwise_screening_certificate composes this bridge with the pointwise screening certificate: positive screening yields the pointwise no-deep predicate, which this theorem lifts to the eventual form. That eventual form is the residual contradiction target in the low-shell regime after finite accounting. In the RS reading, forbidding deep layers on sparse diameter shells constrains two-body recognition-energy shell occupancy, the physical content of the distance-multiplicity problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.