SupportEdgesHaveDisjointRepresentatives
plain-language theorem explainer
Two unordered support edges admit geometrically disjoint ordered representatives inside a finite ordered edge set. Anyone building thrackle or K4 obstruction certificates on planar point sets cites this predicate. It is a pure existential Prop packaging the unordered-to-ordered bridge used by the support-level four-point obstruction.
Claim. Given a finite set $E$ of ordered pairs of planar points and two unordered edges $u,v$, the predicate holds when there exist ordered pairs $e,f\in E$ whose underlying unordered edges are $u$ and $v$ respectively, and whose geometric segments are disjoint.
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 bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Here Point2 is the planar point type from the bipartite distance spectrum. Support edges are unordered pairs (Sym2 Point2) realized by ordered representatives in a finite edge set $E\subseteq\mathrm{Point2}\times\mathrm{Point2}$. Geometric disjointness of ordered edges is the sibling predicate that two segments share no interior geometry relevant to the thrackle obstruction.
The definition sits between finite-graph support bookkeeping (find two unordered candidates) and segment geometry (supply disjoint representatives).
proof idea
Definitional, not a proved theorem. The body is a single existential: witnesses $e,f\in E$ with matching unordered projections and OrderedEdgesGeometricallyDisjoint e f. No tactics or lemmas are applied; downstream results unpack the existential by rcases.
why it matters
This is the support-level interface for the exact four-vertex $K_4$ obstruction certificate. That certificate asks for two unordered support edges with geometrically disjoint representatives, the natural next geometric target after finite-graph bookkeeping finds the candidates.
It also feeds the one-line bridge theorem that a support-level disjoint pair immediately yields the ordered pair required by the thrackle obstruction. In the RS reading of Erdős #132, thrackle-type crossing constraints bound shell occupancy; this predicate is the unordered support face of that geometric constraint.
It does not itself close the Erdős bound; it only names the geometric hypothesis the obstruction certificates consume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.