on_closed_segment_strict
plain-language theorem explainer
An interior point of a closed Euclidean segment in the plane, distinct from both endpoints, admits a strict convex-combination parameter with 0 < t < 1. Geometry and combinatorial distance-shell arguments cite this when excluding endpoints from shell occupancy. The proof unpacks the closed-segment witness and rules out the boundary parameter values by antisymmetry of ≤.
Claim. If $x$ lies on the closed line segment between planar points $a$ and $b$, and $x \neq a$, $x \neq b$, then there exists $t \in \mathbb{R}$ with $0 < t < 1$ such that $x = (1-t)\,a + t\,b$.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the set of pairwise Euclidean distances; physically it is a two-body recognition-energy shell, and its multiplicity is the shell occupancy. Ordered pairs are used for Lean simplicity, so the classical threshold $\le n$ becomes $\le 2n$.
Planar points are elements of Euclidean space $\mathbb{R}^2$. The closed-segment predicate asserts existence of a real parameter $t$ with $0 \le t \le 1$ such that the point equals the affine combination $(1-t)\bullet a + t\bullet b$. The present result upgrades that weak parameter interval to a strict one once the point is known not to be either endpoint.
proof idea
Destructure the closed-segment hypothesis to a witness $t$ with $0 \le t \le 1$ and the affine identity. Reuse that same $t$ and prove the two strict inequalities by contradiction. If not $0 < t$, then $t \le 0$; antisymmetry with $0 \le t$ forces $t = 0$, so the affine formula collapses to the left endpoint, contradicting the given inequality. Symmetrically, not $t < 1$ forces $t = 1$ and collapse to the right endpoint. The endpoint rewrites are discharged by the module tactic on the affine combination.
why it matters
Infrastructure for geometric bookkeeping inside the ordered distance-shell development that physicalizes Erdős #132. Sibling notions (sparse shells, diameter shells, ordered shell multiplicity, the ordered Erdős-132 statement) need interior segment points to carry a strict barycentric parameter when counting occupancy or when two ordered edges meet geometrically. No downstream theorem currently depends on this declaration, so it is local geometry rather than a forcing-chain landmark (T0–T8, RCL, phi, eight-tick octave). It closes a small gap between the weak closed-segment definition and the strict-interior language used in shell arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.