dist_add_on_closed_segment
plain-language theorem explainer
On a closed Euclidean segment in the plane, distances add: for any point x between a and b one has d(a,x)+d(x,b)=d(a,b). Shell-multiplicity arguments cite this as the exact triangle equality that forces endpoint domination and uniqueness. The proof unpacks the convex parameter t, rewrites distances as norms, and cancels via scalar-norm identities and ring.
Claim. Let $a,b,x\in\mathbb{R}^2$. If $x$ lies on the closed segment $[a,b]$, i.e. $x=(1-t)a+tb$ for some $t\in[0,1]$, then $d(a,x)+d(x,b)=d(a,b)$.
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. Points are planar Euclidean states (Point2 is $\mathbb{R}^2$).
A point $x$ lies on the closed segment between visible states $a$ and $b$ when it is a convex combination $x=(1-t)a+tb$ for some real $t\in[0,1]$. Distances are the ambient Euclidean metric (equivalently the norm of the difference vector).
This is the equality case of the triangle inequality along a line segment. Downstream lemmas use it to bound endpoint distances by the full segment length and to recover endpoints from distance equality.
proof idea
Unpack the segment witness to a parameter $t\in[0,1]$ with $x=(1-t)a+tb$. Rewrite all three distances as norms. Two short module identities give $a-x=t\cdot(a-b)$ and $x-b=(1-t)\cdot(a-b)$. Apply norm_smul twice, replace real norms by absolute values, drop the absolutes using $t\ge 0$ and $1-t\ge 0$, then finish by ring: $t|a-b|+(1-t)|a-b|=|a-b|$.
why it matters
Exact additivity on segments is the algebraic engine for the diameter-shell and sparse-shell apparatus in this module. It feeds four immediate corollaries: each endpoint distance is at most the segment length, and equality of either endpoint distance with the full length forces the point to be that endpoint.
Those uniqueness and domination facts underwrite diameter-shell uniqueness and the ordered-multiplicity bounds that translate Erdős #132 into RS language (distance shells as recognition-energy shells). The result is pure planar Euclidean geometry; it does not itself invoke the forcing chain or $\varphi$, but it is infrastructure for the combinatorial shell-counting that the module records as the RS reading of the classical problem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.