certificateWindowPoisson
plain-language theorem explainer
certificateWindowPoisson constructs the scaled Poisson-plateau window φ^P_{L,t0} for Riemann Hypothesis certificates along the BRF route. Analysts applying the B1 bridge on Whitney intervals cite this definition to obtain concrete window functions from a profile ψ. The implementation is a one-line wrapper that scales the Poisson convolution by 1/L after centering at t0.
Claim. The scaled Poisson-plateau window is defined by $φ^P_{L,t_0}(t) := (1/L) (P_b * ψ)((t - t_0)/L)$, taking values in the extended non-negative reals.
background
This module defines the concrete window functions φ_{L,t0} used in the RH certificate layer. The Poisson-plateau window is formed by convolving a profile ψ with the Poisson kernel at parameter b, then scaling the result by 1/L and shifting the center to t0. The module imports the B1 bridge from WindowToOscillation, which converts an integral bound on the window together with a plateau lower bound into an oscillation control on Icc(t0-L, t0+L). Upstream, poissonConv supplies the convolution operation while structures from PhiForcingDerived and SpectralEmergence calibrate the underlying J-cost and gauge content.
proof idea
The definition is a one-line wrapper that applies poissonConv to the shifted and scaled argument (t - t0)/L and multiplies by ENNReal.ofReal (1/L). No further lemmas or tactics are required.
why it matters
This definition is invoked by the downstream theorems oscOn_Icc_whitney_le_div_c0_mul_L_of_poissonPlateau and oscOn_Icc_whitney_le_div_c0Poisson_mul_L_of_poissonPlateau. Those theorems instantiate the B1 bridge to bound oscOn w on the Whitney interval. In the Recognition framework the construction supplies the concrete certificate windows needed for the Riemann Hypothesis proof route, consistent with the phi-ladder and eight-tick octave from the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.