midpoint_on_closed_segment
plain-language theorem explainer
The midpoint of two planar points lies on the closed segment joining them. Elementary convex-geometry fact used inside the distance-shell multiplicity development (Erdős #132 physicalization). Proof is a direct existential witness: parameter t = 1/2, with the two inequalities by norm_num and the vector identity by the module tactic.
Claim. For any $a,b\in\mathbb{R}^2$, the midpoint $\tfrac12 a+\tfrac12 b$ lies on the closed segment $[a,b]$: there exists $t\in[0,1]$ such that $\tfrac12 a+\tfrac12 b=(1-t)\,a+t\,b$.
background
The module DistanceShellMultiplicity records the Recognition Science reading of Erdős problem #132: classical pairwise Euclidean distance values become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Point2 is the Euclidean plane $\mathbb{R}^2$ (alias of EuclideanSpace ℝ (Fin 2) from BipartiteDistanceSpectrum). The predicate OnClosedSegment a b x means $x$ is an affine combination $(1-t)a+tb$ for some real $t$ with $0\le t\le 1$: the closed line segment between two visible planar states.
This lemma is pure planar geometry infrastructure sitting under diameter-shell and sparse-shell arguments later in the same file.
proof idea
Term-mode existential construction. refine supplies the witness $t=1/2$ and three goals: $0\le 1/2$, $1/2\le 1$, and the vector equality. The two scalar inequalities close by norm_num. The remaining identity
$\tfrac12 a+\tfrac12 b=(1-\tfrac12)a+(\tfrac12)b$
is pure module arithmetic over the real scalar action and is discharged by the module tactic.
why it matters
Earns its place as a one-line geometric primitive for the RS physicalization of Erdős #132. Closed-segment membership is the language in which diameter shells, sparse shells, and ordered distance spectra are later constrained; the next sibling notes that a closed segment is convex under affine combinations, of which the midpoint is the symmetric special case.
No downstream consumers are recorded yet (used_by empty), so the lemma is local scaffolding rather than a cited bridge into the forcing chain (T0–T8), RCL, or the mass ladder. It does not touch $\varphi$, eight-tick structure, or $D=3$; it only keeps planar convex geometry available inside the shell-multiplicity development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.