ConwayThrackleEndpointChargeCertificate
plain-language theorem explainer
Constructive certificate for Conway's straight-line thrackle theorem: every finite thrackle admits an injective assignment of each unordered edge to one ambient vertex. Anyone closing the ordered support bound or the constructive residual for Erdős #132 cites this Prop. It is a universal statement over finite point and edge sets, not a proved theorem; the body is the Prop itself.
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 $E$ is a Conway straight-line thrackle, then there exists an injective map from the unordered edge support of $E$ into $A$.
background
The module physicalizes Erdős problem #132: a Euclidean distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances the ordered multiplicity is twice the unordered one, so classical bounds $\le n$ become $\le 2n$.
A Conway thrackle is a straight-line drawing in which every pair of edges meets exactly once (either at a shared endpoint or by proper crossing). The unordered edge support is the set of undirected edges underlying the ordered pair set $E$. An endpoint charge is a map sending each such undirected edge to a vertex of the ambient finite set $A$.
The certificate asserts that every finite thrackle admits an injective such charge. In finite cardinality this is equivalent to the classical Conway support bound $|E| \le |A|$, but it is the form suited to a future constructive formal proof.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over finite vertex sets $A$ and ordered edge sets $E$: whenever $E$ is a thrackle on $A$, there exists an injective charge from the unordered edge support into $A$. No tactics or lemmas are applied; the declaration packages the constructive target for later discharge.
why it matters
Feeds the one-line cardinality argument conway_support_bound_from_endpoint_charge, whose doc states that an injective endpoint charge proves the standard ordered Conway support bound by finite cardinality. Also appears as the first conjunct of Erdos132CurrentConstructiveResidual: a Conway endpoint-charge certificate plus convex-layer screening is the constructive residual that would prove Erdős #132.
In the RS reading, thrackle support bounds control how many ordered pairs can share a single distance shell, hence how large a shell multiplicity can be before geometric packing forces a new shell. Closing this certificate is the main open geometric step on the constructive path to the #132 residual in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.