ordered_edges_meet_simply_comm
plain-language theorem explainer
Simple meeting of ordered planar edges is commutative: the closed segments of e and f share exactly one point exactly when those of f and e do. Anyone counting thrackle-style pairwise meetings or ordered shell multiplicities under Conway's condition would cite this. The proof is a one-line Iff constructor that applies the one-sided symmetry lemma in both directions.
Claim. For ordered edges $e,f$ given by pairs of points in the Euclidean plane $\mathbb{R}^2$, the closed segments of $e$ and $f$ share exactly one point if and only if the closed segments of $f$ and $e$ share exactly one point.
background
This module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is the shell occupancy. Ordered pairs are used for Lean simplicity, so for a positive distance the ordered multiplicity is twice the unordered one and the classical bound $\le n$ becomes $\le 2n$.
Points are elements of $\mathbb{R}^2$ (via the bipartite distance-spectrum abbreviation). Two ordered edges meet simply when their closed segments share exactly one point. That is the Conway straight-line thrackle meeting condition: it excludes overlapping collinear segments that would inflate the pairwise-meeting count past the cardinality of the point set.
The one-sided companion already shows that if $e$ and $f$ meet simply then $f$ and $e$ do, by swapping the two OnClosedSegment conjuncts and reusing the uniqueness witness.
proof idea
Term-mode Iff introduction. Both directions are the same lemma: the one-sided symmetry result that turns a simple meeting of $(e,f)$ into a simple meeting of $(f,e)$ by exchanging the two closed-segment memberships while keeping the unique intersection point. The constructor packages that lemma as the forward and reverse maps of the biconditional.
why it matters
The declaration supplies the commutative form of the thrackle meeting predicate used throughout the ordered-edge layer of the distance-shell multiplicity development. That layer supports the RS reading of Erdős #132, in which shell occupancy is counted under the Conway condition so that collinear overlaps cannot fake extra meetings. No downstream theorem currently depends on the biconditional (used-by is empty), but any later uniqueness, flux-bridge, or sparse-shell argument that needs to reorder edge pairs without re-proving uniqueness will call it. It sits purely on the combinatorial geometry side of the module; it does not itself invoke the forcing chain, RCL, or the mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.