ConwayThrackleSupportBound
plain-language theorem explainer
The Conway straight-line thrackle support bound states that any finite straight-line thrackle on a point set A has at most |A| undirected edges when every pair of edges meets simply. Discrete geometers and anyone closing the Erdős #132 residual cite this interface. It is a pure Prop packaging the classical Lovász–Pach–Szegedy / Cairns–Nikolayevsky counting statement, ready for later discharge by endpoint charge or residual reduction.
Claim. For every finite point set $A \subset \mathbb{R}^2$ and every finite set $E$ of ordered pairs of distinct points of $A$, if $E$ is a Conway thrackle (every two edges meet simply), then the cardinality of the undirected edge support of $E$ is at most $|A|$.
background
This module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean bookkeeping; for a positive distance, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
A Conway thrackle is a straight-line drawing in which every pair of edges meets simply (proper crossing or shared endpoint, no collinear overlaps). The undirected support of an ordered edge set $E$ is the set of unordered pairs obtained by forgetting orientation. The classical counting theorem of Lovász–Pach–Szegedy and Cairns–Nikolayevsky asserts that such a thrackle on vertex set $A$ has at most $|A|$ undirected edges.
The bound is false if the simple-meeting hypothesis is dropped: collinear overlapping segments give counterexamples. The definition therefore hard-wires both the incidence condition (endpoints in $A$, distinct) and the thrackle predicate.
proof idea
Pure definitional packaging: the declaration is a Prop equal to a universal quantifier over finite point sets $A$ and ordered edge sets $E$, with the incidence hypothesis, the Conway thrackle hypothesis, and the cardinality inequality as conclusion. There is no tactic or term proof beyond the Prop body itself.
Downstream discharge routes construct an injective map from unordered support edges to ambient vertices (endpoint charge), or reduce via a large-nonstar residual plus small-cardinality case analysis, then invoke finite-cardinality injectivity.
why it matters
This Prop is the standard ordered Conway input to the live Erdős #132 assembly. It appears directly in Erdos132CurrentLiveResidual (paired with the convex-layer screening bridge) and is the hypothesis of the final assembly theorems that derive the ordered Erdős #132 statement from Conway counting plus screening.
Wrappers convert it to the support-level form by choosing one ordered representative per undirected edge, and recover it from an endpoint-charge certificate or from a large-nonstar residual. In the Recognition Science reading, thrackle sparsity limits how many equal-length two-body shells can sit on a finite point set, which is exactly the combinatorial content of the #132 multiplicity bound.
The constructive comment on the page flags the intended future proof target: an injective charge of each unordered edge to one ambient vertex, equivalent in finite cardinality but better shaped for formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.