unorderedEdgeOfOrdered
plain-language theorem explainer
Maps an ordered pair of planar points to the corresponding unordered edge in Sym₂. Distance-shell and thrackle arguments cite it whenever ordered-pair bookkeeping must be quotiented by orientation. The body is the one-line constructor Sym2.mk.
Claim. Given an ordered pair $e=(p,q)$ of points in $\mathbb{R}^2$, write $\mathrm{unorderedEdgeOfOrdered}(e)$ for the unordered edge $\{p,q\}\in\mathrm{Sym}_2(\mathbb{R}^2)$. Orientation is forgotten; the reverse pair yields the same edge.
background
The module physicalizes Erdős problem #132: a Euclidean distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Lean works with ordered pairs of planar points for simplicity; for positive distances the ordered multiplicity is exactly twice the classical unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Here Point2 is the Euclidean plane $\mathbb{R}^2$ (via the bipartite distance-spectrum abbreviation). Unordered edges live in $\mathrm{Sym}_2(\mathrm{Point2})$, the type of unordered pairs. This definition is the forgetful map from ordered representatives to that Sym₂ edge, used whenever support classes, diameter edges, or thrackle certificates are stated on unordered edges while computation stays ordered.
proof idea
One-line definition: apply the standard constructor Sym2.mk to the ordered pair. No lemmas, no case split. The adjacent comment records the immediate consequence that reversing the ordered representative leaves the unordered edge unchanged.
why it matters
Bridge between the module's ordered-pair API and its unordered support geometry. Downstream, chosenSupportRepresentative_unordered recovers the Sym₂ class of a chosen ordered representative via this map; chosenSupportRepresentative_injective uses that recovery to prove injectivity on unordered support. Diameter certificates (DistinctDiameterRepresentativesMeetSimply, EndpointDisjointDiameterRepresentativesMeetSimply, EndpointDisjointDiameterIntersectionUniqueCertificate) and thrackle endpoint charging (endpoint_charging_of_incident_vertex, mem_unorderedEdgeSupport_iff) all phrase uniqueness and incidence on unordered edges while quantifying over ordered diameter or incident pairs, so they route through this forgetful map. In the RS reading, it is the bookkeeping step that converts ordered two-body events into orientation-free shell edges without changing occupancy counts up to the factor of two fixed by the module convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.