left_endpoint_on_segment
plain-language theorem explainer
For any two points a,b in the plane, the left endpoint a lies on the closed segment [a,b]. Cited whenever geometric edge-meeting is reduced to an endpoint witness. The proof is a one-line existential: take parameter t=0 in the convex combination.
Claim. For all points $a,b\in\mathbb{R}^2$, one has $a\in[a,b]$, i.e. there exists $t\in[0,1]$ with $a=(1-t)a+tb$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count.
Point2 is the Euclidean plane $\mathbb{R}^2$. The predicate OnClosedSegment a b x asserts that $x$ is an affine convex combination of $a$ and $b$: $\exists t\in[0,1]$ with $x=(1-t)\cdot a+t\cdot b$. This is the closed geometric segment between two visible planar states.
The statement is the trivial endpoint membership that every later crossing or meeting lemma needs as a base case.
proof idea
Term-mode existential introduction. Instantiate the witness $t=0$; the two inequalities $0\le 0$ and $0\le 1$ are discharged by norm_num, and the vector identity $a=(1-0)\cdot a+0\cdot b$ is closed by simp.
why it matters
Base endpoint fact for the geometric meeting calculus of diameter shells. Downstream it is applied directly in ordered_edges_meet_of_fst_on_segment, its symmetric form, ordered_edges_meet_of_share_endpoint, segments_meet_of_orient2_zero, and shared_left_diameter_representatives_meet_simply. Those lemmas feed the four-point Hopf–Pannwitz crossing theorem (fourPointDiameterCrossing_thm), which forces closed diameter segments to meet when all cross-distances are at most the diameter. In the RS reading this is the combinatorial skeleton of shell-occupancy control for Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.