c0Poisson
plain-language theorem explainer
c0Poisson supplies the real-valued Poisson plateau constant c0(ψ) by transporting the extended infimum c0PoissonENN ψ via toReal. Researchers building oscillation bounds for Riemann-Hypothesis certificate windows cite it to keep the B1 bridge inside ordinary real analysis. The definition is realized as a one-line wrapper that applies the transport after the infimum over the plateau value set has been formed.
Claim. Let $c_0(ψ)$ denote the real number obtained by transporting the infimum of the Poisson-plateau values of the profile $ψ:ℝ→[0,∞]$ to the standard reals, i.e., $c_0(ψ) :=$ toReal of that infimum.
background
The CertificateWindow module constructs concrete window functions φ_{L,t0} for the RH (BRF route). One family is obtained by convolving a profile ψ with a Poisson kernel and scaling by 1/L; the plateau height of this convolution on the unit interval is captured by the infimum c0(ψ). The module doc states that the B1 bridge then converts a mass bound on the derivative together with a lower bound on the window height into an oscillation bound on the target function w.
proof idea
The definition is a one-line wrapper that applies the toReal transport (from RealsFromLogic) to the result of c0PoissonENN ψ, which itself is the sInf of poissonPlateauValSet ψ.
why it matters
c0Poisson supplies the real plateau height required by the theorem oscOn_Icc_whitney_le_div_c0Poisson_mul_L_of_poissonPlateau that closes the B1 bridge for Poisson windows. It is invoked in the supporting lemmas hpoisson_plateau_of_c0Poisson and ofReal_c0Poisson_le_poissonConv that establish the lower bound on the convolution inside |x|≤1. Within the Recognition Science framework it contributes the concrete Poisson-plateau constant needed for the certificate layer of the Riemann-Hypothesis route.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.