UndirectedThrackleSupportBound
plain-language theorem explainer
The undirected thrackle support bound states that, for all large enough finite planar point sets A, any ordered straight-line edge system on A with no geometrically disjoint pair has undirected support of size at most |A|. Discrete geometers and anyone wiring the RS assembly of Erdős #132 cite it as a counting hypothesis. It is a Prop definition (Hopf–Pannwitz/Perles form), not a proved theorem; the body is an eventual-for-all-n universal statement.
Claim. Eventually for all $n$, every finite $A\subset\mathbb{R}^2$ with $|A|=n$, and every set $E$ of ordered pairs of distinct points of $A$: if no two members of $E$ have geometrically disjoint closed segments, then the number of distinct undirected edges underlying $E$ is at most $|A|$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
Two ordered edges meet geometrically when their closed straight-line segments intersect; they are geometrically disjoint when the segments miss. That meeting predicate is the Hopf–Pannwitz / thrackle condition used here (endpoint-disjointness alone would wrongly exclude crossing diameter diagonals).
A sibling Prop, the Conway thrackle support bound, strengthens the hypothesis to simple meetings and is the correct Lovász–Pach–Szegedy / Cairns–Nikolayevsky counting theorem. The present bound uses only set-theoretic non-disjointness and therefore allows overlapping collinear segments.
proof idea
No proof: the declaration is a bare Prop definition. Its body is the filter statement "eventually for all $n$ at infinity," ranging over finite point sets $A$ of cardinality $n$ and ordered edge systems $E$ supported on distinct pairs from $A$. The geometric hypothesis is that every pair of edges fails geometric disjointness (equivalently, every pair meets). The conclusion is that the cardinality of the undirected edge support of $E$ is at most $|A|$. Downstream assemblies treat the whole Prop as a named hypothesis to be discharged or replaced.
why it matters
This Prop is the counting input in a family of legacy Erdős #132 assembly theorems in the same module: endpoint-disjoint diameter core, four-point diameter crossing, local diameter meeting, separation thrackle, and convex-layer screening variants all take it as hSupport and conclude the ordered form of Erdős #132.
Doc-comments on those parents mark it as deprecated relative to the Conway thrackle support bound: the set-theoretic meeting predicate permits collinear overlaps, for which the bound is false. The caveat is harmless on the diameter-segment route used for #132, because distinct diameter segments never overlap (discharged by the collinear separated-diameter contradiction). In the RS ledger this sits in the mathematics layer that turns geometric thrackle counting into a shell-multiplicity ceiling, feeding the physical reading of distance shells as recognition-energy occupancies.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.