SphaleronInEquilibrium
plain-language theorem explainer
Sphaleron chemical equilibrium on a closed time window means the B-violating sphaleron rate strictly exceeds the Hubble expansion rate at every instant of that window. Cosmologists citing the B−L zero-protection obstruction use this as the physical gate that forces vanishing final baryon number when frozen B−L is zero. The body is a plain universal quantification over the interval, not a derived theorem.
Claim. Given real-valued functions $\Gamma_{\mathrm{sph}}$ (sphaleron rate) and $H$ (Hubble rate) and times $t_0,t_f$, sphalerons are in chemical equilibrium on $[t_0,t_f]$ when $H(t)<\Gamma_{\mathrm{sph}}(t)$ holds for every $t$ with $t_0\le t\le t_f$.
background
The BaryogenesisStaging module holds small, honest targets for the baryogenesis derivation loop. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ charge is zero and sphalerons equilibrate, the surviving baryon number is zero. Loop targets must not fake physics conditions as True.
This definition is the concrete rate-versus-Hubble predicate used as that equilibrium gate. The parameter $H$ is the cosmological expansion rate as a function of time, not the Recognition cost reparametrization $H(x)=J(x)+1$. The comparison $\Gamma_{\mathrm{sph}}>H$ is the standard chemical-equilibrium criterion for B-violating sphaleron processes across a freeze-out window $[t_0,t_f]$.
proof idea
Definitional, not a proof. The body is the single quantified inequality $\forall t\in[t_0,t_f],, H(t)<\Gamma_{\mathrm{sph}}(t)$. No lemmas are applied; the Prop is exactly that statement.
why it matters
This predicate is the physical key for the staging obstruction chain. physical_wall uses it directly: whenever sphalerons are super-Hubble across the window and frozen $B-L=0$, the gated final baryon number is zero, independent of any primordial $B+L$. physical_escape is the negation branch: if Hubble overtakes the rate somewhere, the primordial charge survives. The forcing form nonzero_relic_at_zero_BmL_forces_offEquilibrium states that any model with nonzero relic baryon number at $B-L=0$ cannot keep this equilibrium predicate. BfinalGated_zero_of_chiDot_zero threads the same gate when the CP-odd source is off.
Non-vacuity is discharged by sibling theorems: the predicate can fail (Hubble above a vanishing rate) and can hold (constant super-Hubble rate), so it is neither secretly True nor secretly False. That honesty is the module's stated purpose for the baryogenesis lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.