PointwiseUndirectedThrackleSupportBound
plain-language theorem explainer
The pointwise undirected straight-line thrackle support bound: any finite system of pairwise geometrically intersecting straight edges on a point set A has at most |A| unordered edges. Combinatorial geometers and anyone reducing Erdős #132 cite it as the sharp classical thrackle input. It is a bare Prop definition packaging that universal statement for later certificates and reductions.
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 no two members of $E$ are geometrically disjoint as straight-line segments, then the number of distinct unordered edges supporting $E$ is at most $|A|$.
background
The module physicalizes Erdős problem #132: a Euclidean distance value is a two-body recognition-energy shell, and shell multiplicity is occupancy. Ordered pairs are used for Lean convenience; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds double.
A thrackle (straight-line) is a finite edge system in which every pair of edges meets geometrically. The classical Conway thrackle conjecture / theorem in the straight-line case asserts that the number of edges is at most the number of vertices. The present definition records that claim pointwise, not merely eventually in $n$.
Unordered edge support collapses each ordered pair and its reverse to one undirected edge, so the cardinality comparison is against $|A|$ rather than $2|A|$. Endpoint-charging is the companion certificate form: an injective map from those unordered edges into the vertex set.
proof idea
No proof: this is a definition of a proposition. The body is the universal quantifier over finite point sets $A$ and ordered edge sets $E$, the incidence and distinctness hypotheses on endpoints, the thrackle hypothesis that no two ordered edges are geometrically disjoint, and the conclusion that the cardinality of the unordered edge support is at most $|A|$. Downstream lemmas treat this Prop as a hypothesis or goal and discharge it via endpoint-charging plus finite injectivity.
why it matters
This is the sharp classical thrackle input that the Erdős #132 reduction needs. Downstream, pointwise_thrackle_support_from_endpoint_charging shows any endpoint-charging certificate implies the bound by finite cardinality, isolating the remaining geometric work. The converse packages any cardinal proof as an explicit charge, so the two forms are equivalent on finite systems. undirected_thrackle_support_from_pointwise lifts the pointwise statement to the eventual form used by the #132 reduction.
In the RS reading, distance shells are recognition-energy shells; thrackle-type intersection control limits how many equal-distance pairs can sit on a finite vertex set. The definition itself does not invoke the forcing chain (T5–T8) or the RCL; it supplies the combinatorial ceiling those physicalizations quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.