OnClosedSegment
plain-language theorem explainer
The closed-segment relation says a planar point x lies on the Euclidean segment joining a and b, including endpoints, via a convex combination with parameter in [0,1]. Anyone proving triangle equality, endpoint recovery, or diameter-edge uniqueness in the ordered distance-shell development cites it. The body is a one-line existential definition, not a derived theorem.
Claim. For planar points $a,b,x\in\mathbb{R}^2$, write $x\in[a,b]$ when there exists $t\in\mathbb{R}$ with $0\le t\le 1$ and $x=(1-t)\,a+t\,b$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell occupancy is multiplicity. Ordered pairs are used for Lean simplicity, so for a positive distance the ordered multiplicity is twice the unordered count and the classical bound $\le n$ becomes $\le 2n$.
Points are elements of the Euclidean plane $\mathbb{R}^2$ (the local abbreviation of the bipartite distance-spectrum point type). The closed segment is the standard affine segment between two such points, including endpoints. Upstream holography "closed" predicates (plaquette and domino ledger parity) are unrelated name collisions; they do not enter this definition.
proof idea
Definition only: expand as existence of a real parameter $t$ in the unit interval such that $x$ equals the convex combination $(1-t)\bullet a+t\bullet b$. No lemmas are applied and there is no tactic proof.
why it matters
This is the geometric primitive behind the module's segment calculus. Downstream, triangle equality on a closed segment (dist a x + dist x b = dist a b) is proved from it, and the two endpoint-distance inequalities follow by nonnegativity and linear arithmetic. Endpoint recovery lemmas (if a segment point is as far from one end as the full length, it is the other end) also take it as hypothesis.
Higher in the file it appears in certificates for endpoint-disjoint diameter representatives: uniqueness of intersection points and the collinearity force when two diameter edges share two points. Those certificates support the ordered-shell multiplicity bound that is the RS reading of Erdős #132. It is pure planar Euclidean geometry scaffolding, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.