ordered_edges_meet_swap_right
plain-language theorem explainer
Swapping the two endpoints of the second ordered edge leaves geometric meeting unchanged: if the closed segment of e meets the segment from c to d, it also meets the segment from d to c. Anyone working with ordered-pair thrackle or Hopf–Pannwitz predicates in the plane will cite this. The proof unpacks the intersection witness and applies closed-segment endpoint symmetry.
Claim. Let $e$ be an ordered pair of points in $\mathbb{R}^2$, and let $c,d\in\mathbb{R}^2$. If the closed straight-line segment of $e$ intersects the closed segment from $c$ to $d$, then it also intersects the closed segment from $d$ to $c$.
background
The module Distance Shell Multiplicity 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: for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. Two ordered edges meet geometrically when their closed straight-line segments share a point: there exists $x$ lying on both closed segments. Geometric disjointness (no shared point on the closed segments) is the correct Hopf–Pannwitz / thrackle predicate; mere endpoint-disjointness is too strong and would exclude crossing diameter diagonals.
The supporting fact is closed-segment symmetry: if $x$ lies on the closed segment from $a$ to $b$, then it lies on the closed segment from $b$ to $a$ (reparametrize the convex combination by $1-t$).
proof idea
Term-style unpack-and-rebuild. Destructure the geometric-meeting hypothesis to an intersection point $x$ together with membership of $x$ on both closed segments. Keep the membership on the first edge $e$ unchanged. Replace membership of $x$ on the segment from $c$ to $d$ by membership on the segment from $d$ to $c$ via on_closed_segment_symm, then repackage the same witness $x$.
why it matters
Geometric meeting is the intersection predicate underlying thrackle-style counting of ordered edges in the planar distance spectrum. Endpoint order is an artifact of the ordered-pair encoding used throughout the module; this lemma shows that meeting is insensitive to reversing the second edge, so shell and diameter arguments can freely flip orientation without leaving the geometric relation.
The module sits in the RS reading of Erdős #132 (distance shells as two-body recognition-energy shells). No downstream consumers are recorded yet (used_by is empty), so the lemma is local infrastructure for ordered-edge geometry rather than a named step in the T0–T8 forcing chain. It closes a small orientation gap so later sparse-shell or diameter-shell uniqueness arguments need not case-split on endpoint order.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.