unorderedEdgeOfOrdered_swap
plain-language theorem explainer
Reversing the two endpoints of an ordered pair of planar points leaves the corresponding unordered edge unchanged. Anyone moving from ordered-pair distance shells to undirected support cites this invariance. The argument is a short case split on the pair plus the standard equality criterion for two-element multisets.
Claim. For every ordered pair $e=(a,b)$ of points in $\mathbb{R}^2$, the unordered edge of $(b,a)$ equals the unordered edge of $(a,b)$. Equivalently, the map that forgets orientation is invariant under swapping the two coordinates.
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 whose occupancy is the shell multiplicity. Lean works with ordered pairs for bookkeeping; for positive distances the ordered multiplicity is exactly twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
Points are planar: $\mathrm{Point2}$ is Euclidean space $\mathbb{R}^2$. An ordered edge is a pair in $\mathrm{Point2}\times\mathrm{Point2}$. The forget-orientation map sends such a pair to the two-element multiset (symmetric square) on the two endpoints. The present lemma records that this undirected support does not depend on which endpoint is written first.
proof idea
Term-mode proof by cases on the product pair $e=(a,b)$. Unfold the forget-orientation definition (symmetric-square constructor on the ordered pair). The goal reduces to equality of two $\mathrm{Sym2}$ values, discharged by the standard criterion $\mathrm{Sym2.mk_eq_mk_iff}$: the swapped pair matches the original under the reverse branch of the disjunction, witnessed by reflexivity.
why it matters
This is a tiny orientation-invariance fact needed whenever diameter or shell arguments pass from ordered representatives to undirected support edges. Downstream it is used by the theorem that shared-endpoint diameter representatives of distinct unordered diameter support edges meet simply, which "discharges the endpoint-sharing half of the diameter-support Conway condition." In the broader RS reading of Erdős #132, diameter shells and sparse-shell flux bridges rely on clean undirected support; without swap-invariance, ordered bookkeeping would double-count or misidentify edges when endpoints are shared.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.