pith. sign in
module module high

IndisputableMonolith.NumberTheory.ClassicalZeroFreeRegion

show as:
view Lean formalization →

The module supplies the classical nonnegative trigonometric kernel for the Hadamard-de la Vallee-Poussin zero-free argument. Number theorists in the Recognition Science zeta program cite it when contrasting classical methods against the native approach. It consists of kernel definitions and supporting lemmas that build directly on the imported StripZeroFreeRegion module.

claimThe classical nonnegative trigonometric kernel $K(\theta)$ used in the Hadamard-de la Vallee-Poussin argument for a zero-free region of $\zeta(s)$ to the left of $\operatorname{Re}(s)=1$.

background

This module sits in the NumberTheory domain as the classical counterpart within the RS zeta program. It imports StripZeroFreeRegion, whose doc-comment states: "Phase 5 of the RS-native zeta program. This module does two things: 1. It records the proven Mathlib zero-free result on the line/half-plane Re(s) ≥ 1."

The module's own doc-comment identifies its focus: the classical nonnegative trigonometric kernel used in the Hadamard-de la Vallee-Poussin argument. Sibling declarations cover kernel identities such as the square form and nonnegativity statements.

proof idea

This is a definition module, no proofs. It organizes the classical kernel and its elementary properties as a foundation for later zero-free arguments.

why it matters in Recognition Science

The module supplies the classical kernel that supports zero-free region arguments in the Recognition Science framework. It provides the Hadamard-de la Vallee-Poussin side that contrasts with the RS-native results recorded in StripZeroFreeRegion. It touches the classical proof of a zero-free strip left of Re(s)=1.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (7)