module module moderate

`IndisputableMonolith.NumberTheory.RiemannHypothesis.CertificateWindow`

The CertificateWindow module defines the nonnegative flat-top window φ_{L,t0} associated to a profile ψ at scale L and center t0 for use in Riemann Hypothesis analysis. It supplies scaled test functions matching the manuscript form L^{-1} ψ((t-t0)/L) when ψ ≥ 0. The module imports WindowToOscillation and Mathlib convolution machinery while declaring sibling objects for Poisson kernels and plateau values. This is a definitions module supporting the window-to-oscillation bridge in the BRF route.

claimThe central object is the flat-top window defined by φ_{L,t0}(t) := ofReal(ψ((t-t0)/L)/L) for a profile ψ:ℝ→ℝ with ψ≥0, L>0 and t0∈ℝ.

background

This module sits in the NumberTheory.RiemannHypothesis domain and targets the bridge from window/measure control to oscillation control. The upstream WindowToOscillation module states: 'This file targets the bridge step immediately preceding Lemma local-to-global-wedge in docs/primes/Riemann-proofs/Riemann-active.txt: 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.' It introduces the flat-top window together with Poisson kernel and convolution auxiliaries.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the certificate window φ_{L,t0} and related Poisson objects that feed the oscillation-control arguments of the BRF route, specifically the step toward the local-to-global-wedge lemma referenced in the upstream doc-comment.

scope and limits

Does not prove any form of the Riemann Hypothesis.
Does not contain numerical verification or explicit bounds.
Does not implement the local-to-global-wedge lemma itself.

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.NumberTheory.RiemannHypothesis.WindowToOscillation module_import

declarations in this module (14)

def certificateWindowFlat L38
lemma lower_of_plateau_one L45
def poissonKernel L81
def poissonConv L85
def poissonPlateauValSet L94
def c0PoissonENN L98
def c0Poisson L105
lemma c0PoissonENN_le_poissonConv L108
lemma ofReal_c0Poisson_le_poissonConv L116
lemma hpoisson_plateau_of_c0Poisson L126
def certificateWindowPoisson L141
theorem oscOn_Icc_whitney_le_mul_L_of_flatTop L148
theorem oscOn_Icc_whitney_le_div_c0_mul_L_of_poissonPlateau L169
theorem oscOn_Icc_whitney_le_div_c0Poisson_mul_L_of_poissonPlateau L223