exists_scalar_of_orient2_zero
plain-language theorem explainer
If three planar points are orientation-zero and the first two are distinct, the third is an affine multiple of the base segment: there is a real scalar t with c − a = t(b − a) in both coordinates. Anyone proving collinear diameter or lens-segment claims in the Erdős #132 shell analysis cites this. The proof splits on a nonzero coordinate difference and builds t as that ratio.
Claim. Let $a,b,c\in\mathbb{R}^2$ with $a\neq b$. If the signed planar orientation $\mathrm{orient}_2(a,b,c)=0$, then there exists $t\in\mathbb{R}$ such that $c_i-a_i=t(b_i-a_i)$ for both coordinates $i\in\{0,1\}$.
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 (threshold $\le n$ becomes $\le 2n$). Points live in Point2, the planar type from the bipartite distance spectrum.
The signed quantity $\mathrm{orient}_2(a,b,c)$ is the standard 2D cross-product test for collinearity of the triple. Vanishing orientation means $c$ lies on the line through $a$ and $b$. The theorem unpacks that geometric condition into an explicit affine parameter $t$ along the base vector $b-a$.
This is pure planar Euclidean geometry supporting later shell-multiplicity arguments; it does not itself invoke the forcing chain or recognition cost $J$.
proof idea
From $a\neq b$, at least one coordinate differs. Case-split on that coordinate.
If $a_0\neq b_0$, set $t=(c_0-a_0)/(b_0-a_0)$. The $i=0$ identity is immediate by field simplification. The $i=1$ identity rearranges the expanded orientation equation $\mathrm{orient}_2=0$ and finishes by linear arithmetic.
If instead $a_1\neq b_1$, take $t=(c_1-a_1)/(b_1-a_1)$ and swap the roles of the two coordinates. No external lemmas beyond field and linarith machinery.
why it matters
This is the central planar-collinearity unpack for the distance-shell module. Downstream, onClosedSegment_of_orient2_zero_in_lens uses it to conclude that a collinear point inside the closed lens $D(a,\Delta)\cap D(b,\Delta)$ with $\mathrm{dist}(a,b)=\Delta$ lies on the closed segment $[a,b]$. The four-point contradiction collinearDiameterEndpointContradiction likewise relies on the same line parametrization: four collinear points with two diameter pairs and all cross distances $\le\Delta$ force endpoint coincidence via $|s-t|=1$ with parameters in $[0,1]$.
In the RS reading of Erdős #132, diameter shells control sparse-shell occupancy. Without an explicit scalar along the line, those geometric-disjointness and lens arguments cannot close in coordinates. The result is local Euclidean scaffolding, not a forcing-chain step (T0–T8), but it underwrites the planar geometry those shell bounds need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.