ThrackleEndpointChargingCertificate
plain-language theorem explainer
Defines the endpoint-charging form of the straight-line thrackle theorem as a proposition: every finite pairwise-intersecting straight-line edge system admits an injective charge from its unordered edge support into the vertex set. Combinatorial geometers and anyone closing the thrackle input to Erdős #132 shell bounds would cite it. The body is a pure Prop packaging of that existence statement; no proof work lives here.
Claim. The endpoint-charging thrackle certificate asserts: for every finite point set $A\subset\mathbb{R}^2$ and every finite set $E$ of ordered pairs with both endpoints in $A$ and distinct, if no two members of $E$ are geometrically disjoint as straight segments, then there exists an injective map from the unordered edge support of $E$ into $A$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so classical unordered multiplicity $m$ becomes ordered multiplicity $2m$, and the classical bound $\le n$ becomes $\le 2n$.
A thrackle (here, straight-line) is a finite edge system in which every pair of edges meets. Conway's thrackle conjecture bounds the number of edges by the number of vertices. The endpoint-charging reformulation asks for an injective assignment of each unordered support edge to a vertex of $A$. Once that injection exists, finite cardinality alone yields the support bound $|\mathrm{support}(E)|\le|A|$.
Sibling notions in the module include ordered distance spectra, shell multiplicities, sparse shells, and diameter shells. The geometric disjointness predicate on ordered edges is the negation of the thrackle intersection hypothesis.
proof idea
Definitional packaging only: the declaration is a Prop abbreviation whose body is the universal quantification over finite point sets $A$ and ordered edge sets $E$, the two edge-wellformedness and pairwise-non-disjointness hypotheses, and the existential claim of an injective charge from the subtype of unordered support edges into the subtype of points of $A$. No tactics or lemmas fire here; downstream theorems construct or consume the certificate.
why it matters
This certificate is the common target of the residual-closure ladder in the module. Star systems and tiny ambient sets are closed separately; the remaining geometric work is concentrated in large non-star (or four-point non-star) support bounds, which are lifted through thrackle_endpoint_charging_from_large_nonstar_support_bound, thrackle_endpoint_charging_from_fourpoint_nonstar_support_bound, thrackle_endpoint_charging_from_large_nonstar_residual, and thrackle_endpoint_charging_from_nonstar_residual into the full certificate.
Once obtained, pointwise_thrackle_support_from_endpoint_charging converts it by finite cardinality into the pointwise undirected thrackle support bound, isolating "the remaining geometric content of the classical thrackle input." That bound feeds Conway-style support theorems such as conway_support_bound_from_large_nonstar, which in turn constrain distance-shell multiplicities for the RS reading of Erdős #132. The declaration therefore sits at the interface between classical thrackle geometry and the shell-occupancy estimates the module needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.