kernelBL_pos
plain-language theorem explainer
The Boltzmann washout survival kernel from source time t' to freeze-out tf is strictly positive for any real washout rate. Cosmologists tracking baryon asymmetry after sphaleron reprocessing cite this to guarantee washout can only suppress, never reverse, the sign of a sourced B-L charge. The proof is a one-line appeal to positivity of the real exponential.
Claim. For any washout rate $\Gamma_w:\mathbb{R}\to\mathbb{R}$ and any times $t',t_f\in\mathbb{R}$, the survival kernel $\exp\bigl(-\int_{t'}^{t_f}\Gamma_w\bigr)$ satisfies $0 < \exp\bigl(-\int_{t'}^{t_f}\Gamma_w\bigr)$.
background
This module stages honest, small targets for the baryogenesis derivation loop. The standing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the final baryon number is zero. Loop targets must not fake missing mechanism with axioms or True placeholders.
The survival kernel is the genuine Boltzmann factor $\exp(-\int_{t'}^{t_f}\Gamma_{\mathrm{wash}})$, not a polynomial proxy such as $(1-\varphi^{-8})^k$. It multiplies sourced charge between production time $t'$ and freeze-out $t_f$. The washout exponent is the integrated rate that appears in the exponent; the kernel is its negative exponential.
Sibling facts already record that a nonnegative accumulated washout forces the survival weight to be at most one, and that final $B$ vanishes exactly when $B-L$ does under equilibrium reprocessing.
proof idea
One-line term proof. Unfold the kernel to $\mathrm{Real.exp}(-\mathrm{washoutExponent},\Gamma_w,t',t_f)$ and apply Real.exp_pos, which states that the real exponential is strictly positive on all of $\mathbb{R}$. No estimate on $\Gamma_w$ or on the integration window is required: positivity holds for every real exponent.
why it matters
In the baryogenesis staging lane this pins a basic sign property of the washout kernel: suppression is allowed, sign flip is not. That property underwrites the sphaleron zero-protection obstruction highlighted in the module doc: if sourced $B-L$ is zero, reprocessing cannot manufacture a nonzero final $B$ by washout alone. Downstream siblings such as the final-$B$ obstruction and the freeze-out window rely on a kernel that stays in $(0,\infty)$ so that vanishing of the source remains equivalent to vanishing of the relic. No used-by edges are recorded yet; the lemma is infrastructure for the Steve baryogenesis loop rather than a closed paper proposition. It does not itself invoke the forcing chain (T0-T8), RCL, or the $\varphi$-ladder mass formula; it is pure real analysis inside the cosmology staging layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.