washoutExponent
plain-language theorem explainer
The washout exponent is the definite integral of a washout rate Γ from production time t' to freeze-out tf. Cosmologists and baryogenesis modelers cite it as the optical depth that enters the Boltzmann survival kernel. The body is a one-line integral definition, not a derived identity.
Claim. For a real-valued rate function $\Gamma$ and times $t', t_f$, the washout exponent is $\int_{t'}^{t_f} \Gamma(s)\, ds$.
background
This module stages honest theorem targets for the Steve baryogenesis loop. The governing 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.
In the Boltzmann treatment of baryon washout, the survival weight of charge produced at time $t'$ and frozen at $t_f$ is controlled by the accumulated washout optical depth. The rate $\Gamma$ is left as an arbitrary real function of time; no positivity or smoothness is built into this definition itself.
Downstream, the exponential survival kernel is written as $\exp(-\text{washout exponent})$, explicitly the genuine Boltzmann factor rather than a polynomial proxy such as $(1-\varphi^{-8})^k$.
proof idea
Pure definition: the value is the Lebesgue (Mathlib interval) integral of $\Gamma$ from $t'$ to $t_f$. No lemmas are applied; there is no proof obligation beyond the integral existing as a real number in the noncomputable setting.
why it matters
This is the optical-depth primitive for the baryogenesis staging lane. It is consumed by kernelBL, the exponential survival kernel $\exp(-\int_{t'}^{t_f}\Gamma_{\mathrm{wash}})$, and by the inequality that nonnegative accumulated washout implies survival weight at most one. A third use site appears in the source-off gate chain around $\dot\chi=0$.
The module's purpose is to keep the baryogenesis derivation from faking missing mechanism: washout must be the real Boltzmann integral, not an ad hoc polynomial in $\varphi$. This definition locks that convention before any claim about relic $B$ or freeze-out windows is stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.