endpoint_charging_of_incident_vertex
plain-language theorem explainer
In a finite planar point set, any ordered edge system that is a star about a fixed vertex admits an injective endpoint charge from its unordered edge support into the vertex set. Thrackle and Erdős-distance arguments cite this as the star case of the endpoint-charging certificate. The proof embeds support edges as unordered pairs with the hub and applies the support-subset image injection lemma.
Claim. Let $A$ be a finite set of planar points and $E$ a finite set of ordered pairs with both endpoints in $A$ and no loops. If every edge of $E$ is incident to a fixed vertex $v$, then there exists an injective map from the unordered edge support of $E$ into $A$.
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 bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so classical bounds $\le n$ become $\le 2n$.
A directed edge set is a star about $v$ when every ordered edge has $v$ as one endpoint (OrderedEdgesIncidentTo). The thrackle endpoint-charging certificate asks, for every finite pairwise-intersecting straight-line edge system on $A$, for an injective charge from the unordered support of $E$ into $A$. Once that map exists geometrically, the support bound is pure finite cardinality.
The present theorem is the star case of that certificate: when all edges already share a common incident vertex, the charge can be built without residual geometric intersection hypotheses.
proof idea
Work classically. Define $f(x)={v,x}$ as an unordered pair. Using the star hypothesis, every unordered support edge arises as $f$ of the opposite endpoint of some ordered edge in $E$, and that opposite endpoint lies in $A$. Thus the unordered support is contained in the image $A.image,f$.
The conclusion is then the one-line application of the existing lemma that any support contained in such an image admits an injective endpoint charge into $A$. Case splits on left versus right incidence only rearrange which endpoint is the non-hub vertex; no geometric disjointness is used.
why it matters
This closes the star branch of the thrackle endpoint-charging certificate. Downstream, thrackle_endpoint_charging_from_nonstar_residual cases on whether a common incident vertex exists: if yes, it applies this theorem; if no, it invokes the non-star residual certificate. Together they yield the full endpoint-charging form of the straight-line thrackle theorem.
In the module's RS reading, thrackle-type support bounds control how many two-body recognition edges can share a distance shell without geometric separation, feeding the distance-shell multiplicity program tied to Erdős #132. The star case is the elementary base: a common hub already injects edges into vertices, so the hard geometry lives only in the non-star residual.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.