ordered_edges_meet_simply_symm
plain-language theorem explainer
Simple meeting of ordered planar edges is symmetric: if the closed segments of e and f share exactly one point, the same holds after swapping e and f. Cited when building thrackle-style pairwise meeting counts and support-level shell relations for the Erdős #132 physicalization. Proof unpacks the unique intersection and swaps the two OnClosedSegment conjuncts.
Claim. Let $e,f$ be ordered pairs of points in $\mathbb{R}^2$. If the closed segments of $e$ and $f$ share exactly one point, then the closed segments of $f$ and $e$ share exactly one point.
background
The module DistanceShellMultiplicity records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count.
Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. Two ordered edges meet simply when their closed segments share exactly one point: $\exists!, x$ lying on both closed segments. The Conway straight-line thrackle theorem counts edges under this condition; it excludes overlapping collinear segments that would inflate the pairwise-meeting count past $|A|$.
proof idea
Term-mode unpack of unique existence. From the hypothesis obtain the unique common point $x$ together with the pair of segment-membership facts and the uniqueness certificate. Rebuild the swapped witness as the same $x$ with the two membership facts reversed. Uniqueness for the swapped pair is the original uniqueness applied to any candidate after reversing its membership pair. No external lemmas beyond the definition of simple meeting.
why it matters
Supplies the one-direction symmetry used by the immediate iff form ordered_edges_meet_simply_comm, and is applied inside support_edges_meet_simply_symm to swap support-level simple meetings of undirected edges drawn from a finite edge set. Those support relations sit in the thrackle-style counting apparatus that bounds shell multiplicities for the RS reading of Erdős #132 (distance shells as two-body recognition-energy shells). Without edge-order symmetry the ordered-pair bookkeeping would not descend cleanly to unordered support edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.