diameterOrderedEdges
plain-language theorem explainer
For a finite planar point set and a real shell value Δ, this is the finset of ordered distinct pairs realizing Euclidean distance exactly Δ. It is the ordered diameter-edge set used throughout the module’s thrackle and Hopf–Pannwitz counting. Construction is a classical filter of the ordered non-diagonal product on the equality dist(p,q)=Δ.
Claim. Given a finite set $A$ of points in the Euclidean plane and a real number $\Delta$, let $E_\mathrm{ord}(A)$ be the set of ordered pairs $(p,q)\in A\times A$ with $p\neq q$. Define the ordered diameter-edge set as $\{(p,q)\in E_\mathrm{ord}(A):\|p-q\|=\Delta\}$.
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum; in RS language it is a two-body recognition-energy shell, and multiplicity is shell occupancy. Lean works with ordered pairs for simplicity. For positive distance, ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. The ambient ordered event set is the non-diagonal product: all $(p,q)$ drawn from a finite $A$ with $p\neq q$. Filtering that set by exact distance $\Delta$ yields the ordered edges of a single shell. When $\Delta$ is a diameter shell (maximal pairwise distance), those edges feed Conway thrackle geometry and Hopf–Pannwitz-type multiplicity bounds.
proof idea
Definitional, not a proof. Under classical choice, take the finset of ordered non-diagonal pairs in $A$ and retain only those pairs whose Euclidean distance equals the given shell value $\Delta$. No lemmas are applied beyond finset filter and the ambient ordered-pair construction.
why it matters
This is the basic edge object for every diameter-shell argument in the module. Downstream, the ordered diameter edges appear in the (intentionally false-as-stated) legacy Conway predicate on ordered edges, the correct support-level Conway thrackle condition, the diameter Conway thrackle bound $\mathrm{orderedShellMultiplicity}\le 2|A|$, and the Hopf–Pannwitz-style theorem that no-disjoint-diameter-edges plus an ordered thrackle bound imply the diameter ordered-multiplicity bound. It also feeds cardinality comparisons between ordered representatives and unordered support. In the RS reading of Erdős #132, these edges are the two-body events whose occupancy must stay controlled on the diameter shell.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.