erdos132_from_hopf_pannwitz_and_reduced_components
plain-language theorem explainer
From the classical Hopf–Pannwitz diameter sparsity bound and a reduced shell-flux component package, every sufficiently large finite planar point set has two distinct sparse distance shells (ordered Erdős #132). Cite this as the final assembly step after the pair-budget pressure work. The proof is a one-line wrapper: reduce the package, then apply the non-reduced assembly lemma.
Claim. Assume the Hopf–Pannwitz ordered diameter bound: for all large $n$, every planar $n$-point set $A$ admits a diameter shell $\Delta$ that is sparse. Assume also a reduced shell-flux component package (low-shell structure under pair-budget pressure, plus deep-layer screening). Then the ordered Erdős #132 statement holds: for all large $n$, every planar $n$-point set has two distinct sparse distance shells.
background
This module physicalizes Erdős problem #132 inside Recognition Science. Classically a distance value is a shell in the pairwise Euclidean spectrum; here it is a two-body recognition-energy shell whose multiplicity is shell occupancy. The development uses ordered pairs for Lean bookkeeping: for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Erdos132Ordered asserts that for all sufficiently large finite planar sets there exist two distinct sparse shells. HopfPannwitzOrderedDiameterBound is the classical geometric input: eventually every $n$-point set has a diameter shell that is sparse (Hopf–Pannwitz supplies sparsity of the diameter; existence of a maximum distance is separate finite bookkeeping). ShellFluxReducedComponentPack is the sharper remaining geometry package after the finite pair-budget pressure work: low-shell structure once pressure holds on a diameter shell, plus deep-layer screening of the residual case.
The module doc frames the only nontrivial geometry left as screening that residual deep-layer case once its low-shell bound comes from finite counting.
proof idea
Term-mode one-line wrapper. Convert the reduced package $C$ to the older full component pack by shell_flux_component_pack_of_reduced, then feed that pack together with the Hopf–Pannwitz hypothesis into erdos132_from_hopf_pannwitz_and_components. No new geometric argument appears at this site; the reduction only collapses the definitional exit-versus-residual split already recorded in the reduced pack.
why it matters
Final assembly from the sharper reduced component package (doc-comment). It closes the RS reading of Erdős #132 once Hopf–Pannwitz is granted as classical input and the reduced flux components (low-shell structure under pair-budget pressure, deep-layer screening) are in hand. In the module hierarchy this sits above the diameter-shell uniqueness and sparsity infrastructure and above the flux-bridge siblings (SparseShellsDiverge, SecondSparseShellFluxBridge). No downstream consumers are wired yet in the graph; the declaration is the terminal ordered #132 theorem on this path. Framework role: distance shells as recognition-energy shells, with ordered multiplicity the occupancy count—pure mathematics feeding the RS geometry stack rather than a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.