erdos132_from_hopf_pannwitz_and_no_deep_layer
plain-language theorem explainer
Hopf–Pannwitz diameter sparsity together with the exact low-shell no-deep-layer theorem imply Erdős #132 in ordered-pair form: every large finite planar set has two distinct sparse distance shells. Discrete geometers and RS shell-flux readers cite this as the sharp assembly after finite counting is finished. The proof is a one-line term that packages the no-deep-layer hypothesis into the minimal-geometry pack and applies the prior Hopf–Pannwitz-plus-minimal-geometry theorem.
Claim. Assume that for all sufficiently large finite planar point sets the diameter distance shell is sparse (Hopf–Pannwitz in ordered normalization), and that in the low-shell regime the residual deep-layer case never occurs on a diameter shell. Then for all sufficiently large $n$, every planar $n$-point set admits two distinct sparse ordered distance shells (Erdős problem #132, ordered form).
background
The module physicalizes Erdős #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 bookkeeping, so the classical bound $\le n$ becomes $\le 2n$ on ordered multiplicity.
Erdos132Ordered asserts that eventually every $n$-point planar set has two distinct sparse shells. HopfPannwitzOrderedDiameterBound is the classical geometric input that the diameter shell is eventually sparse (existence of a diameter shell is separate finite-order bookkeeping). NoDeepLayerCaseInLowShellRegime is the sharp residual geometric claim left after finite accounting: on a diameter shell in the low-shell regime, the deep-layer case cannot occur.
Upstream, erdos132_from_hopf_pannwitz_and_minimal_geometry already reduces Erdős #132 to Hopf–Pannwitz plus a single deep-layer screening bridge packaged as ShellFluxMinimalGeometryPack.
proof idea
One-line term wrapper. Apply erdos132_from_hopf_pannwitz_and_minimal_geometry to the given Hopf–Pannwitz hypothesis, feeding it the pack produced by minimal_geometry_pack_of_no_deep_layer from the no-deep-layer hypothesis. No new geometry is proved here; the step only identifies the exact no-deep-layer theorem with the remaining screening bridge in the minimal-geometry pack.
why it matters
This is the current sharp final assembly for the RS reading of Erdős #132: all finite counting is implemented, so the only live geometric inputs are Hopf–Pannwitz diameter sparsity and impossibility of the low-shell residual deep-layer case (doc-comment). Downstream, erdos132_from_final_components routes a component pack through this theorem, and erdos132_from_diameter_sparsity_and_no_deep_layer swaps the Hopf–Pannwitz surface for a pure diameter-sparsity bound while keeping the same no-deep-layer input.
In the framework, sparse shells are recognition-energy shells with controlled occupancy; the diameter shell is the first sparse shell supplied by classical geometry, and the no-deep-layer clause closes the residual case that finite shell-flux bookkeeping cannot kill. The live endpoint named downstream is Erdos132CurrentLiveResidual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.