right_endpoint_on_segment
plain-language theorem explainer
The right endpoint of a closed planar segment always lies on that segment. Geometric lemmas on ordered edges and diameter crossings cite this as the trivial endpoint witness. The proof is a one-line term construction: take parameter t = 1 and simplify the convex combination.
Claim. For any two points $a,b$ in the Euclidean plane $\mathbb{R}^2$, the point $b$ lies on the closed line segment $[a,b]$. Equivalently, there exists $t\in[0,1]$ with $b=(1-t)a+tb$ (namely $t=1$).
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count.
Point2 is the Euclidean plane $\mathbb{R}^2$. The predicate OnClosedSegment a b x asserts that $x$ is a convex combination of $a$ and $b$: there 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 companion left-endpoint fact is the symmetric $t=0$ case.
proof idea
Term-mode construction of the existential witness. Instantiate the parameter at $t=1$. Two norm_num subgoals discharge $0\le 1$ and $1\le 1$. The remaining equality $b=(1-1)\cdot a+1\cdot b$ is closed by simp on the scalar arithmetic of the convex combination.
why it matters
Endpoint membership is the base case for geometric meeting of ordered edges. Downstream, ordered_edges_meet_of_snd_on_segment and its symmetric form apply this fact directly: if the second endpoint of one ordered edge lies on the other segment, the edges meet at that endpoint. Shared-endpoint meeting (ordered_edges_meet_of_share_endpoint) likewise uses left/right endpoint witnesses.
Those meeting lemmas feed the four-point Hopf–Pannwitz crossing theorem: if two diameter-length segments have all cross-distances at most the diameter and distinct endpoints, their closed segments meet. That crossing control is part of the ordered-shell multiplicity apparatus for the RS reading of Erdős #132 (sparse shells, diameter uniqueness, flux bridges). The result itself is pure planar geometry; its place in the chain is as the trivial right-endpoint witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.