kernelBL_le_one_of_nonneg
plain-language theorem explainer
If the integrated washout rate from source time t' to freeze-out tf is nonnegative, the Boltzmann B-L survival kernel is at most 1. Cosmology and baryogenesis workers cite this to bound relic charge by the bare source integral. The proof unfolds the exponential kernel and applies the standard exp(−x) ≤ 1 criterion for x ≥ 0.
Claim. Let $\Gamma_w:\mathbb{R}\to\mathbb{R}$ and $t',t_f\in\mathbb{R}$. If the washout exponent $\int_{t'}^{t_f}\Gamma_w(s)\,ds$ is nonnegative, then the survival kernel $\exp\bigl(-\int_{t'}^{t_f}\Gamma_w(s)\,ds\bigr)\le 1$.
background
The module stages honest, small targets for the Steve baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus equilibration forces vanishing final baryon number. Loop targets must not fake missing mechanism with axioms or True stand-ins.
The washout exponent is the definite integral $\int_{t'}^{t_f}\Gamma_w$ of a washout rate along the forward interval. The survival kernel is the genuine Boltzmann factor $\exp(-\int_{t'}^{t_f}\Gamma_w)$, not a polynomial proxy such as $(1-\varphi^{-8})^k$. Nonnegative accumulated washout is the physical regime when $\Gamma_w$ does not reverse-sign the integral.
Downstream of the kernel sits the Boltzmann relic (comoving $B-L$ charge surviving to freeze-out): the source weighted by this exponential under the integral, the B4 acceptance shape.
proof idea
Unfold the definition of the survival kernel to $\exp(-W)$ with $W$ the washout exponent. Rewrite the goal via Real.exp_le_one_iff, which reduces $\exp(-W)\le 1$ to $-W\le 0$. The hypothesis $W\ge 0$ finishes the inequality by linear arithmetic.
why it matters
In the baryogenesis staging lane this is a basic sanity bound: washout can only suppress the survival weight, never amplify it above unity, once the integrated rate is nonnegative. That keeps relic-charge estimates honest relative to the bare source integral and blocks inflated $B-L$ survival claims.
It supports the module's obstruction program (sphaleron equilibrium with zero $B-L$ yields zero final $B$) by guaranteeing the exponential kernel is a contraction factor rather than a gain. No downstream theorems currently depend on it; it is a local lemma ready for relic-charge and freeze-out window arguments. Framework-wise it is standard Boltzmann kinetics inside the RS cosmology stack, not a T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.