certificateWindowFlat
plain-language theorem explainer
The certificateWindowFlat definition constructs the flat-top window φ_{L,t0} by scaling a profile ψ with unit plateau on [-1,1] by the factor 1/L and recentering at t0, returning a function to extended nonnegative reals. Analysts working on the Riemann Hypothesis via the BRF certificate route cite this to instantiate explicit windows for oscillation bounds. The definition proceeds by a direct one-line scaling and recentering of the input profile.
Claim. The flat-top window function φ_{L,t_0} : ℝ → ℝ_{≥0}^∞ associated to a profile ψ : ℝ → ℝ at scale L > 0 and center t_0 is given by φ_{L,t_0}(t) := ofReal(ψ((t - t_0)/L) / L).
background
This module supplies concrete window functions for the Riemann Hypothesis certificate layer along the BRF route. The flat-top window is built from a profile ψ that takes the constant value 1 on the interval [-1,1], then scaled by 1/L so that the total mass equals 1. The module also defines a Poisson-plateau variant and instantiates the B1 bridge from WindowToOscillation: if the integral of φ_{L,t0} against the negative Stieltjes measure of an antitone w is at most D and φ_{L,t0} ≥ c on the open interval of length 2L, then the oscillation of w on the closed interval is at most D/c.
proof idea
The definition is a one-line wrapper that applies ENNReal.ofReal to the rescaled profile value ψ((t - t0)/L) / L.
why it matters
This definition supplies the explicit flat-top window used by the lower-bound lemma lower_of_plateau_one and the oscillation-control theorem oscOn_Icc_whitney_le_mul_L_of_flatTop. It fills the concrete instantiation step required by the B1 bridge in the RH certificate construction, allowing the transition from window lower bounds to oscillation estimates on intervals of length 2L. In the Recognition Science framework it supports the number-theoretic side of the RH analysis by providing the scaled windows needed for the certificate layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.