DiameterShellSparseBound
plain-language theorem explainer
Hopf–Pannwitz sparsity component: for all large enough n, every n-point planar set has sparse diameter shell under ordered multiplicity (at most 2n). Cited by anyone wiring the ordered Erdős #132 assembly or the Hopf–Pannwitz bridge from thrackle or Conway inputs. Pure Prop definition: eventual quantification over finite point sets and diameter shells, no proof body.
Claim. For all sufficiently large $n$, every finite $A\subset\mathbb{R}^2$ with $|A|=n$ and every real $\Delta$ that is a diameter shell of $A$ is a sparse shell of $A$ (ordered pairwise multiplicity at most $2n$).
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, and its multiplicity is shell occupancy. Lean works with ordered pairs, so for positive distances ordered multiplicity is exactly twice the unordered count and the classical threshold $\le n$ becomes $\le 2n$.
A diameter shell is a distance value $\Delta$ realized as the maximum pairwise distance of a finite point set $A\subset\mathbb{R}^2$. A sparse shell is one whose ordered multiplicity stays at most $2n$ when $|A|=n$. The present declaration packages the asymptotic claim that every diameter shell is sparse.
That claim is the sparsity half of the Hopf–Pannwitz theorem in ordered normalization, and the module treats it as the straight-line thrackle bridge into the Erdős #132 assembly.
proof idea
No proof: this is a Prop definition. The body is an eventual filter statement (∀ᶠ n in atTop) quantifying over finite point sets of cardinality $n$ and over reals $\Delta$ that satisfy the diameter-shell predicate, asserting the sparse-shell predicate. Downstream theorems discharge it by filter_upwards from an ordered multiplicity bound, a diameter Conway thrackle bound, or the pair of thrackle components (no disjoint diameter edges plus ordered thrackle bound).
why it matters
This interface is the sparsity leg of Hopf–Pannwitz in the ordered setting. hopf_pannwitz_ordered_from_diameter_sparsity reduces ordered Hopf–Pannwitz to this Prop once diameter-shell existence is known; HopfPannwitzComponentPack stores it beside that existence fact. The Erdős #132 assembly erdos132_from_diameter_sparsity_and_no_deep_layer feeds it (via the Hopf–Pannwitz bridge) together with the low-shell no-deep-layer hypothesis into the ordered Erdős #132 statement.
Several entry theorems manufacture the Prop from combinatorial inputs: ordered multiplicity bounds, diameter Conway thrackle bounds, and the two thrackle components. In the RS reading, diameter-shell sparsity is the occupancy control on the maximum two-body recognition-energy shell, the geometric bottleneck in the physicalization of Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.