LargeNonStarThrackleEndpointChargingCertificate
plain-language theorem explainer
Certificate proposition for the large non-star residual of straight-line thrackle endpoint charging: any thrackle edge set on at least three ambient points with no star center admits an injective charge from unordered edges into vertices. Downstream residual-closing lemmas reduce the full thrackle endpoint-charge theorem to this case after stars and two-point systems are handled. Pure Prop definition; the quantified statement is the content.
Claim. For every finite point set $A$ in the plane and every finite set $E$ of ordered pairs with both endpoints in $A$ and distinct, if no two members of $E$ are geometrically disjoint, $|A|\ge 3$, and $E$ is not a star (no vertex is incident to every edge), then there exists an injective map from the unordered edge support of $E$ into $A$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
A thrackle here is a finite ordered edge set in which no two edges are geometrically disjoint (they cross or share a vertex). Endpoint charging seeks an injection from the unordered support of $E$ into the ambient vertex set $A$, assigning each edge a distinct endpoint. Stars (all edges share a common vertex) and systems with $|A|\le 2$ are already closed elsewhere; the residual therefore begins at three ambient points and excludes stars.
The certificate is the weakest finite cardinal statement still needed on the thrackle side after those cases are removed.
proof idea
Definitional Prop, not a proved theorem. The body is the universal quantification over ambient point sets $A$ and ordered edge sets $E$, with hypotheses that edges stay inside $A$ with distinct ends, that no two edges are geometrically disjoint, that $|A|\ge 3$, and that $E$ is non-star, concluding existence of an injective charge from the unordered edge support into $A$. No tactics or lemmas are applied; downstream theorems discharge or consume this Prop.
why it matters
This is the residual interface that lets the thrackle endpoint-charge program finish after stars and tiny systems are closed. Three parents consume it: the support-bound implication produces the certificate from a cardinal support bound; the non-star residual closer upgrades it to the full non-star certificate by case-splitting on $|A|\le 2$; and the top thrackle residual closer composes those steps to obtain the complete straight-line thrackle endpoint-charge certificate.
In the RS reading of Erdős #132, thrackle control on distance shells feeds shell-multiplicity bounds. The certificate isolates the only remaining combinatorial obligation on the thrackle side, keeping the large non-star case cleanly separated from star geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.