undirected_thrackle_support_from_pointwise
plain-language theorem explainer
The pointwise undirected straight-line thrackle support bound implies the eventual (large-$n$) form used in the Erdős #132 reduction. Anyone wiring the thrackle bridge into distance-shell multiplicity cites this implication. The argument is a one-line `filter_upwards` that drops the universal quantifier over all finite sets down to large cardinalities.
Claim. Assume that for every finite point set $A\subset\mathbb{R}^2$ and every ordered edge set $E$ with endpoints in $A$, distinct endpoints, and no geometrically disjoint pair, the unordered support of $E$ has cardinality at most $|A|$. Then the same bound holds eventually: for all sufficiently large $n$, every $n$-point set $A$ and every such edge system $E$ satisfies $|\mathrm{unorderedSupport}(E)|\le|A|$.
background
This module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so classical unordered multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
The undirected thrackle support bound is the Perles/Hopf–Pannwitz geometric theorem in clean undirected form: if an ordered edge set has no geometrically disjoint pairs, its unordered support has at most $|A|$ edges. The pointwise version quantifies over every finite $A$ and $E$ at once; the eventual version only asks the bound for all large enough $|A|=n$ (filter atTop). The classical thrackle theorem is not asymptotic, so the pointwise form is the sharper statement that should eventually be proved or imported.
Caveat recorded on the eventual predicate: the meeting predicate allows overlapping segments, and the bound as stated fails for collinear point sets; the thrackle bridge uses the non-collinear regimes relevant to the shell argument.
proof idea
Pure filter transport. From the pointwise hypothesis $h$, apply filter_upwards on atTop to obtain a large-$n$ witness. For each such $n$, take any $A$ with $|A|=n$ and any ordered edge set $E$ whose endpoints lie in $A$, are distinct, and form no geometrically disjoint pair. The conclusion is exactly $h$ applied to that same $A$ and $E$; the cardinality hypothesis on $A$ is unused. No geometric lemma is invoked.
why it matters
Sits in the thrackle bridge that feeds the RS reading of Erdős #132 (distance-shell multiplicity as two-body recognition-energy occupancy). The doc-comment states the role directly: the pointwise straight-line thrackle support theorem implies the eventual form used by the Erdős #132 reduction. Downstream shell-flux and sparse-shell siblings in this module expect the eventual bound; this lemma is the named conversion step from the sharper classical statement to that asymptotic interface.
No current used_by edges are recorded, so the declaration is presently a proved interface hinge rather than a hot dependency. It closes the gap between the geometric thrackle literature (pointwise) and the filter-style hypotheses preferred by the ordered-spectrum and sparse-shell development. Framework landmarks T0–T8 are not directly cited here; the link is combinatorial geometry inside the distance-shell physicalization, not the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.