on_closed_segment_comm
plain-language theorem explainer
Closed-segment membership is independent of endpoint order: a planar point lies on the segment joining a and b exactly when it lies on the segment joining b and a. Anyone proving collinearity or diameter facts for ordered-pair distance shells in the Erdős #132 physicalization would cite this. The proof is a one-line Iff constructor that feeds the one-sided symmetry lemma both ways.
Claim. For planar points $a,b,x\in\mathbb{R}^2$, $x$ lies on the closed segment $[a,b]$ if and only if $x$ lies on the closed segment $[b,a]$. Equivalently, there exists $t\in[0,1]$ with $x=(1-t)a+tb$ if and only if there exists $s\in[0,1]$ with $x=(1-s)b+sa$.
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 positive-distance ordered multiplicity is twice the unordered count and classical thresholds double.
Point2 is the Euclidean plane $\mathbb{R}^2$. The predicate OnClosedSegment a b x means $x$ is an affine convex combination of the endpoints: there is $t\in[0,1]$ with $x=(1-t)\cdot a+t\cdot b$. That is the closed geometric segment between two visible planar states.
The one-sided companion already shows that if $x$ lies on $[a,b]$ then it lies on $[b,a]$, by the parameter flip $t\mapsto 1-t$. The present statement packages that fact as a biconditional.
proof idea
Term-mode Iff introduction. Both directions are exactly the existing one-sided symmetry lemma on_closed_segment_symm: from a witness $t\in[0,1]$ one obtains $1-t\in[0,1]$ and the affine identity $(1-t)a+tb=(1-(1-t))b+(1-t)a$. No new algebra is performed here; the constructor simply applies that lemma twice.
why it matters
In the distance-shell multiplicity development, closed segments appear when identifying collinear configurations, diameter shells, and sparse shells tied to Erdős #132. Commutativity of the segment predicate lets later arguments ignore endpoint order when working with ordered pair events.
No downstream consumers are wired yet (used_by is empty), so this is infrastructure: a small geometric hygiene lemma that keeps ordered-pair bookkeeping from forcing case splits on orientation. It sits under the broader RS reading of distance shells as recognition-energy shells, not under the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.