thrackle_endpoint_charging_from_large_nonstar_residual
plain-language theorem explainer
A large non-star endpoint-charge certificate for pairwise-intersecting straight-line edge systems implies the full thrackle endpoint-charge certificate. Anyone reducing the straight-line thrackle support bound by residual case splits would cite this. Star systems and two-point systems are already closed, so only the large non-star residual remains. The proof is a two-step term composition of residual lifts.
Claim. Assume that every finite pairwise-intersecting straight-line edge system on a point set $A$ with $|A|\ge 3$ that is not a star admits an injective charge from its unordered edge support into $A$. Then every finite pairwise-intersecting straight-line edge system (with no size or star restriction) admits such an injective endpoint charge.
background
This module records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean distance set; physically it is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity: for positive distances, ordered multiplicity is twice the unordered count, so the classical threshold $\le n$ becomes $\le 2n$.
The full endpoint-charging certificate asks, for every finite point set $A$ and every edge set $E$ of ordered pairs inside $A$ that is pairwise non-disjoint in the straight-line sense, for an injective map from the unordered edge support of $E$ into $A$. Once that geometric charge exists, the support bound is pure finite cardinality.
The large non-star residual form is the same statement restricted to $|A|\ge 3$ and to systems that are not stars (no vertex incident to every edge). Systems with $|A|\le 2$ are already stars, so the residual only has to start at three ambient points.
proof idea
Pure term-mode composition of two residual lifts already in the module. First apply the large-to-nonstar residual lemma to the hypothesis, obtaining a non-star endpoint-charge certificate. Then feed that into the nonstar-to-full residual lemma, which closes the star and $|A|\le 2$ cases and yields the unrestricted thrackle endpoint-charge certificate. No new geometric construction appears here.
why it matters
This is the residual bridge that lets a large non-star certificate upgrade to the full straight-line thrackle endpoint-charge theorem. Its sole downstream consumer is the support-bound form: a cardinal support bound on large non-star systems is enough for the full endpoint-charging certificate, obtained by first turning the support bound into a large non-star charge certificate and then applying this theorem.
In the module's Erdős #132 reading, endpoint charging is the combinatorial engine behind shell-occupancy control for pairwise-intersecting straight-line systems. The declaration does not itself touch the forcing chain (T5--T8) or the Recognition Composition Law; it sits in the pure geometric layer that later feeds distance-shell multiplicity bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.