thrackle_endpoint_charging_from_nonstar_residual
plain-language theorem explainer
Given a certificate that every pairwise-intersecting straight-line edge system with no common vertex admits an injective endpoint charge into the point set, the full thrackle endpoint-charging certificate follows. Anyone closing the straight-line thrackle bound via residual casework would cite this. The proof is a two-branch case split: star systems are charged by the incident-vertex lemma; the residual is handed to the hypothesis.
Claim. Assume every finite point set $A\subset\mathbb{R}^2$ and every finite ordered edge set $E$ on $A$ that is pairwise non-disjoint and has no common incident vertex admits an injective charge from the unordered support of $E$ into $A$. Then the same injective charge exists for every pairwise non-disjoint system, with or without a common vertex.
background
This 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 simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
The endpoint-charging form of the straight-line thrackle theorem asks, for every finite pairwise-intersecting straight-line edge system on a point set $A$, for an injective map from unordered support edges into $A$. Once that injection exists, the support bound is pure finite cardinality.
Star systems (those with a vertex incident to every edge) are already closed by a dedicated geometric lemma that charges each unordered edge at an incident endpoint. The non-star residual certificate therefore only needs to handle pairwise-intersecting systems with no common incident vertex. This declaration glues the two pieces.
proof idea
Term-mode case analysis on the existence of a common incident vertex.
Introduce the point set $A$, edge set $E$, the edge-support hypotheses, and pairwise geometric non-disjointness. Split on whether some $v\in\mathbb{R}^2$ is incident to every ordered edge of $E$.
If such a $v$ exists, apply the upstream star-charging lemma endpoint_charging_of_incident_vertex to obtain the injective charge directly from incidence.
If no such $v$ exists, the non-star residual hypothesis applies: feed it $A$, $E$, the edge and non-disjointness assumptions, and the proof that every candidate vertex fails incidence (by negating the star witness). The residual certificate returns the required injection.
why it matters
This is the glue step that turns a residual non-star certificate into the full straight-line thrackle endpoint-charging theorem. Downstream, thrackle_endpoint_charging_from_large_nonstar_residual further reduces the residual to a large-system certificate by closing the $|A|\le 2$ and star cases, quoting that "a large non-star endpoint-charge certificate is enough for the full straight-line thrackle endpoint-charge theorem."
In the Recognition Science reading of Erdős #132, thrackle-type support bounds control how many two-body recognition edges can share a distance shell without geometric disjointness. Endpoint charging is the combinatorial engine behind those multiplicity bounds. The declaration itself is pure discrete geometry; it does not invoke the forcing chain (T5–T8), RCL, or the phi-ladder, but it sits on the combinatorial spine that the module uses to physicalize shell occupancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.