SupportEdgesMeetSimply
plain-language theorem explainer
Support-level simple meeting: two unordered edges u and v meet simply relative to an ordered edge set E when some ordered representatives in E have closed segments sharing exactly one point. Diameter-support thrackle arguments cite this, because ordered diameter sets carry both orientations. The body is a pure existential unpacking of ordered simple meeting via unorderedEdgeOfOrdered.
Claim. Let $E$ be a finite set of ordered pairs of points in the Euclidean plane, and let $u,v$ be unordered edges (elements of $\mathrm{Sym}_2$ of the plane). The support edges $u$ and $v$ meet simply relative to $E$ if there exist $e,f\in E$ whose unordered classes are $u$ and $v$ respectively, and whose closed segments share exactly one point.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean convenience; for positive distances, ordered multiplicity is twice the classical unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Point2 is the Euclidean plane $\mathbb{R}^2$. An ordered edge is a pair of points; unorderedEdgeOfOrdered forgets orientation into a Sym2 class. Upstream, OrderedEdgesMeetSimply e f asserts unique intersection of the two closed segments: $\exists! x$ lying on both. That is the geometric condition in the Conway straight-line thrackle theorem, which excludes overlapping collinear segments that would inflate pairwise meeting counts past $|A|$.
Support-level meeting is the right lift when $E$ contains both orientations of the same undirected edge, as diameter ordered edge sets do.
proof idea
Definition, not a proved theorem. The proposition is the existential: witnesses $e,f\in E$ with unorderedEdgeOfOrdered e = u, unorderedEdgeOfOrdered f = v, and OrderedEdgesMeetSimply e f. No tactics or lemmas are applied in the body; downstream one-liners such as support_edges_meet_simply_of_ordered_representatives simply package those witnesses.
why it matters
This is the geometric atom of the support-level Conway condition. IsConwayThrackleSupport E requires that every pair of distinct unordered support edges of $E$ satisfy this predicate; the doc notes that diameter ordered edges cannot be an ordered thrackle because both orientations are present. DiameterSupportSimpleRepresentativeCertificate restates the same condition on the unordered support of diameter edges after orientation duplicates are removed.
In the RS reading of Erdős #132, diameter shells are the extremal two-body recognition shells; thrackle-type meeting controls how many such edges a planar point set can carry. The definition therefore sits between ordered segment geometry and the shell-multiplicity bounds the module targets. It does not itself invoke the forcing chain (T5–T8), but it is part of the planar combinatorial layer those physical claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.