IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion
This module supplies the classical nonnegative trigonometric kernel and supporting lemmas for the Hadamard-de la Vallee-Poussin zero-free region argument. It extends the Re(s) >= 1 zero-free result imported from StripZeroFreeRegion inside the RS-native zeta program. Analytic number theorists comparing classical and modern zero-free strips would cite these constructions. The module organizes targeted definitions and identities around kernel nonnegativity and square representations.
claimThe classical nonnegative trigonometric kernel $K(θ)$ satisfies $K(θ) = |1 + 2e^{iθ} + e^{2iθ}|^2$ (equivalently $3 + 4 cos θ + cos 2θ$) and is used to obtain a zero-free region for $ζ(s)$ with $Re(s) > 1 - c / log |t|$ for some $c > 0$.
background
The module belongs to the NumberTheory domain and forms part of Phase 5 of the RS-native zeta program. It imports the StripZeroFreeRegion module, whose doc-comment records the proven Mathlib zero-free result on the line/half-plane Re(s) ≥ 1. The module's own doc-comment identifies its focus as the classical nonnegative trigonometric kernel employed in the Hadamard-de la Vallee-Poussin argument. Sibling declarations establish the kernel's square representation, nonnegativity, and derived statements such as logZeroFreeStrip_of_deLaValleePoussin and the bridge to the zero-free strip.
proof idea
This is a definition module containing supporting lemmas for the kernel properties; no overarching proof. Individual lemmas establish the equality of the kernel to a square expression and its nonnegativity, followed by applications that produce the logarithmic zero-free strip and the bridge result.
why it matters in Recognition Science
This module supplies the classical zero-free region construction that complements the RS-native results in StripZeroFreeRegion. It fills the classical Hadamard-de la Vallee-Poussin step in the zeta zero-free chain and enables direct comparison with the RS program. The sibling bridge lemma connects the imported Re(s) ≥ 1 result to the classical strip.
scope and limits
- Does not derive explicit numerical width of the zero-free region.
- Does not prove the prime number theorem or its error terms.
- Does not incorporate RS-native constants such as phi or the mass formula.
- Does not address higher-order zero-free regions or density theorems.
depends on (1)
declarations in this module (7)
-
theorem
deLaValleePoussin_trig_kernel_eq_square -
theorem
deLaValleePoussin_trig_kernel_nonneg -
structure
DeLaValleePoussinZeroFreeRegion -
def
logZeroFreeStrip_of_deLaValleePoussin -
theorem
stripZeroFreeBridge_of_deLaValleePoussin -
structure
ClassicalZeroFreeRegionAttackSurface -
def
classicalZeroFreeRegionAttackSurface