undirected_thrackle_support_of_conway_thrackle
plain-language theorem explainer
Assuming the Conway straight-line thrackle support bound, any finite planar edge system in which every pair of edges meets simply has undirected support size at most the number of vertices. Graph theorists working thrackle bounds and the Hopf–Pannwitz counting step would cite it. The proof is a one-line application of that assumed bound to a Conway thrackle edge system.
Claim. Assume the Conway straight-line thrackle support bound: if every pair of edges in a finite straight-line drawing meets simply, then the undirected edge support has size at most the number of ambient vertices. Let $A$ be a finite planar point set and $E$ a set of ordered pairs of distinct points of $A$. If $E$ is a Conway thrackle (every two distinct edges share exactly one point: a common endpoint or a proper crossing), then the cardinality of the undirected support of $E$ is at most $|A|$.
background
This module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean distance set; physically it is a two-body recognition-energy shell whose multiplicity is the shell occupancy. The development uses ordered pairs for Lean simplicity: for a positive distance, ordered multiplicity is twice the usual unordered multiplicity, so the classical threshold $\le n$ becomes $\le 2n$.
A Conway straight-line thrackle is an edge system in which every pair of distinct edges meets simply: they share exactly one point (shared endpoint or proper crossing). The Conway support bound states that any such thrackle on a finite vertex set $A$ has undirected support of size at most $|A|$. That bound is the Lovász–Pach–Szegedy / Cairns–Nikolayevsky counting theorem in this setting, and it is false without the simple-meeting condition (collinear overlapping edges give counterexamples).
The present statement simply specializes the bound to edge systems already known to be Conway thrackles.
proof idea
One-line term proof. Apply the Conway thrackle support bound hypothesis directly to the given vertex set, ordered edge set, edge-validity hypothesis (endpoints in $A$, non-loops), and the Conway thrackle hypothesis. The conclusion of the bound is exactly the desired undirected-support inequality; no intermediate rewriting is needed.
why it matters
In the distance-shell multiplicity development, thrackle-type bounds limit how many edges a geometric configuration can carry under simple-meeting constraints. The diameter-specific ordered thrackle bound documented next in the module uses four-point crossing geometry to guarantee the Conway condition and is described as the correct classical target for the Hopf–Pannwitz counting step; once Conway thracklehood is established, this lemma supplies the general undirected support form those arguments need.
Within Recognition Science the module links classical combinatorial geometry (Erdős #132) to recognition-energy shell occupancy. The result itself is pure discrete geometry and does not invoke the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder mass formula; it is combinatorial scaffolding for shell-multiplicity bounds.
No downstream consumers are recorded yet, so the lemma is presently a leaf available for diameter-shell and sparse-shell arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.