kernelBL
plain-language theorem explainer
Defines the B−L Boltzmann survival weight from a source time t' to freeze-out tf as exp of minus the integrated washout rate. Cosmology and baryogenesis workers cite it inside relic-charge integrals. The body is a one-line Real.exp of the negated washout exponent; it is the genuine exponential factor, not a discrete φ-ladder polynomial.
Claim. For a washout rate $\Gamma_w:\mathbb{R}\to\mathbb{R}$ and times $t',t_f\in\mathbb{R}$, the B−L survival kernel is $K_{\mathrm{BL}}(\Gamma_w;t',t_f)=\exp\bigl(-\int_{t'}^{t_f}\Gamma_w(s)\,ds\bigr)$.
background
The module stages honest theorem targets for the Steve baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ plus sphaleron equilibration forces vanishing final baryon number.
The washout exponent is the definite integral $\int_{t'}^{t_f}\Gamma(s),ds$ of a rate along the interval from emission to freeze-out. The present definition packages that integral into the classical Boltzmann survival factor $\exp(-\int\Gamma_{\mathrm{wash}})$. The doc-comment stresses that this is the genuine continuous exponential, not a discrete Recognition ladder factor of the form $(1-\varphi^{-8})^k$.
Related kernel families elsewhere (BIT exponential kernels, ILG radial kernels) share the name "kernel" but live in different physical settings; here the object is strictly the washout survival weight for comoving $B-L$.
proof idea
Definition only: unfold to $\mathrm{Real.exp}(-\mathrm{washoutExponent},\Gamma_w,t',t_f)$, where the washout exponent is the interval integral of $\Gamma_w$. No tactics or lemmas beyond the Mathlib exponential.
why it matters
This weight is the survival factor inside the relic charge profile $\int_{t_0}^{t_f} a^3 S_X(t'),K_{\mathrm{BL}}(\Gamma_w;t',t_f),dt'$, the B4 acceptance shape for Boltzmann relics. Downstream lemmas record that the kernel is always strictly positive (washout suppresses, never sign-flips) and is at most one whenever the accumulated washout is nonnegative.
It also sits under the source-off falsifier: if $\dot\chi\equiv 0$ on the window, the integrand vanishes and the relic is identically zero. The washout-gate theorem later requires that strong washout of $B-L$ be carried by an operator with $\Delta(B-L)\neq 0$ (Weinberg contact, not sphalerons), discharging the physical meaning of a nonzero $\Gamma_w$ that this kernel assumes.
In the staging loop the definition prevents faking freeze-out by a polynomial ladder factor; the continuous Boltzmann form is the honest contact with standard cosmology.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.