IsConwayThrackle
plain-language theorem explainer
Defines a Conway straight-line thrackle on an ordered finite edge set in the plane: every two distinct ordered edges meet simply (share exactly one point, either a common endpoint or a proper crossing). Cited by diameter-shell and four-point support bounds in the RS treatment of Erdős #132. The body is a direct universal quantification over pairwise simple meetings.
Claim. A finite set $E$ of ordered pairs of planar points is a Conway straight-line thrackle when every two distinct edges $e,f\in E$ meet simply: their closed segments share exactly one point (a shared endpoint or a proper crossing).
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 convenience; for positive distances, ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum. Edges are ordered pairs in a Finset. The predicate OrderedEdgesMeetSimply encodes that two ordered edges have closed segments intersecting in exactly one point. That is the right notion when $E$ may contain both orientations of the same undirected segment.
Classically, a (straight-line) thrackle is a drawing in which every pair of edges meets exactly once. Conway's thrackle conjecture bounds the number of edges by the number of vertices; the straight-line case is settled by Lovász–Pach–Szegedy / Cairns–Nikolayevsky counting.
proof idea
Pure definition: no proof obligations. The proposition is the universal statement that every pair of distinct members of $E$ satisfies OrderedEdgesMeetSimply. Downstream lemmas discharge or assume this predicate; they do not unfold a nontrivial construction here.
why it matters
This is the local thrackle hypothesis for the RS distance-shell program. Downstream it feeds ConwayThrackleSupportBound (unordered support size $\le |A|$), the endpoint-charge certificate (injective charging of undirected edges to vertices), and the exact four-point Conway support bound (K4 boundary: at most four unordered support edges when $|A|=4$ and no free incident vertex). The collinear residual isolates the remaining hand geometry when the algebraic dichotomy degenerates.
Diameter shells are intended to form thrackles on their undirected support; the ordered formulation DiameterEdgesFormConwayThrackle is kept only as a warning surface (both orientations share a segment). In the broader chain, thrackle control on diameter edges limits shell multiplicity and thereby constrains the Erdős #132 occupancy story in recognition units. No T0–T8 forcing step is proved here; the link is combinatorial scaffolding for shell bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.