PointwiseNoDeepLayerCaseInLowShellRegime
plain-language theorem explainer
Universal geometric residual for Erdős #132: every finite planar point set whose diameter is a distance shell and which satisfies the low-shell structure hypotheses cannot realize the residual deep-layer case. Assembly theorems that pair Conway thrackle bounds with no-deep-layer cite this Prop directly. It is a pure definitional packaging of that universal quantification, not a proved theorem.
Claim. For every finite set $A$ of planar points and every real $\Delta$, if $\Delta$ is a diameter shell of $A$ and $A$ has low-shell structure at scale $\Delta$, then the deep-layer residual case does not hold for $(A,\Delta)$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the multiplicity. Ordered pairs are used for Lean simplicity, so the classical multiplicity bound $\le n$ becomes $\le 2n$ for positive distances.
A diameter shell means $\Delta$ realizes the diameter of the finite point set $A$. Low-shell structure packages the sparse-shell hypotheses under which the residual obstruction is a deep layer (a configuration with no second sparse shell). The deep-layer case is exactly that residual obstruction.
This declaration is the pointwise (all finite $A$) form of the no-deep-layer residual. The Erdős target only needs an eventual/asymptotic version, but the pointwise form is the cleaner classical geometric statement when finite exceptions are not required.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over finite planar point sets $A$ and real scales $\Delta$: diameter-shell plus low-shell structure imply negation of the deep-layer residual. No tactics or lemmas are applied; downstream results discharge or transport this Prop.
why it matters
This is the clean negative residual in the Erdős #132 assembly path. The structure Erdos132OrderedConwayNoDeepResidualPack packages Conway thrackle support together with this Prop; erdos132_from_ordered_conway_and_pointwise_no_deep_layer_live turns that package into the ordered Erdős statement.
It is definitionally interchangeable with the positive screening form: pointwise_deep_layer_screening_iff_no_deep_layer equates it to PointwiseDeepLayerScreeningCertificate, via the two directions that either extract a second sparse shell from a screening certificate or rebuild the certificate by contradiction. no_deep_layer_from_pointwise filters the pointwise statement up to the eventual residual used in the main assembly.
In RS terms this is the geometric gate that keeps distance-shell multiplicity from admitting a deep residual layer once the low-shell regime is fixed, closing the combinatorial side of the #132 physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.