orient2_of_on_closed_segment
plain-language theorem explainer
If a planar point x lies on the closed segment [c,d], its signed orientation relative to the directed line ab is the same convex combination of the endpoint orientations. Segment-separation and geometric-disjointness arguments in the distance-shell multiplicity development cite this. The proof unpacks the segment parameter and applies affinity of orient2 in its third argument.
Claim. Let $a,b,c,d,x\in\mathbb{R}^2$. If $x$ lies on the closed segment $[c,d]$, then there exists $t\in[0,1]$ such that $\mathrm{orient}_2(a,b,x)=(1-t)\,\mathrm{orient}_2(a,b,c)+t\,\mathrm{orient}_2(a,b,d)$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count. Points are planar Euclidean states (Point2 = $\mathbb{R}^2$).
OnClosedSegment c d x means $x=(1-t)c+td$ for some $t\in[0,1]$. The quantity orient2 a b p is the standard planar orientation (signed parallelogram area of $b-a$ and $p-a$), linear in the third argument.
The companion lemma orient2_affine_third records that affinity: substituting an affine combination for the third point yields the matching combination of orientations. The present statement specializes that identity to points already known to lie on a closed segment.
proof idea
Term-mode unpack of the segment witness. Destructure hx : OnClosedSegment c d x to obtain $t\in[0,1]$ and the equality $x=(1-t)\bullet c+t\bullet d$. Reuse that same $t$ in the existential conclusion, rewrite the left-hand orientation via the segment equation, and finish by orient2_affine_third a b c d t.
why it matters
Feeds proper_segment_separation_geometrically_disjoint: a proper separation certificate implies geometric disjointness of ordered edges, because a meeting point on $[c,d]$ would also lie on line $ab$, forcing a convex combination of two same-strict-sign orientations to vanish. That contradiction step needs exactly this convex-combination identity.
In the broader distance-shell program, controlled non-crossing of planar edges underpins sparse-shell and diameter-shell counting for the ordered Erdős #132 threshold. The lemma is pure planar geometry; it does not itself invoke the forcing chain (T5–T8) or the mass ladder, but it is infrastructure for the RS reading of shell occupancy in $D=2$ configurations embedded in the $D=3$ spatial setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.