diameter_shell_sparse_from_thrackle_components
plain-language theorem explainer
Hopf–Pannwitz diameter sparsity holds for large finite point sets in the plane once the diameter graph has no two geometrically disjoint edges and the ordered straight-line thrackle bound is in force. Anyone assembling the ordered form of Erdős #132 cites this bridge. The proof is a two-step term composition: thrackle components yield an ordered diameter-edge bound, which is then rewritten as shell sparsity.
Claim. Assume that, for all sufficiently large finite $A\subset\mathbb{R}^2$, the ordered diameter-edge graph of any diameter shell has no two geometrically disjoint edges, and that any ordered edge set on $A$ with no geometrically disjoint pair has cardinality at most $2|A|$. Then every diameter shell is sparse in the ordered normalization: its ordered multiplicity is at most $2|A|$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean bookkeeping; for a positive distance, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
A diameter shell is a distance value $\Delta$ realizing the maximum pairwise distance on a finite point set $A$. SparseShell asserts that the ordered multiplicity of that shell is at most $2|A|$. The two input hypotheses are the geometric half of Hopf–Pannwitz (no two diameter edges are geometrically disjoint) and the ordered thrackle bound (any ordered edge set without geometrically disjoint pairs has size $\le 2|A|$). Together they are the thrackle-level components of diameter sparsity.
proof idea
Term-mode composition, not a tactic script. First apply the intermediate lemma that turns the two thrackle components into an ordered bound on the diameter-edge set. Then feed that bound into the rewriting lemma that converts an ordered diameter-edge cardinality bound into DiameterShellSparseBound (every diameter shell is a SparseShell). No geometric argument is reopened here; the work is pure hypothesis plumbing.
why it matters
This is the Hopf–Pannwitz sparsity bridge inside the RS treatment of Erdős #132. Downstream, erdos132_from_thrackle_and_no_deep_layer assembles the ordered Erdős #132 statement from exactly these thrackle-level components plus the low-shell no-deep-layer theorem: "Final assembly from the thrackle-level Hopf–Pannwitz components plus the low-shell no-deep-layer theorem." In the Recognition reading, diameter shells are extremal two-body recognition-energy shells; sparsity of the diameter shell is the first half of controlling shell occupancy on the distance spectrum. The result does not itself close Erdős #132; it only discharges the diameter-sparsity leg so the final assembly can combine it with the deep-layer obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.