on_closed_segment_symm
plain-language theorem explainer
Closed segments in the plane are symmetric in their endpoints: if a point lies on the segment from a to b, it also lies on the segment from b to a. Anyone handling ordered-edge geometry or shell occupancy for the Erdős #132 physicalization cites this. The proof reparametrizes the convex combination by t ↦ 1−t and checks the affine identity.
Claim. For planar points $a,b,x\in\mathbb{R}^2$, if $x$ lies on the closed line segment joining $a$ to $b$ (i.e., $x=(1-t)a+tb$ for some $t\in[0,1]$), then $x$ also lies on the closed line segment joining $b$ to $a$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity; for a positive distance, ordered multiplicity is twice the unordered count, so the classical bound $\le n$ becomes $\le 2n$.
Points are planar Euclidean states (Point2 $\simeq \mathbb{R}^2$). The predicate "on the closed segment" means $x$ is an affine convex combination of the endpoints: there exists $t\in[0,1]$ with $x=(1-t)\cdot a+t\cdot b$. That is the geometric substrate for later notions of edges meeting, simple crossings, and diameter shells.
proof idea
Unpack the witness $t\in[0,1]$ and the identity $x=(1-t)a+tb$. Supply the reversed parameter $1-t$; the bounds $0\le 1-t\le 1$ are immediate from $0\le t\le 1$ by linear arithmetic. Rewrite $x$ and finish by the module tactic, which rearranges the affine combination into $(1-(1-t))b+(1-t)a$.
why it matters
Endpoint symmetry is the basic invariance that lets ordered-edge geometry forget orientation. It is the one-direction half of the iff form of segment symmetry, and it is applied directly when swapping either endpoint of a geometrically or simply meeting ordered edge pair. Downstream crossing lemmas (including the symmetric orientation-zero-on-segment statement) and the unordered-edge missing criterion for geometrically disjoint pairs all route through this fact. In the RS reading of Erdős #132, that keeps shell-occupancy counts independent of arbitrary edge orientation choices on the planar point set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.