The Cauchy-Schwarz Inequality for 2D Real Vectors via Sum-of-Squares Decomposition

We present a formally verified proof of the Cauchy-Schwarz inequality for two-dimensional real vectors. For all real numbers \(a, b, c, d\), we establish that \((ac + bd)^2 \leq (a^2 + b^2)(c^2 + d^2)\). The proof proceeds by introducing the cross-term witness \((ad - bc)^2 \geq 0\) and applying the Lagrange identity, which expresses the difference \((a^2 + b^2)(c^2 + d^2) - (ac + bd)^2\) as the perfect square \((ad - bc)^2\). The argument is formalized in the Platonic proof language with full verification, using no axioms beyond the standard bootstrap for real arithmetic. The explicit Sum-of-Squares (SOS) structure makes the proof constructive and renders the inequality's tightness immediately apparent: equality holds if and only if \((a, b)\) and \((c, d)\) are proportional.

Keywords: Cauchy-Schwarz inequality, sum-of-squares, Lagrange identity, formal verification

MSC 2020: 26D15 (Inequalities for sums, series, and integrals), 15A39 (Linear inequalities of matrices)