OrderedEdgesShareEndpoint
plain-language theorem explainer
Two ordered planar edges share an endpoint when any endpoint of one equals any endpoint of the other. Diameter-shell and Erdős-#132 multiplicity arguments cite this predicate to split shared-endpoint cases from endpoint-disjoint ones. It is a pure four-way disjunction on the four point components; no proof content.
Claim. For ordered edges $e=(p,q)$ and $f=(r,s)$ in $\mathbb{R}^2\times\mathbb{R}^2$, the edges share an endpoint when $p=r$ or $p=s$ or $q=r$ or $q=s$.
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 occupancy is the shell multiplicity. Ordered pairs are used for Lean simplicity, so for a positive distance the ordered multiplicity is twice the unordered one (classical threshold $\le n$ becomes $\le 2n$).
Points are planar: Point2 is the Euclidean plane $\mathbb{R}^2$. An ordered edge is simply a pair of such points. Downstream diameter lemmas treat diameter-shell representatives as ordered edges of maximal length $\Delta$ in a finite planar set $A$, and repeatedly case-split on whether two such edges share a vertex.
The predicate is purely combinatorial on the four endpoints. A nearby doc note records the geometric companion: shared endpoint implies the corresponding closed segments meet.
proof idea
Definitional, not a proved theorem. The body is the four-way disjunction comparing the two components of $e$ against the two components of $f$. No lemmas are applied; consumers typically by_cases on the predicate and handle the shared-endpoint branch by the elementary meeting fact for closed segments.
why it matters
This is the case-split hinge for the local diameter-meeting bridge in the RS reading of Erdős #132. Downstream, diameter_segments_meet_from_endpoint_disjoint_core combines endpoint-disjoint local meeting with the shared-endpoint branch to obtain full local meeting of diameter segments. Likewise distinct_diameter_representatives_meet_simply_from_cases merges shared-endpoint and endpoint-disjoint representative lemmas into the full ordered-representative certificate.
Several endpoint-disjoint certificates (EndpointDisjointDiameterRepresentativesMeetSimply, EndpointDisjointDiameterIntersectionUniqueCertificate, and the theorems that discharge them) take the negation of this predicate as a hypothesis, so uniqueness and simple-meeting statements only need to treat pairs that do not share a vertex. Without a crisp shared-endpoint test, the diameter-shell geometry would not factor cleanly into the two regimes the module proves separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.