ordered_edges_meet_symm
plain-language theorem explainer
Geometric meeting of two ordered planar edges is symmetric: if the closed segments of e and f intersect, then those of f and e intersect. Anyone using the thrackle-style meeting predicate in the ordered distance-shell setup cites this. The proof is a one-line existential witness swap.
Claim. Let $e,f$ be ordered pairs of points in the plane. If there exists a point $x$ lying on both closed segments determined by $e$ and by $f$, then the same holds with $e$ and $f$ interchanged.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is 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$.
Point2 is the planar point type from the bipartite distance spectrum. Two ordered edges meet geometrically when their closed straight-line segments share a point: $\exists x$ on both closed segments. The companion notion is geometric disjointness (no intersection), which is the correct Hopf–Pannwitz / thrackle predicate; mere endpoint-disjointness is too strong and would exclude crossing diameter diagonals.
proof idea
Term-mode proof. Unpack the hypothesis as an existential witness $x$ together with the two closed-segment memberships. Rebuild the same existential with the two memberships swapped. No auxiliary lemmas are required.
why it matters
Symmetry of the geometric meeting predicate is bookkeeping needed wherever ordered edges appear in the distance-shell multiplicity development (diameter shells, sparse shells, thrackle-type constraints). The module frames this as the RS reading of Erdős #132: shells are recognition-energy levels and multiplicity is occupancy. No downstream consumers are wired yet in the graph, so the lemma sits as local infrastructure for ordered-edge arguments rather than a named step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.