HopfPannwitzComponentPack
plain-language theorem explainer
Packages the two classical inputs of the ordered Hopf–Pannwitz diameter bound: eventual existence of a diameter shell, and sparsity of every such shell. Anyone assembling the ordered Erdős #132 pipeline cites this pack instead of threading the two filters separately. It is a pure Prop structure with no proof body; downstream theorems filter both fields at once.
Claim. A proposition asserting both of the following for all sufficiently large finite planar point sets $A$: (i) the ordered distance spectrum of $A$ attains a maximum value $\Delta$ (a diameter shell exists); (ii) every diameter shell of $A$ is sparse in the ordered normalization (ordered multiplicity at most $2|A|$).
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 unordered bound $\le n$ becomes $\le 2n$.
A diameter shell is a realized maximum distance $\Delta$ on a finite set $A\subset\mathbb{R}^2$. Existence of such a shell for large $|A|$ is finite-order bookkeeping: the nonempty ordered spectrum has a maximum. The genuine geometric content of Hopf–Pannwitz is the sparsity bound on that shell (the straight-line thrackle bridge), not maximum existence. The two statements are therefore kept as separate eventual properties and only later conjoined.
Sibling notions include ordered shell multiplicity, the sparse-shell predicate, and uniqueness of the diameter shell when it exists.
proof idea
No proof: this is a structure of type Prop whose fields are exactly the two named eventual properties (diameter-shell existence for large $n$, and sparsity of every diameter shell). Inhabitants are pairs of proofs of those two filters. Downstream, hopf_pannwitz_ordered_from_components applies filter_upwards to both fields and reconstructs the combined ordered Hopf–Pannwitz diameter bound.
why it matters
This pack is the current bridge into the ordered Hopf–Pannwitz diameter bound. The immediate consumer is hopf_pannwitz_ordered_from_components, which turns an inhabitant into HopfPannwitzOrderedDiameterBound. That bound is then fed to erdos132_from_final_components, the fully reduced assembly theorem for ordered Erdős #132, whose remaining classical geometry inputs are exactly: diameter-shell existence, Hopf–Pannwitz diameter sparsity, and absence of a residual deep-layer case in the low-shell regime.
In the RS reading, diameter sparsity controls occupancy of the highest two-body recognition-energy shell. Packaging existence and sparsity separately keeps bookkeeping distinct from thrackle geometry, so each classical input can be discharged or replaced independently without rewriting the Erdős #132 assembly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.