ordered_edges_meet_comm
plain-language theorem explainer
Geometric meeting of two ordered planar edges is commutative: the closed segments of e and f intersect if and only if those of f and e do. Anyone working the Hopf–Pannwitz / thrackle side of the ordered distance-shell setup cites this to flip edge order freely. The proof is a one-line Iff constructor that applies the one-sided symmetry lemma in both directions.
Claim. For ordered edges $e,f$ in the Euclidean plane $\mathbb{R}^2$, the closed straight-line segments of $e$ and $f$ intersect if and only if the closed segments of $f$ and $e$ intersect.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count (threshold $\le n$ becomes $\le 2n$). Points are Point2, i.e. Euclidean space $\mathbb{R}^2$.
Two ordered edges meet geometrically when there exists a point lying on both closed segments. That is the correct Hopf–Pannwitz / thrackle intersection predicate; mere endpoint-disjointness is too strong and would exclude crossing diameter diagonals.
The one-sided lemma already shows that if $e$ meets $f$ then $f$ meets $e$, by swapping the two segment-membership witnesses at the common point.
proof idea
Term-mode Iff introduction. Both directions are exactly the existing one-sided symmetry lemma ordered_edges_meet_symm: from a witness point on both closed segments, swap the two conjuncts to get the reversed ordered pair. No new geometric work.
why it matters
Commutativity lets later shell-multiplicity and thrackle arguments treat edge order as immaterial when testing geometric meetings. The module sits in the RS reading of Erdős #132 (distance shells as recognition-energy shells). No downstream consumers are wired yet; the lemma is infrastructure for ordered-edge geometry beside diameter shells and sparse-shell divergence. It does not itself touch the forcing chain (T0–T8) or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.