NonStarThrackleEndpointChargingCertificate
plain-language theorem explainer
Defines the residual certificate for straight-line thrackle endpoint charging on non-star systems: every pairwise-intersecting edge set on a finite point set in the plane, with no common incident vertex, admits an injective charge from unordered edges into ambient points. Anyone closing the thrackle endpoint-charge form after handling stars cites this Prop. It is a pure definition of a universal statement, not a proved theorem.
Claim. For every finite point set $A \subset \mathbb{R}^2$ and every finite set $E$ of ordered pairs from $A$ with distinct endpoints, if no two edges of $E$ are geometrically disjoint and no vertex is incident to every edge of $E$, 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, and shell multiplicity is occupancy. Ordered pairs are used for Lean convenience; for positive distances, ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
A thrackle (here, straight-line) is a drawing in which every pair of edges meets. Endpoint charging assigns each edge an endpoint injectively, which immediately bounds $|E|$ by $|A|$. Star systems (all edges share a common vertex) are already charged by the incident-vertex rule. The residual asked here is exactly the complementary case: pairwise intersecting edge sets with no common incident vertex.
Sibling notions in the module include ordered distance spectra, sparse shells, and diameter shells; the thrackle certificate sits downstream of those combinatorial primitives as a charging device for edge counts.
proof idea
No proof: the declaration is a bare Prop definition. It packages three hypotheses (edges live in $A$ with distinct ends; no geometrically disjoint pair; no universal incident vertex) and asserts existence of an injective charge from the unordered edge support into $A$. Downstream theorems discharge or reduce this Prop; the definition itself only names the residual obligation.
why it matters
This residual is the non-star half of the straight-line thrackle endpoint-charge problem inside the Distance Shell Multiplicity development of Erdős #132. Downstream, thrackle_endpoint_charging_from_nonstar_residual combines it with star closure to obtain the full endpoint-charging certificate. Separately, nonstar_thrackle_endpoint_charging_from_large_residual reduces the residual further to large ambient sets, since $|A|\le 2$ forces a star.
In the Recognition Science reading, bounding shell occupancy via thrackle-style charging constrains two-body recognition-energy multiplicities on the plane. The certificate is the precise interface between the combinatorial thrackle statement and the module's shell-multiplicity bounds; closing it (or its large-residual form) is what turns the residual into a usable edge bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.