physical_escape
plain-language theorem explainer
If sphalerons fall out of equilibrium anywhere in the freeze-out window (Hubble overtakes the B-violating rate), the gated endpoint baryon number equals the primordial charge, not the reprocessed (28/79)(B−L). Cosmologists citing B+L freeze-out as the escape from the Sakharov wall use this. The proof is a one-line application of the generic out-of-equilibrium gate lemma.
Claim. Let $\Gamma_{\mathrm{sph}}$ and $H$ be real-valued rate and Hubble functions on a time window $[t_0,t_f]$, and let $B_{\mathrm{prim}}$, $B{-}L\in\mathbb{R}$. If it is not the case that $H(t)<\Gamma_{\mathrm{sph}}(t)$ for all $t\in[t_0,t_f]$, then the equilibrium-gated final baryon number equals $B_{\mathrm{prim}}$ (rather than $\frac{28}{79}(B{-}L)$).
background
This module stages honest theorem targets for the baryogenesis derivation loop. The first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B{-}L$, so if sourced $B{-}L$ vanishes and sphalerons equilibrate, surviving baryon number is zero.
Sphaleron chemical equilibrium over a window is the genuine rate-vs-Hubble predicate: $\forall t\in[t_0,t_f],, H(t)<\Gamma_{\mathrm{sph}}(t)$. It fails whenever Hubble overtakes the rate; it is never secretly True.
The gated endpoint baryon number branches on that predicate. In equilibrium, sphalerons enforce the chemical partition and drag $B$ to $\frac{28}{79}(B{-}L)$. Out of equilibrium they freeze and impose no constraint, so a primordial $B{+}L$ charge survives untouched. That is the conditional content of the $B=0$ wall.
proof idea
One-line wrapper. Instantiate the generic escape lemma BfinalGated_escape at the concrete equilibrium proposition SphaleronInEquilibrium Γsph H t₀ tf, feeding the hypothesis that this proposition fails. That lemma unfolds the gated definition and rewrites by if_neg, yielding equality with the primordial charge. No rate integrals or SM input enter here.
why it matters
This is the physical door of the staging file: the negation branch of the sphaleron gate, now keyed to a real $\neg(H<\Gamma)$ condition rather than an opaque proposition. The module doc frames the wall as the first invariant preventing the baryogenesis lane from faking a missing mechanism. Downstream of the generic escape lemma, this specializes the only door through which a nonzero relic can survive when $B{-}L=0$: sphalerons must fall out of equilibrium somewhere in the window (B+L freeze-out).
The forcing form recorded just below the proof states the operational obstruction every B+L-freeze-out claim must discharge: a model cannot keep $H<\Gamma$ across the window, assert $B{-}L=0$, and still report a nonzero baryon relic. No used_by edges are recorded yet; the declaration is a leaf citation target for later EW-phase-transition and sphaleron-rate wiring.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.