BfinalGated_zero_of_chiDot_zero
plain-language theorem explainer
Under sphaleron equilibrium, a vanishing CP-odd source (chi-dot identically zero) forces the gated endpoint baryon number to zero. Cosmologists tracking the B0 obstruction in electroweak baryogenesis would cite this. The proof rewrites the gate to the banked relic map, then applies the source-off seam already proved for that map.
Claim. Fix an equilibrium proposition that holds, real profiles $a$, $\Gamma_w$, $c_\chi$, $T$, $\dot\chi$, and constants $K_x,t_0,t_f,B_{\mathrm{prim}}$. If $\dot\chi(t')=0$ for every $t'$, then the equilibrium-gated endpoint baryon number built from the Boltzmann relic $B-L$ charge equals $0$.
background
This module stages honest targets for the Steve baryogenesis loop. The first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, surviving baryon number is zero.
The gated endpoint $B_{\mathrm{final}}^{\mathrm{gated}}$ equals $(28/79)\cdot(B-L)$ when the equilibrium flag holds, and equals the primordial $B+L$ charge otherwise. The relic profile is the comoving Boltzmann integral $\int_{t_0}^{t_f} a^3 S_X(t'),e^{-\int_{t'}^{t_f}\Gamma_{\mathrm{wash}}},dt'$. Upstream, Bfinal_zero_of_chiDot_zero already shows that $\dot\chi\equiv 0$ kills the relic and hence the reprocessed baryon number. The companion rewrite BfinalGated_eq_relic says that under a true equilibrium hypothesis the gate collapses exactly to that banked map.
proof idea
Two-line term proof. First rewrite the gated endpoint via BfinalGated_eq_relic, using the hypothesis that the equilibrium proposition holds; the gate therefore equals the banked real-valued wall map applied to the relic profile. Then discharge the goal by Bfinal_zero_of_chiDot_zero, which already chains source-off through the relic integral into a vanishing reprocessed baryon number. No new analysis of the Boltzmann integral is performed here.
why it matters
Closes the source-off path through the equilibrium gate: with sphalerons in equilibrium and the CP-odd source off, frozen $B-L$ vanishes and the gated endpoint vanishes. This is the full chain from the Boltzmann relic into the B0 obstruction stated in the module doc (sphalerons conserve $B-L$; zero sourced $B-L$ plus equilibration implies zero surviving $B$).
It sits downstream of the banked seam Bfinal_zero_of_chiDot_zero and the coherence lemma BfinalGated_eq_relic, packaging both for callers that work with the gated interface rather than the bare relic map. No downstream consumers are wired yet (used_by is empty); the declaration is a staging target meant to keep the baryogenesis lane from faking the missing mechanism. It does not itself prove that sphalerons equilibrate or that $\dot\chi$ vanishes in nature; those remain separate physical inputs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.