orient2_affine_third
plain-language theorem explainer
Orientation of an affine combination of two plane points relative to a directed line equals the same affine combination of the endpoint orientations. Planar geometers and anyone proving segment-line incidence or thrackle-type separation would cite it. The proof unfolds the 2D determinant definition and finishes by ring normalization.
Claim. For points $a,b,c,d$ in the Euclidean plane $\mathbb{R}^2$ and any real scalar $t$, $$\operatorname{orient}(a,b,(1-t)\,c+t\,d)=(1-t)\,\operatorname{orient}(a,b,c)+t\,\operatorname{orient}(a,b,d),$$ where $\operatorname{orient}(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$ is the signed twice-area of triangle $abc$.
background
The module Distance Shell Multiplicity records the RS physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is the shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count.
Point2 is the Euclidean plane $\mathbb{R}^2$. The orientation form is the signed twice-area determinant: it vanishes exactly when the third point lies on the line through the first two, and its sign labels the open half-planes. The present identity states that this form is affine in its third argument, so orientation varies linearly along any affine line (in particular along a segment).
proof idea
Short tactic proof with no external lemmas. Unfold the determinant definition of orientation, simplify the scalar multiplications and coordinate projections on the affine combination $(1-t),c+t,d$, then apply ring normalization. The resulting polynomial identity in the eight coordinates and the parameter $t$ is the bilinearity of the $2\times 2$ determinant in its third column.
why it matters
Local engine for four downstream results in the same module. It discharges the equality step in the closed-segment convex-combination theorem (orientation of a point on $[c,d]$ is a convex mix of the endpoint orientations). That fact, with an affine intermediate-value lemma, yields existence of an orientation zero on a segment whose endpoints have opposite signs. Same-side separation (segments on one strict side of a line are geometrically disjoint from the spanning segment) and opposite-side meeting under diameter cross-distance bounds both route through the same affine identity.
Those separation and incidence lemmas underwrite thrackle and matching arguments in the ordered shell-multiplicity analysis of Erdős #132, where diameter shells control sparse-shell flux in the RS recognition-energy reading. The identity itself is pure planar algebra, not a T0-T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.