onClosedSegment_iff_mem_segment
plain-language theorem explainer
The module's single-parameter closed-segment predicate on planar points is definitionally interchangeable with Mathlib's real convex segment. Diameter-shell and collinearity arguments in the Erdős #132 distance-multiplicity development cite this to unlock the convex-geometry API. The proof is a short bidirectional rewrite between the weight t and the pair of barycentric weights (1-t, t).
Claim. For planar points $a,b,x\in\mathbb{R}^2$, there exists $t\in[0,1]$ with $x=(1-t)\cdot a+t\cdot b$ if and only if $x$ lies in Mathlib's convex segment $\mathrm{segment}\,\mathbb{R}\,a\,b$ (i.e., $x=s\cdot a+t\cdot b$ for some $s,t\ge 0$ with $s+t=1$).
background
The module Distance Shell Multiplicity records the Recognition Science reading of Erdős problem #132: classical pairwise Euclidean distance values become two-body recognition-energy shells, and shell occupancy is multiplicity. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Points are Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. The local predicate OnClosedSegment a b x asserts existence of a real parameter $t$ with $0\le t\le 1$ and $x=(1-t)\cdot a+t\cdot b$: the closed affine segment between two visible planar states. Mathlib's segment $\mathbb{R}$ a b is the standard two-weight convex combination set. Equating the two forms is the bridge that imports Mathlib's segment library into the shell-multiplicity development.
proof idea
Bidirectional constructor on the two existential forms.
Forward: from $t\in[0,1]$ and $x=(1-t)a+tb$, exhibit barycentric weights $s:=1-t$ and $t$, check nonnegativity by linarith, the sum identity by ring, and rewrite the combination.
Reverse: from $s,t\ge 0$ with $s+t=1$ and $x=sa+tb$, take the single parameter to be $t$; the bound $t\le 1$ is linarith from $s\ge 0$; then $s=1-t$ by linarith and substitute into the combination.
why it matters
This is pure glue: it makes the module-local segment language identical to Mathlib's convex segment, so later diameter-shell and sparse-shell lemmas can quote Mathlib facts about membership, endpoints, and convex combinations without re-proving affine arithmetic.
Siblings such as IsDiameterShell, dist_le_of_diameter_shell, and the Erdős #132 ordered-multiplicity statements sit in the same file and need collinearity and segment language when arguing that a maximal distance is realized only on the boundary of the point set. No downstream theorem yet records a direct used_by edge, so the result is preparatory infrastructure inside the planar distance spectrum, not a forcing-chain step (T5–T8) or an RCL identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.