outOfEquilibrium_falsifiable
plain-language theorem explainer
If a washout rate always strictly exceeds the Hubble expansion rate, no freeze-out instant exists at which the two rates equalize and thereafter washout falls below expansion. Cosmologists checking Sakharov's out-of-equilibrium condition in the baryogenesis staging lane would cite this. The proof is a direct irreflexivity contradiction after substituting the putative crossing equality.
Claim. Let $\Gamma_w, H : \mathbb{R} \to \mathbb{R}$ be rate functions and let $t_f \in \mathbb{R}$. If $H(t) < \Gamma_w(t)$ for every $t$, then it is false that both $\Gamma_w(t_f) = H(t_f)$ and $\Gamma_w(t) < H(t)$ for all $t > t_f$.
background
This module stages small, honest targets for the baryogenesis derivation loop. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ plus sphaleron equilibrium forces vanishing relic baryon number. Loop targets must not fake missing physics as True.
Sakharov's third condition requires a departure from thermal equilibrium. In rate language that is usually a freeze-out window: washout $\Gamma_w$ crosses the Hubble rate $H$ from above at some $t_f$, then stays below it. The parameters here are arbitrary real functions; the names only recall that cosmology convention.
The sole nontrivial upstream fact used is irreflexivity of strict order on the ambient reals (via the foundation lt_irrefl bridge): nothing is strictly less than itself.
proof idea
Term/tactic hybrid. Introduce the negated conjunction by rintro, keeping only the crossing equality $\Gamma_w(t_f)=H(t_f)$ and discarding the post-crossing clause. Specialize the standing hypothesis $H(t)<\Gamma_w(t)$ at $t=t_f$, rewrite the right-hand side by the crossing equality, and obtain $H(t_f)<H(t_f)$. Discharge by lt_irrefl.
why it matters
Inside Cosmology.BaryogenesisStaging this blocks a common sleight of hand: asserting an out-of-equilibrium freeze-out while simultaneously assuming washout remains super-Hubble at every time. The module's charter is to keep the Steve baryogenesis loop from inventing a missing mechanism; this lemma is a pure logical filter on that claim shape.
It sits beside siblings that encode sphaleron reprocessing, $B_{\mathrm{final}}=0$ iff $B-L=0$, washout exponents, and freeze-out windows. No downstream consumers are wired yet (used_by empty), so it is presently a guardrail rather than a lemma inside a finished abundance calculation. It does not itself invoke RS landmarks (T5 J-cost, $\phi$, eight-tick, $D=3$); it only polices the classical Sakharov rate condition that any later RS-native baryogenesis argument must still satisfy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.