ConwayThrackleSupportBoundOnSupport
plain-language theorem explainer
Support-level Conway thrackle bound: any finite point set A and any ordered edge set E on A that forms a Conway thrackle support has at most |A| unordered support edges. This is the interface used by the Erdős #132 residual packs in the distance-shell module. It is a Prop definition, not a proved theorem; the ordered thrackle theorem discharges it by choosing one orientation per undirected edge.
Claim. The following proposition: for every finite set $A$ of points in the plane and every finite set $E$ of ordered pairs from $A$ with distinct endpoints, if $E$ is a Conway thrackle support, then the number of unordered edges in the support of $E$ is at most $|A|$.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and shell multiplicity is occupancy. Lean works with ordered pairs; 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 thrackle: every pair of edges meets, either at a shared endpoint or in a proper crossing. The support-level form is the right surface when the ordered finset may contain both orientations of an undirected edge. The unordered edge support collapses opposite orientations to one undirected edge before counting.
Sibling notions in the module include diameter shells, sparse shells, and ordered distance spectra. The bound is stated only for edges whose endpoints lie in $A$ and are distinct.
proof idea
No proof body: this is a bare Prop definition packaging the universal statement over point sets $A$ and ordered edge sets $E$. The mathematical content is the inequality $|\mathrm{unorderedEdgeSupport}(E)| \le |A|$ under the thrackle-support hypothesis and the endpoint-in-$A$ side condition.
Discharge is external. The companion theorem conway_support_bound_on_support_from_ordered assumes the standard ordered Conway thrackle bound, picks one ordered representative per unordered support edge, applies that bound to the chosen system, and transfers the cardinality back to the unordered support.
why it matters
This Prop is the Conway-counting half of every live residual package for Erdős #132 in the module. Downstream structures Erdos132ConwayCountingScreeningResidualPack, Erdos132ConwayEndpointDisjointCollinearityScreeningResidualPack, and Erdos132ConwayEndpointDisjointUniquenessScreeningResidualPack each require it as a field, paired with deep-layer screening (and sometimes endpoint-disjoint uniqueness or collinearity).
The assembly theorems erdos132_from_support_conway_and_deep_screening_live and its endpoint-disjoint variants take this bound as a hypothesis and conclude the ordered form of Erdős #132. The diameter-side bridge diameter_conway_bound_from_support_conway specializes it under a diameter-support thrackle condition.
In the RS reading, bounding shell occupancy by the number of points is the combinatorial control on two-body recognition-energy shells that the #132 physicalization needs. It does not itself invoke the forcing chain (T5–T8) or the mass ladder; it is pure plane combinatorial geometry feeding the distance-shell argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.