OrderedEdgesIncidentTo
plain-language theorem explainer
An ordered edge set on the plane is a star about a vertex v when every ordered pair has v as an endpoint. Discrete geometers and thrackle analysts cite it to split star versus non-star cases in support bounds. The body is a one-line universal quantification over the finite edge set.
Claim. For a point $v\in\mathbb{R}^2$ and a finite set $E$ of ordered pairs of points, the predicate holds precisely when every $e\in E$ satisfies $e_1=v$ or $e_2=v$ (i.e., $E$ is a directed star centered at $v$).
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count for positive distances (threshold $\le n$ becomes $\le 2n$). Points are planar Euclidean points (Point2 $\simeq \mathbb{R}^2$).
Edges are ordered pairs drawn from a finite ambient set. A star configuration means every ordered edge is incident to a fixed center. That dichotomy (star vs non-star) is the first case split in Conway thrackle and K4-obstruction arguments later in the file.
Upstream edge-set constructions (lattice-ball ordered adjacency, bipartite spectrum points) supply the ambient vocabulary; this predicate only classifies incidence geometry of a given finite ordered edge set.
proof idea
Pure definitional abbreviation: the proposition is the universal statement that every member of the finite ordered edge set has first or second component equal to the distinguished vertex. No lemmas or tactics.
why it matters
Star detection is the hinge for thrackle support certificates in this module. Downstream, endpoint_charging_of_incident_vertex builds an injective endpoint charge from a star hypothesis; conway_support_bound_from_large_nonstar closes the small-card and star cases before invoking the large non-star residual. Exact four- and five-point certificates (ExactFourPointK4ObstructionCertificate, Conway thrackle bounds, non-star thrackle bounds) explicitly quantify over the negation of this predicate to isolate non-star geometry, including the collinear Conway residual.
In the RS reading of Erdős #132, shell occupancy bounds must control thrackle-like edge systems; the star case is the elementary counting regime, so isolating it lets the harder geometric obstruction work concentrate on non-stars. No forcing-chain landmark (T5–T8) is invoked here; the link is combinatorial infrastructure for distance-shell multiplicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.