nonstar_thrackle_endpoint_charging_from_large_residual
plain-language theorem explainer
Any large non-star thrackle endpoint-charging certificate already yields the full non-star residual certificate: systems with at most two ambient points are automatically stars, so they never appear as non-star counterexamples. Combinatorialists working the straight-line thrackle endpoint-charge reduction, and anyone closing the RS physicalization of Erdős #132, would cite this. The proof is a two-branch card case split plus a contradiction from an incident vertex.
Claim. Assume every pairwise-intersecting straight-line edge system on a finite point set $A\subset\mathbb{R}^2$ with $|A|\ge 3$ and with no common incident vertex admits an injective endpoint-charging map from its unordered edge support into $A$. Then the same conclusion holds for every such system with no common incident vertex, with no lower bound on $|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 bookkeeping; for positive distances the ordered multiplicity is twice the unordered one, so classical thresholds double.
The non-star residual certificate asks: every finite point set $A$ and every edge set $E$ of ordered pairs inside $A$, with no two edges geometrically disjoint and with no vertex incident to every edge, admits an injective charge from the unordered edge support of $E$ into $A$. Star systems are already handled by a separate incident-vertex charging lemma, so this residual only targets pairwise-intersecting thrackles without a common vertex.
The large non-star certificate is the same statement restricted to $|A|\ge 3$. The doc-comment records the reason: every system with $|A|\le 2$ is automatically a star, so the residual only needs the large case.
proof idea
Fix ambient points $A$, edges $E$, the edge-support hypotheses, pairwise non-disjointness, and the non-star hypothesis (no common incident vertex). Case on $|A|\le 2$.
If $|A|\le 2$, apply exists_incident_vertex_of_card_le_two to produce a vertex incident to every edge of $E$, then eliminate against the non-star hypothesis.
If not, deduce $|A|\ge 3$ by omega and feed $A,E$ and all hypotheses into the large non-star certificate hypothesis. That supplies the required injective charging map.
why it matters
This is the middle step in the thrackle endpoint-charge reduction chain inside the distance-shell module. Downstream, thrackle_endpoint_charging_from_large_nonstar_residual composes it with the star residual: "Star systems and $|A|\le 2$ systems are closed. Therefore a large non-star endpoint-charge certificate is enough for the full straight-line thrackle endpoint-charge theorem."
In the RS reading, thrackle endpoint charging controls how recognition edges can share endpoints without geometric disjointness, which feeds shell-occupancy bounds for the Erdős #132 physicalization. The declaration itself is pure combinatorial bookkeeping: it removes the small-card cases from the non-star residual so that only the genuinely hard large non-star systems remain open for geometric argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.