sourceBL
plain-language theorem explainer
Defines the instantaneous B-L source density as the product of a washout (or production) rate Γ and the equilibrium B-L charge density induced by a rolling scalar. Staging proofs for Sakharov baryogenesis cite it as the banked B2 scalar feeding the a³-weighted Boltzmann integrand. The body is a one-line product of Γ with nEqBL.
Claim. For real parameters $\Gamma$, $c_\chi$, $T$, $K_X$, and $\dot\chi$, the B-L source density is $S_{B-L}(\Gamma,c_\chi,T,K_X,\dot\chi)=\Gamma\,n_{B-L}^{\mathrm{eq}}(c_\chi,T,K_X,\dot\chi)$, where $n_{B-L}^{\mathrm{eq}}$ is the equilibrium charge density (susceptibility times chemical potential linear in $K_X\dot\chi$).
background
This module stages honest theorem targets for the Steve baryogenesis loop. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with equilibrated sphalerons forces vanishing final baryon number.
The equilibrium density $n_{B-L}^{\mathrm{eq}}$ is defined upstream as susceptibility times chemical potential: $n_{B-L}^{\mathrm{eq}}(c_\chi,T,K_X,\dot\chi)=\chi_{\mathrm{sus}}(c_\chi,T),\mu_{B-L}(K_X,\dot\chi)$, with $\mu_{B-L}$ linear in the rolling velocity $K_X\dot\chi$. The source multiplies that density by a rate $\Gamma$ (washout or production channel).
Sibling scaffolding includes freeze-out windows, washout exponents, and the sphaleron reprocessing factor that converts residual $B-L$ into final $B$.
proof idea
Pure definition: unfold to the product $\Gamma\cdot n_{B-L}^{\mathrm{eq}}(c_\chi,T,K_X,\dot\chi)$. No lemmas, no tactics. Downstream zero and oddness proofs unfold this def together with $n_{B-L}^{\mathrm{eq}}$, susceptibility, and $\mu_{B-L}$, then close by ring.
why it matters
Banked B2 scalar for the rolling $B-L$ source. Downstream, a3SourceBL multiplies it by $a(t)^3$ to form the Boltzmann integrand $a^3 S_X(t)=a(t)^3\cdot\Gamma_{\mathrm{wash}}(t)\cdot c_\chi(t)\cdot T(t)^2\cdot K_X\cdot\dot\chi(t)$. The gate sourceBL_zero_of_chiDot_zero records that a frozen background ($\dot\chi=0$) kills the source; that gate composes into relicChargeProfile_zero_of_chiDot_zero (B3/B4 source-off falsifier). Orientation reversal a3SourceBL_odd uses linearity of the source in $\dot\chi$ through $\mu_{B-L}=K_X\dot\chi$. Together these keep the baryogenesis lane from faking a nonzero relic when the rolling field is off.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.