deLaValleePoussin_trig_kernel_eq_square
plain-language theorem explainer
The identity equates the classical de la Vallee-Poussin trigonometric kernel 3 + 4 cos θ + cos 2θ to twice the square of (cos θ + 1) for real θ. Number theorists working on zero-free regions cite it as the algebraic positivity ingredient in the Hadamard-de la Vallee-Poussin argument for the Riemann zeta function. The proof reduces the left-hand side via the cosine double-angle formula and normalizes the resulting polynomial identity.
Claim. For all real numbers $θ$, $3 + 4 cos θ + cos(2θ) = 2 (cos θ + 1)^2$.
background
The module tracks track B1 of the RH unconditional-closure plan and isolates the elementary trigonometric positivity kernel as a prerequisite for the logarithmic zero-free strip. It proves the identity 3 + 4 cos θ + cos 2θ = 2 (cos θ + 1)^2 ≥ 0 without claiming the full analytic theorem. Upstream structures from J-cost, spectral emergence, and kernel families supply the broader Recognition Science setting but are not invoked in this elementary step.
proof idea
The proof rewrites the double-angle cosine term via the standard double-angle formula and applies ring normalization to confirm the polynomial identity.
why it matters
This supplies the algebraic identity applied by the downstream nonnegativity theorem to establish 3 + 4 cos θ + cos 2θ ≥ 0. It fills the elementary step in the classical zero-free region construction inside Recognition Science's plan for unconditional RH closure, positioned as the starting point for the logarithmic strip input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.