dist_convex_combination_le
plain-language theorem explainer
Any convex combination of two points inside a closed Euclidean ball about a stays inside that ball. Planar geometers working the diameter-shell side of Erdős #132 cite it when they need the segment between two Δ-bounded points to remain Δ-bounded from a. The proof is a short tactic application of closed-ball convexity, with membership rewritten through distance commutativity.
Claim. Let $a,c,d$ be points in the Euclidean plane $\mathbb{R}^2$ and let $\Delta\in\mathbb{R}$. For every $t\in[0,1]$, if $\mathrm{dist}(a,c)\le\Delta$ and $\mathrm{dist}(a,d)\le\Delta$, then $\mathrm{dist}\bigl(a,(1-t)\,c+t\,d\bigr)\le\Delta$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for bookkeeping, so positive-distance ordered multiplicity is twice the unordered count and classical thresholds double.
Points live in Point2, the Euclidean plane $\mathbb{R}^2$. The closed ball of radius $\Delta$ about $a$ is the set of points at distance at most $\Delta$ from $a$. Mathlib records that every closed ball in a real normed space is convex, so any convex combination of two members remains a member.
The local geometric setting is diameter shells: a distance value $\Delta$ that realizes the diameter of a finite planar set, with cross-distance bounds controlling which pairs can sit on that shell.
proof idea
Invoke convexity of the closed ball of radius $\Delta$ about $a$. Rewrite the two distance hypotheses as membership of $c$ and $d$ in that ball (using $\mathrm{dist}$-commutativity). The weights $1-t$ and $t$ are nonnegative and sum to 1 by elementary arithmetic. Convexity therefore places the combination $(1-t),c+t,d$ in the ball; rewriting membership back to a distance inequality finishes the proof.
why it matters
Immediate consumer is the segment-intersection lemma: if $c$ and $d$ lie on opposite strict sides of the line through $a,b$, and all four cross-distances from ${a,b}$ to ${c,d}$ are at most the diameter $\Delta=\mathrm{dist}(a,b)$, then the segments $[a,b]$ and $[c,d]$ meet. That lemma needs the present bound to keep intermediate points of $[c,d]$ inside the $\Delta$-ball about $a$ (and likewise about $b$).
In the broader module this is scaffolding geometry for sparse-shell and diameter-shell uniqueness statements that encode the RS reading of Erdős #132 (distance shells as recognition-energy shells). It is pure planar metric geometry; it does not itself invoke the forcing chain, RCL, or $\varphi$-ladder, but it underwrites the combinatorial control of shell multiplicities those physical claims rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.