BfinalGated_wall
plain-language theorem explainer
Under sphaleron equilibrium, a vanishing frozen B−L charge forces the endpoint baryon number to zero, no matter what primordial B+L was present. Cosmologists working the Sakharov/sphaleron obstruction cite this as the abstract wall. The proof unfolds the gated endpoint, takes the equilibrium branch, substitutes B−L = 0, and multiplies by zero.
Claim. Let $\mathrm{inEq}$ be a decidable proposition that holds, and let $B_{\mathrm{prim}}, B{-}L \in \mathbb{R}$ with $B{-}L = 0$. Then the gated endpoint baryon number equals zero: if sphalerons are in equilibrium the chemical partition gives $\frac{28}{79}\,(B{-}L)$, which vanishes when $B{-}L = 0$.
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, surviving baryon number is zero.
The gated endpoint $B_{\mathrm{final}}$ is defined by a boolean branch on equilibrium. In equilibrium, sphalerons enforce the Standard Model chemical partition and drag baryon number to $\frac{28}{79},(B{-}L)$. Out of equilibrium they freeze and impose no constraint, so a primordial $B{+}L$ charge survives untouched. The wall is exactly the equilibrium branch of that gate.
The classical factor $28/79$ is the SM sphaleron reprocessing coefficient relating equilibrium $B$ to frozen $B{-}L$. The companion escape (out-of-equilibrium branch) is documented immediately below this theorem: freeze-out can leave nonzero $B$ even when $B{-}L = 0$.
proof idea
One-line algebraic reduction on the definition. Unfold the gated endpoint, rewrite with if_pos using the hypothesis that equilibrium holds, substitute $B{-}L = 0$, and apply real multiplication by zero. No cosmology lemmas are needed; the result is pure definitional arithmetic on the equilibrium branch.
why it matters
This is the abstract form of the B0 obstruction that the staging module exists to protect: without a nonzero frozen $B{-}L$ (or an out-of-equilibrium escape), baryogenesis cannot succeed under equilibrated sphalerons. Downstream, physical_wall specializes the abstract equilibrium proposition to the rate-vs-Hubble predicate SphaleronInEquilibrium, so whenever sphalerons are super-Hubble across the window a vanishing frozen $B{-}L$ forces $B = 0$.
Together the pair separates the chemical-partition arithmetic from the physical rate condition, keeping the baryogenesis lane from faking a missing mechanism. The companion door (out-of-equilibrium survival of primordial $B{+}L$) is the explicit negation branch; this theorem is only the wall side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.