isConwayThrackle_chosenOrderedSupport
plain-language theorem explainer
If an ordered edge set satisfies the Conway simple-meeting condition on its unordered support, then the finset of chosen ordered representatives is itself a Conway straight-line thrackle. Anyone transferring thrackle bounds from ordered edge systems to undirected diameter supports cites this. The proof unpacks image membership, recovers distinct support edges, and applies the ordered simple-meeting lemma to the representatives.
Claim. Let $E$ be a finite set of ordered pairs of planar points. If every pair of distinct undirected edges in the unordered support of $E$ admits ordered representatives in $E$ whose closed segments meet in exactly one point, then the chosen ordered-representative finset of $E$ is a Conway straight-line thrackle: every two distinct chosen ordered edges meet simply.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count for positive distances (so classical $\le n$ becomes $\le 2n$).
A Conway straight-line thrackle is an ordered edge system in which every two distinct edges share exactly one point (common endpoint or proper crossing). Diameter edge sets typically contain both orientations of each undirected edge, so they cannot be thrackles as ordered finsets. The support-level condition therefore asks only that distinct unordered support edges meet simply via some ordered representatives in $E$.
chosenOrderedSupport picks one ordered representative per unordered support edge. The present theorem says the support-level Conway hypothesis lifts to the ordinary ordered thrackle predicate on that chosen system.
proof idea
Classical reasoning. Fix two distinct members of the chosen ordered support; each is the image of a support edge under the representative map. Distinctness of the ordered edges forces the underlying unordered support edges to be distinct (else the representatives would coincide). Apply the support hypothesis to those two support edges to obtain ordered witnesses in $E$ that meet simply. The chosen representatives are unordered-equal to those witnesses, so the lemma that ordered edges with the same undirected geometry inherit simple meeting finishes the argument.
why it matters
This is the bridge from support-level geometry to the classical ordered thrackle theorem inside the distance-shell multiplicity development. Downstream, conway_support_bound_on_support_from_ordered chooses one representative per support edge, invokes the standard ordered Conway bound on that system, and transfers cardinality back to the undirected support. The module doc for that parent states the intent explicitly: the ordered theorem implies the support-level form used for diameter edge sets.
In the RS reading of Erdős #132, diameter shells are the extremal two-body recognition shells; the Conway counting bound (Lovász–Pach–Szegedy / Cairns–Nikolayevsky) controls how many such edges a planar point set can carry when every pair meets simply. Without the promotion step, the ordered thrackle theorem cannot be applied to bidirectional diameter edge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.