exists_incident_vertex_of_card_le_two
plain-language theorem explainer
On an ambient set of at most two points, every ordered nonloop edge system is a star: some vertex meets every edge. Empty systems are stars about the origin; nonempty ones are stars about the first endpoint of any chosen edge. Cited when discharging the |A|≤2 boundary in Conway thrackle support and non-star residual charging for the Erdős #132 shell-multiplicity program. Proof is a short emptiness case-split plus a three-point cardinality contradiction.
Claim. Let $A$ be a finite planar point set with $|A|\le 2$, and let $E$ be a finite set of ordered pairs $(p,q)$ with $p,q\in A$ and $p\neq q$. Then there exists a point $v$ such that every edge of $E$ is incident to $v$ (i.e., $E$ is a star about $v$).
background
This module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum. An ordered edge system $E$ on ambient $A$ is required to be nonloop and supported in $A$: every $e\in E$ has both endpoints in $A$ and distinct. The predicate OrderedEdgesIncidentTo v E says $E$ is a star about $v$: every ordered edge has $v$ as one endpoint.
The lemma is the finite-combinatorial base case before thrackle and Conway support arguments: once $|A|\le 2$, geometry is irrelevant and every admissible $E$ is automatically a star.
proof idea
Classical case split on whether $E$ is nonempty.
If $E$ is nonempty, pick any edge $e_0$ and take $v:=e_0.1$. Suppose some $e\in E$ misses $v$. Using the support hypotheses on $e_0$ and $e$, a short case on whether $e.1=e_0.2$ produces three pairwise-distinct members of $A$. The helper card_ge_three_of_three_mem_distinct then yields $|A|\ge 3$, contradicting $|A|\le 2$ via omega.
If $E$ is empty, take $v:=0$. The star predicate is vacuous: any membership $e\in E$ is absurd.
why it matters
Closes the first non-star finite boundary: on $\le 2$ ambient points every admissible ordered system is a star, so residual non-star hypotheses can only live on larger sets.
Downstream, conway_support_bound_from_large_nonstar applies it under $|A|\le 2$ to reduce the full Conway thrackle support bound to the large non-star residual ("star systems plus all ambient sets of size at most three are closed"). Likewise nonstar_thrackle_endpoint_charging_from_large_residual uses it to show small systems are automatically stars, so closing large non-star systems closes the whole non-star residual.
In the RS reading of Erdős #132, this is pure discrete support control on recognition-energy shells: no appeal to the forcing chain (T5–T8), RCL, or $\varphi$-ladder constants is needed here; it is the combinatorial floor under thrackle charging and Conway support in the distance-shell multiplicity program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.