IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion
The module introduces the classical nonnegative trigonometric kernel for the Hadamard-de la Vallee-Poussin zero-free region argument in the RS-native zeta program. Researchers in analytic number theory cite it when connecting classical zeta results to the Recognition Science framework. It builds directly on the upstream StripZeroFreeRegion module's zero-free result for Re(s) ≥ 1 and organizes kernel properties via sibling declarations.
claimThe classical nonnegative trigonometric kernel $K$ used in the Hadamard-de la Vallée-Poussin argument, satisfying $K(θ) ≥ 0$ and expressible as a square.
background
This 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.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the classical kernel that enables the de La Vallee-Poussin zero-free region, providing a benchmark that feeds the broader RS zeta program and the strip zero-free results. It fills the classical Hadamard-de la Vallee-Poussin step referenced in the module doc-comment.
scope and limits
- Does not establish zero-free regions beyond the classical bound.
- Does not address the full Riemann hypothesis.
- Does not incorporate RS-specific constants such as phi.
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