SphaleronInEquilibrium_can_hold
plain-language theorem explainer
The sphaleron equilibrium predicate is satisfiable: there exist rate and Hubble functions and a closed time window on which Hubble stays strictly below the sphaleron rate. Cosmologists in the Sakharov/sphaleron obstruction lane cite this to show the equilibrium regime is non-empty. The proof is a constant-rate witness with Γ_sph ≡ 1 and H ≡ 1/2 on [0,1], checked by norm_num.
Claim. There exist real-valued functions $\Gamma_{\mathrm{sph}}, H : \mathbb{R} \to \mathbb{R}$ and times $t_0 \le t_f$ such that $H(t) < \Gamma_{\mathrm{sph}}(t)$ for every $t \in [t_0, t_f]$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
Sphaleron chemical equilibrium over a window is the genuine rate-vs-Hubble predicate: $H(t) < \Gamma_{\mathrm{sph}}(t)$ for all $t$ in $[t_0, t_f]$. It is never secretly True; the sibling result shows a configuration where Hubble overtakes a vanishing rate, so the predicate can fail.
The dual non-vacuity claim here is that the same predicate can hold. Physically this matches the early-universe regime $T \gg T_{\mathrm{EW}}$, where $\Gamma_{\mathrm{sph}} \sim \alpha_w^5 T^4$ greatly exceeds $H \sim T^2/M_{\mathrm{Pl}}$.
proof idea
Term-mode existence proof by explicit witness. Instantiate $\Gamma_{\mathrm{sph}}(t) = 1$ (constant fast rate), $H(t) = 1/2$ (constant Hubble), and the window $[0,1]$. The inequality $t_0 \le t_f$ is norm_num. For every $t$ in the window the pointwise comparison $1/2 < 1$ is again norm_num. No upstream lemmas beyond the definition of the equilibrium predicate are required.
why it matters
Together with the sibling failure witness, this pins the equilibrium predicate as a genuine physical regime rather than a vacuous tautology or impossibility. The module doc states the first invariant of the staging loop: if $B-L = 0$ and sphalerons equilibrate, then $B_{\mathrm{final}} = 0$. That obstruction (the physical wall) only bites if equilibrium can actually occur; this theorem supplies the existence half.
No downstream consumers are wired yet (used_by is empty). The result sits in the cosmology baryogenesis lane as scaffolding hygiene: loop-generated targets must not fake physics conditions as True. It does not itself compute a relic asymmetry or close the full Sakharov chain; it only certifies that the equilibrium gate is inhabitible.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.