physical_wall
plain-language theorem explainer
When electroweak sphalerons stay super-Hubble across a freeze-out window and the frozen B−L charge vanishes, the gated endpoint baryon number is forced to zero, independent of any primordial B+L. Cosmologists tracking the Sakharov/sphaleron obstruction cite this physical form of the wall. The proof is a one-line application of the abstract gated-wall lemma with the rate-vs-Hubble equilibrium predicate plugged in.
Claim. Let $\Gamma_{\mathrm{sph}}$ and $H$ be real-valued sphaleron-rate and Hubble functions on a time window $[t_0,t_f]$, and let $B_{\mathrm{prim}}$ and $B-L$ be real charges. If $H(t)<\Gamma_{\mathrm{sph}}(t)$ for every $t\in[t_0,t_f]$ (sphaleron chemical equilibrium) and $B-L=0$, then the equilibrium-gated final baryon number equals $0$, regardless of $B_{\mathrm{prim}}$.
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 the sourced $B-L$ is zero 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)$ throughout $[t_0,t_f]$. It is never secretly True; it fails whenever Hubble overtakes the rate. The gated endpoint baryon number is the conditional partition: in equilibrium the sphalerons drag $B$ to $(28/79)\cdot(B-L)$; out of equilibrium a primordial $B+L$ charge survives untouched.
The upstream wall lemma states the same zero conclusion for an arbitrary decidable equilibrium proposition. The present theorem specializes that gate to the physical rate-vs-Hubble predicate.
proof idea
One-line term wrapper. It applies the abstract gated-wall lemma, supplying classical decidability for the equilibrium proposition, the hypothesis that sphalerons are in equilibrium on the window, the two charge parameters, and the assumption $B-L=0$. The abstract lemma unfolds the gated definition, takes the equilibrium branch, and multiplies $(28/79)\cdot 0$ to zero. No further rate or Hubble algebra is needed here.
why it matters
This is the physical form of the B0 wall in the baryogenesis staging loop: the obstruction is keyed to a real rate-vs-Hubble condition rather than an opaque proposition. Downstream, the forcing form uses it to conclude that any model with a nonzero baryon relic at vanishing $B-L$ must have sphalerons fall out of equilibrium; that is the constraint every $B+L$-freeze-out claim must discharge. It also sits beside the lepton-side obstruction that multiplies $B-L$ by the complementary chemical factor. Within the Recognition cosmology lane this keeps the Sakharov/sphaleron story from faking equilibrium as a vacuous true hypothesis, matching the module rule that loop targets introduce no new axioms or fake physics conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.