hopf_pannwitz_ordered_from_components
plain-language theorem explainer
From a pack that splits diameter-shell existence from diameter-shell sparsity, one obtains the ordered Hopf–Pannwitz diameter bound: for all large enough finite planar point sets, some diameter distance is a sparse shell. Anyone wiring the Erdős #132 reduction cites this bridge lemma. The proof is a pure filter combination of the two pack fields, with no new geometry.
Claim. Suppose diameter shells eventually exist for large finite planar sets, and the diameter shell is sparse. Then eventually, for every $n$-point set $A\subset\mathbb{R}^2$, there exists a distance $\Delta$ that is both a diameter shell of $A$ and a sparse shell of $A$.
background
This module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. The development works with ordered pairs, so for a positive distance the ordered multiplicity is twice the unordered one and the classical threshold $\le n$ becomes $\le 2n$.
The target statement is the ordered Hopf–Pannwitz diameter bound: eventually every $n$-point planar set admits a distance $\Delta$ that is simultaneously a diameter shell and a sparse shell. The input is a component pack that factors this into two independent claims: eventual existence of a diameter shell, and a sparsity bound on that diameter shell. Existence is finite-order bookkeeping (a nonempty ordered distance spectrum has a maximum); the genuine geometry sits in the sparsity half.
proof idea
Term-mode filter proof. Apply filter_upwards to the pack's two fields (eventual diameter existence and diameter sparsity). For a large $n$ and an $n$-point set $A$, unpack a diameter shell $\Delta$ from existence, then feed that same $\Delta$ into the sparsity bound. The resulting witness is exactly a diameter shell that is sparse, which is the ordered Hopf–Pannwitz diameter bound. No geometric argument is added here.
why it matters
This is the current bridge from the split Hopf–Pannwitz components to the single ordered diameter bound used downstream. The final assembly theorem erdos132_from_final_components applies it directly: given the component pack and a no-deep-layer hypothesis in the low-shell regime, it obtains the ordered Erdős #132 statement. A sibling reduction shows that once diameter-shell existence is proved, Hopf–Pannwitz collapses to the diameter-sparsity theorem alone, again by feeding a pack into this lemma.
In the RS reading, sparse diameter shells are the first sparse two-body recognition-energy shells; they seed the shell-flux bridge that turns classical distance geometry into the multiplicity bound of Erdős #132. The lemma itself is pure bookkeeping, but it is the seam where the classical geometric inputs enter the RS assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.