DiameterEdgesFormConwayThrackle
plain-language theorem explainer
Defines the (false) claim that ordered diameter edges of a planar point set form a Conway thrackle whenever the distance is a diameter shell. Kept only as a legacy warning surface: ordered pairs double-count each undirected segment, so the thrackle condition fails. Cite the unordered-support variant instead. Pure Prop abbreviation; no proof content.
Claim. The proposition asserting: for every finite $A \subset \mathbb{R}^2$ and every $\Delta \in \mathbb{R}$, if $\Delta$ is a diameter shell of $A$, then the ordered diameter-edge finset of $(A,\Delta)$ is a Conway thrackle. (This ordered formulation is false; the correct statement uses unordered edge support.)
background
The module physicalizes Erdős problem #132: a distance value is a shell in the pairwise Euclidean spectrum, read as a two-body recognition-energy shell whose multiplicity is occupancy. Lean works with ordered pairs, so positive-distance ordered multiplicity is twice the classical unordered count (threshold $\le n$ becomes $\le 2n$).
Points are Point2 $= \mathbb{R}^2$ with the Euclidean metric. A diameter shell means $\Delta$ realizes the maximum pairwise distance on $A$. The ordered diameter-edge set filters ordered pairs at exact distance $\Delta$. A Conway thrackle requires that every pair of edges meets in exactly one point (endpoint or proper crossing), a classical bound ingredient for thrackle-type multiplicity estimates.
The sibling correct statement replaces the ordered thrackle predicate by its unordered-support form, because $(a,b)$ and $(b,a)$ are distinct ordered edges sharing one geometric segment.
proof idea
Not a proved theorem: a bare Prop abbreviation quantifying over finite point sets $A$ and reals $\Delta$, requiring that diameter-shell hypotheses imply the ordered thrackle predicate on the filtered ordered diameter edges. No tactics, no lemmas discharged. The body is intentionally the wrong (ordered) formulation retained as a warning surface pointing to the unordered-support replacement.
why it matters
Sits in the RS reading of Erdős #132 (distance-shell multiplicity as recognition-energy occupancy). It records a failed first attempt to phrase the diameter Conway condition on ordered representatives. Downstream work should ignore it: used_by is empty, and the module doc plus sibling doc redirect to the unordered-support Conway condition on diameter edges. No forcing-chain landmark (T0–T8), RCL, or constant identity depends on this Prop; it is local combinatorial scaffolding hygiene inside the distance-shell development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.