affine_zero_of_nonpos_nonneg
plain-language theorem explainer
Any real affine combination of a nonpositive number and a nonnegative number hits zero for some weight in [0,1]. Analysts and discrete geometers cite it as the 1D intermediate-value step that forces a planar orientation determinant to vanish on a segment. The proof is a short case split: both zero when equal, otherwise the explicit convex weight t = (-u)/(v-u).
Claim. If $u,v\in\mathbb{R}$ satisfy $u\le 0$ and $v\ge 0$, then there exists $t\in[0,1]$ such that $(1-t)u+tv=0$.
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$).
The signed planar orientation $$\mathrm{orient2}(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$$ is twice the signed area of triangle $abc$. Vanishing means $c$ lies on the line through $a$ and $b$.
This lemma is pure 1D convex analysis: the affine path from a nonpositive value to a nonnegative value must cross zero. It is the scalar engine behind the geometric intermediate-value statement for orientation on a segment.
proof idea
Case on whether $u=v$. If equal, both must be zero by the sign hypotheses; take $t=0$ and simplify by ring.
If unequal, set $t=(-u)/(v-u)$. The denominator is positive because $u\le 0\le v$ and $u\ne v$ force $u<v$. Nonnegativity of $t$ is division of two nonnegative quantities; $t\le 1$ rewrites as $-u\le v-u$, i.e. $0\le v$. The affine combination identity is then field simplification plus ring.
why it matters
Immediate parent is exists_orient2_zero_on_segment_of_nonpos_nonneg: if the endpoints of segment $[c,d]$ have opposite orientation signs relative to line $ab$, some point of the segment lies on that line. The parent instantiates this lemma at $u=\mathrm{orient2}(a,b,c)$ and $v=\mathrm{orient2}(a,b,d)$, then rebuilds the planar point as the same convex combination of $c$ and $d$.
That geometric IVT is part of the combinatorial toolkit for distance-shell multiplicity and the RS reading of Erdős #132 (sparse shells, diameter shells, ordered spectra). It is ordinary real analysis, not a forcing-chain step, but it underwrites the planar incidence arguments the shell-multiplicity development needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.