on_closed_segment_convex
plain-language theorem explainer
Closed segments in the plane are convex: any affine combination of two points on [a,b] stays on [a,b]. Distance-shell and planar-geometry arguments in the Erdős #132 physicalization cite this when mixing points along a diameter or chord. The proof unpacks barycentric parameters, forms the convex combination of those scalars, and closes with nlinarith plus the module tactic.
Claim. Let $a,b,x,y\in\mathbb{R}^2$. Suppose $x$ and $y$ lie on the closed segment $[a,b]$, and let $s\in[0,1]$. Then the affine combination $(1-s)x+sy$ also lies on $[a,b]$.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132: classical distance values become two-body recognition-energy shells, and shell occupancy is multiplicity (ordered pairs double the usual count, so the classical threshold $\le n$ becomes $\le 2n$).
Point2 is the Euclidean plane $\mathbb{R}^2$. A point $x$ lies on the closed segment between visible planar states $a$ and $b$ when there exists $t\in[0,1]$ with $x=(1-t)\cdot a+t\cdot b$. That is the standard barycentric parametrization of $[a,b]$.
The local setting is elementary convex geometry in the plane, used later for diameter shells and sparse-shell flux bridges rather than for the J-cost or phi-ladder themselves.
proof idea
Unpack the two OnClosedSegment hypotheses to barycentric witnesses $t_1,t_2\in[0,1]$ with $x=(1-t_1)a+t_1 b$ and $y=(1-t_2)a+t_2 b$. Propose the combined parameter $(1-s)t_1+s t_2$. The two inequalities $0\le(1-s)t_1+s t_2\le 1$ are discharged by nlinarith from $s,t_1,t_2\in[0,1]$. The vector identity $(1-s)x+s y=(1-((1-s)t_1+s t_2))a+((1-s)t_1+s t_2)b$ follows by rewriting the witnesses and applying the module tactic on the real vector space structure.
why it matters
This is a small convex-geometry lemma inside the distance-shell stack that physicalizes Erdős #132: shells are pairwise Euclidean distances reinterpreted as recognition-energy levels, and multiplicities count ordered pair events. Segment convexity is the elementary fact needed when arguments move points along chords or diameters (siblings include diameter-shell uniqueness and sparse-shell divergence).
No downstream theorem currently depends on it (used_by is empty), so it is infrastructure rather than a forcing-chain step. It does not touch T5–T8, the RCL, or the mass ladder; it only stabilizes planar geometry used by shell-occupancy counting. Closing more of the sparse-shell and flux-bridge siblings is where this lemma would earn citations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.