c0PoissonENN
plain-language theorem explainer
c0PoissonENN defines the extended nonnegative Poisson plateau constant for a profile ψ as the infimum of its Poisson plateau value set. Researchers on the Recognition Science route to the Riemann Hypothesis cite it when constructing explicit certificate windows that feed the B1 bridge from window integrals to oscillation bounds. The definition is a direct one-line application of the infimum operator to the plateau value set generated by Poisson convolution of ψ.
Claim. For a profile $ψ:ℝ→[0,∞]$, the Poisson plateau constant $c_0(ψ)$ is the infimum of the Poisson plateau value set of $ψ$.
background
The module constructs concrete window functions for the RH certificate layer. A flat-top window is built from profile ψ with a unit plateau on [-1,1] and scaled to mass 1 by 1/L. A Poisson-plateau window is obtained as the Poisson-kernel convolution of the same profile, likewise scaled by 1/L. These windows instantiate the B1 bridge: ∫ φ_{L,t0} d(-w') ≤ D together with φ_{L,t0} ≥ c on Ioo(t0-L,t0+L) implies oscOn w (Icc(t0-L,t0+L)) ≤ D/c.
proof idea
The definition is a one-line wrapper that applies the infimum operator to the Poisson plateau value set of the input profile ψ.
why it matters
This definition supplies the plateau constant that feeds the real-valued c0Poisson and the lemmas c0PoissonENN_le_poissonConv, ofReal_c0Poisson_le_poissonConv, hpoisson_plateau_of_c0Poisson, and the oscillation bound theorem oscOn_Icc_whitney_le_div_c0Poisson_mul_L_of_poissonPlateau. It fills the concrete certificate window layer in the BRF route to the Riemann Hypothesis, linking Poisson convolution to the B1 bridge inequality. In the Recognition Science framework it supports spectral emergence by providing explicit windows for oscillation control within the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.