dist_from_diff_eq_smul
plain-language theorem explainer
If two planar displacement vectors are scalar multiples componentwise, Euclidean distance scales by the absolute value of that scalar. The lemma packages collinear base-segment distance arithmetic for all endpoint orderings used in diameter-shell arguments. Anyone proving four-point collinear contradictions or closed-segment membership inside a lens cites it. The proof equates squared distances via the Euclidean sum-of-squares formula, then recovers the nonnegative square root.
Claim. Let $a,b,u,v$ be points in the Euclidean plane and let $t\in\mathbb{R}$. If $v_i-u_i=t(b_i-a_i)$ for both coordinates $i\in\{0,1\}$, then $d(u,v)=|t|\,d(a,b)$.
background
The ambient module physicalizes Erdős problem #132: classical pairwise distance values become two-body recognition-energy shells, and shell occupancy is multiplicity. Ordered pairs are used for Lean bookkeeping, so a classical multiplicity bound $\le n$ becomes $\le 2n$ for positive distances.
Points are Point2, the module's planar point type (an abbreviation of the bipartite distance-spectrum point type). Distance is the standard Euclidean metric on $\mathbb{R}^2$, with squared distance equal to the sum of squared coordinate differences.
The hypothesis is pure collinear scaling: the displacement $v-u$ equals $t$ times $b-a$ in each coordinate. The conclusion is the corresponding absolute scaling of lengths. Downstream geometry (diameter shells, lenses $D(a,\Delta)\cap D(b,\Delta)$) repeatedly needs this identity for every ordering of endpoints on a line.
proof idea
Flip the given coordinate identities to express $u_i-v_i$ as $-t(b_i-a_i)$. Expand both squared distances with the Euclidean sum-of-squares formula on Fin 2, substitute, and cancel the sign via $(u_i-v_i)^2=t^2(b_i-a_i)^2$ together with $(a_i-b_i)^2=(b_i-a_i)^2$. This yields $(d(u,v))^2=t^2(d(a,b))^2$. Rewrite the right-hand side as $(|t|,d(a,b))^2$ using $t^2=|t|^2$. Nonnegativity of both distances and of $|t|,d(a,b)$ lets absolute values drop after the square-equality criterion, giving $d(u,v)=|t|,d(a,b)$.
why it matters
Diameter-shell uniqueness and sparse-shell divergence in this module rest on controlling collinear four-point configurations at the maximal distance $\Delta$. The parent collinearDiameterEndpointContradiction uses the scaling to parametrize points on a common line and force endpoint coincidence from $|s-t|=1$ with parameters in $[0,1]$. Separately, onClosedSegment_of_orient2_zero_in_lens applies it when orientation vanishes and a third point sits in the closed lens of radius $\Delta=d(a,b)$, concluding closed-segment membership.
In the RS reading, each distance shell is a two-body recognition-energy level; multiplicity bounds are occupancy bounds. This elementary Euclidean identity is the coordinate engine that turns collinearity-plus-lens hypotheses into segment constraints, without invoking the heavier geometric-disjointness package. It does not itself touch the forcing chain (T0–T8) or the mass ladder; it is pure planar metric scaffolding for the Erdős #132 physicalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.