ordered_edges_meet_swap_left
plain-language theorem explainer
Swapping the two endpoints of the first ordered edge preserves geometric meeting with a second ordered edge in the plane. Anyone using ordered-pair thrackle or Hopf–Pannwitz predicates on planar distance shells cites this symmetry. The argument is a one-line existential reassembly via closed-segment endpoint symmetry.
Claim. Let $a,b\in\mathbb{R}^2$ and let $f$ be an ordered pair of points in $\mathbb{R}^2$. If the closed segments $[a,b]$ and $[f_1,f_2]$ intersect, then the closed segments $[b,a]$ and $[f_1,f_2]$ also intersect.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with multiplicity as shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Points live in the Euclidean plane: Point2 is $\mathbb{R}^2$. Two ordered edges meet geometrically when their closed straight-line segments share a point. Explicitly, there exists $x$ lying on both closed segments. The companion notion of 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.
Upstream, closed segments are symmetric in their endpoints: if $x$ lies on $[a,b]$, then $x$ lies on $[b,a]$. That fact is the only geometric input needed here.
proof idea
Unpack the geometric-meeting witness: some point $x$ lies on both closed segments. Apply the closed-segment endpoint-symmetry lemma to the first conjunct, replacing membership on $[a,b]$ by membership on $[b,a]$. Re-pack the same $x$ with the unchanged second-segment membership. The whole proof is that existential reassembly.
why it matters
Ordered edges are the native language of the distance-shell multiplicity development (Erdős #132 in RS units). Geometric meeting must be invariant under endpoint order, otherwise every thrackle-style count would double-count or miss crossings depending on arbitrary orientation. This lemma closes that orientation gap for the first edge.
No downstream consumers are wired yet in the graph, so the result is presently a local symmetry lemma inside the shell-multiplicity toolkit. It sits beside diameter-shell uniqueness, sparse-shell divergence, and the ordered Erdős-132 statement, all of which need orientation-insensitive intersection. In the broader RS picture it supports clean planar combinatorics for recognition-energy shells without forcing a choice of edge direction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.