IsConwayThrackleSupport
plain-language theorem explainer
Unordered-support Conway thrackle condition for a finset of ordered planar edges: every two distinct undirected edges in the support meet simply (closed segments share exactly one point). Diameter edge sets carry both orientations, so the classical ordered thrackle predicate is the wrong surface; this is the correct one. Cited by the diameter-shell thrackle claim, the support thrackle cardinality bound, and the promotion to ordered thrackle on a chosen representative. Pure definition of a Prop.
Claim. Let $E$ be a finite set of ordered pairs of points in the Euclidean plane $\mathbb{R}^2$. Write $\mathrm{supp}(E)$ for the unordered (undirected) edge support of $E$. Then $E$ is a Conway thrackle support when for all distinct $u,v\in\mathrm{supp}(E)$ there exist ordered representatives $e,f\in E$ of $u$ and $v$ whose closed segments meet in exactly one point.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with multiplicity as shell occupancy. Points live in the Euclidean plane (Point2). The development uses ordered pairs for Lean convenience; for a positive distance, ordered multiplicity is twice the unordered multiplicity, so classical thresholds scale by two.
A Conway thrackle (straight-line) requires every pair of distinct edges to meet exactly once, counting shared endpoints. When an ordered finset stores both orientations of each undirected edge, that ordered set cannot itself be a thrackle. The support-level meeting predicate therefore asks only that two undirected support edges admit ordered representatives in $E$ whose closed segments share exactly one point. That is the right formulation for bidirectional ordered edge data such as diameter edge sets.
proof idea
Definitional: the body is the Prop that every pair of distinct members of the unordered edge support of $E$ satisfies the support-level simple-meeting predicate. No tactics or lemmas; the meaning is entirely carried by that meeting predicate (existence of ordered representatives in $E$ whose closed segments meet in one point).
why it matters
This is the correct Conway surface for diameter edge sets in the Erdős #132 development. Downstream, the diameter-shell claim asserts that the ordered diameter edges of a planar set form a Conway thrackle support; the support thrackle bound then states that any such support has unordered cardinality at most the number of vertices. A third consumer promotes the support condition to the ordinary ordered Conway predicate on a chosen one-orientation representative finset. Together these close the geometric step that diameter shells behave like thrackles, feeding the multiplicity and sparsity analysis of distance shells in the RS reading of Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.