on_closed_segment_self_eq
plain-language theorem explainer
The degenerate closed segment from a planar point to itself contains only that point. Anyone using collinearity or segment predicates in planar distance-shell arguments would cite this. The proof unpacks the convex-combination witness and reduces the affine combination by the module tactic.
Claim. Let $a,x\in\mathbb{R}^2$. If $x$ lies on the closed line segment from $a$ to $a$ (i.e., $x=(1-t)a+ta$ for some $t\in[0,1]$), then $x=a$.
background
This module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count for positive distances.
Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. The predicate OnClosedSegment a b x asserts that $x$ is an affine combination $x=(1-t)\cdot a+t\cdot b$ for some real parameter $t$ with $0\le t\le 1$: the closed segment between two visible planar states.
The degenerate case $b=a$ is the zero-length segment. Upstream geometry (triangle edge data, ledger-closed plaquettes) sits in the broader RS stack; this lemma is pure planar affine algebra and needs none of that structure beyond the point type.
proof idea
Term/tactic hybrid. Destructure the existential witness of OnClosedSegment a a x to obtain $t\in[0,1]$ and the equality $x=(1-t)\cdot a+t\cdot a$. Rewrite the goal with that equality, then invoke the module tactic, which normalizes the affine combination over the real vector space to $a$. No external lemmas are required.
why it matters
Supports the local geometry of distance shells in the RS reading of Erdős #132: shell occupancy and diameter-shell uniqueness rely on clean segment predicates, including the degenerate case. The next comment in-file states triangle equality on a closed segment ($\mathrm{dist}(a,x)+\mathrm{dist}(x,b)=\mathrm{dist}(a,b)$ for interior $x$); the self-endpoint identity is the trivial base of that collinearity toolkit.
No downstream consumers are wired yet (used_by empty). It does not touch the forcing chain (T0–T8), RCL, or $\varphi$-ladder constants; it is scaffolding mathematics for planar recognition geometry rather than a physics landmark.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.