poissonKernel
plain-language theorem explainer
The poissonKernel definition supplies the normalized Poisson kernel on the real line as the map sending x to the extended nonnegative real (1/π) b / (b² + x²). Researchers constructing the BRF certificate windows for the Riemann Hypothesis would cite this when forming the Poisson-plateau window from a profile ψ. The definition is a direct one-line term encoding of the classical formula with no lemmas invoked.
Claim. The normalized Poisson kernel at height $b$ is the function $P_b : ℝ → ℝ_{≥0}^∞$ defined by $P_b(x) = (1/π) b / (b² + x²)$.
background
The CertificateWindow module constructs concrete window functions φ_{L,t0} for the RH certificate layer. A flat-top window is built from a profile ψ with unit plateau on [-1,1] scaled by 1/L; the Poisson-plateau variant is the convolution of ψ with the Poisson kernel at height b, again scaled by 1/L. This kernel is the standard harmonic-analysis object on the line, here lifted to ℝ≥0∞ values. The module imports WindowToOscillation to obtain the B1 bridge: (∫ φ_{L,t0} d(-w') ≤ D) + (φ_{L,t0} ≥ c on Ioo(t0-L,t0+L)) implies oscOn w (Icc(t0-L,t0+L)) ≤ D/c. Upstream structures supply the J-cost convexity from PhiForcingDerived and the gauge content from SpectralEmergence that frame the overall Recognition Science setting.
proof idea
The definition is a direct term-mode encoding that applies the classical Poisson density formula and wraps the result in ENNReal.ofReal. No lemmas or tactics are used; it is literally the one-line expression (1/π) b / (b² + x²) lifted to extended reals.
why it matters
This definition is the immediate building block for poissonConv, which realizes the Poisson-plateau window and feeds the oscillation bound used in the RH certificate. It supplies the concrete smoothing operator required by the module's B1 bridge from WindowToOscillation. In the Recognition framework it connects the spectral-emergence structures (SU(3)×SU(2)×U(1) and three generations) to the numerical certificate layer via the phi-ladder and J-cost minimization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.