pith. sign in
module module high

IndisputableMonolith.NumberTheory.RiemannHypothesis.CertificateWindow

show as:
view Lean formalization →

The CertificateWindow module defines the nonnegative flat-top window φ_{L,t0} tied to a profile ψ at scale L and center t0. It forms part of the window-to-oscillation bridge in the BRF route toward the Riemann Hypothesis. The module supplies auxiliary definitions including Poisson kernels and plateau values that support measure control on the positive distribution -w'. Researchers working on analytic number theory proofs of RH would reference these window constructions.

claim$ϕ_{L,t_0}(t) := ofReal(ψ((t-t_0)/L)/L)$ for a profile $ψ:ℝ→ℝ$ with $ψ≥0$, matching the manuscript form $L^{-1}ψ((t-t_0)/L)$.

background

This module sits in the NumberTheory.RiemannHypothesis section and imports WindowToOscillation, whose doc-comment states it targets the bridge step immediately preceding Lemma local-to-global-wedge: a window (test-function) bound for the positive distribution -w' implies a bound on the essential oscillation Δ_I(w) = essSup_I w - essInf_I w. The central object is the flat-top window associated to a profile ψ at scale L>0 and center t0, given explicitly by ofReal(ψ((t-t0)/L)/L). Sibling definitions include certificateWindowFlat, poissonKernel, poissonConv, and plateau lemmas such as lower_of_plateau_one and hpoisson_plateau_of_c0Poisson that operationalize the window for oscillation estimates.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the window objects required for the oscillation control step in the BRF approach to the Riemann Hypothesis. It directly supports the bridge from window/measure bounds to essential oscillation bounds as described in the upstream WindowToOscillation module, which precedes the local-to-global-wedge lemma in the Riemann-proofs documentation.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (14)