HopfPannwitzOrderedDiameterBound
plain-language theorem explainer
For all large enough finite planar point sets, some Euclidean diameter value is a sparse ordered distance shell. This proposition packages the classical Hopf-Pannwitz geometric input for the ordered-pair form of Erdős problem #132 and is left unproved here. Anyone assembling the shell-flux route to ordered Erdős #132 cites it as the diameter-sparsity hypothesis. It is a bare Prop abbreviation whose body is an eventual filter statement, not a theorem with a proof.
Claim. For all sufficiently large $n$, every finite set $A\subset\mathbb{R}^2$ with $|A|=n$ admits a real number $\Delta$ such that $\Delta$ is a diameter shell of $A$ and the ordered distance shell at $\Delta$ is sparse.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell, and its multiplicity is the shell occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is exactly twice the usual unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
A diameter shell is a distance realized as the maximum pairwise separation of a finite planar point set. A sparse shell is one whose ordered multiplicity stays inside the Erdős bound. Hopf-Pannwitz is the classical planar fact that diametral pairs are sparse; this declaration names that fact as an asymptotic proposition over cardinality.
The Prop is deliberately a statement surface only. Component packs and flux bridges later inhabit it; the classical geometry is not re-proved in this module.
proof idea
No proof body: the declaration is a proposition abbreviation. Its right-hand side is the filter statement that, eventually along the filter at infinity on $n$, every $n$-point finite planar set $A$ admits some real $\Delta$ that is both a diameter shell and a sparse shell.
Downstream constructors inhabit the proposition by pairing a diameter-existence half with a diameter-sparsity half. One standard route takes a Hopf-Pannwitz component pack, filters upward on its diameter-exists and diameter-sparse fields, and assembles the required witness $\Delta$ for each large $A$.
why it matters
This proposition is the classical geometric gate for every ordered assembly of Erdős #132 in the module. The flux-bridge theorem, the component-package theorem, the reduced-component assembly, the minimal-geometry pack, and the sharp no-deep-layer final assembly all take it as a named hypothesis and discharge the remaining counting internally.
The design choice is explicit in the doc-comment: Hopf-Pannwitz supplies the diameter shell as the first sparse shell and is left as classical input on this statement surface, while the shell-flux bridge carries the rest. In the RS reading, that sparse diameter shell is the first sparse two-body recognition-energy shell; once it exists, flux and component arguments push sparsity down the distance spectrum. The separation keeps finite-order bookkeeping (implemented here) cleanly apart from planar geometry (imported as this Prop).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.