a3SourceBL
plain-language theorem explainer
Defines the comoving B-L source density a³S_X(t) as the cube of the scale factor times the banked pointwise source Γ_wash c_χ T² K_X χ̇. Cosmologists staging the Steve baryogenesis Boltzmann integral cite it as the integrand prefactor. The body is a one-line product of a(t)³ with sourceBL evaluated on the time slices.
Claim. For real-valued backgrounds $a$, $\Gamma_w$, $c_\chi$, $T$, $\dot\chi$ and constant $K_X$, the rolling B-L source background at time $t$ is $$a^3 S_X(t) := a(t)^3 \, \Gamma_w(t)\, n_{\mathrm{eq}}^{B-L}\bigl(c_\chi(t), T(t), K_X, \dot\chi(t)\),$$ equivalently $a(t)^3\cdot\Gamma_w(t)\cdot c_\chi(t)\cdot T(t)^2\cdot K_X\cdot\dot\chi(t)$ once the equilibrium density is expanded.
background
This module stages honest, small 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 banked scalar sourceBL is the pointwise source $\Gamma, n_{\mathrm{eq}}^{B-L}(c_\chi,T,K_X,\dot\chi)$, itself built from chemical potential $\mu_{B-L}=K_X\dot\chi$ and susceptibility. Multiplying by $a(t)^3$ converts that local rate into the comoving density that enters a Boltzmann integral.
Downstream, the relic profile integrates $a^3 S_X(t')$ against a genuine exponential washout kernel $\exp(-\int_{t'}^{t_f}\Gamma_{\mathrm{wash}})$, not a polynomial survival factor. The definition therefore sits between the B2 source gate and the B4 acceptance shape of the relic.
proof idea
Pure definitional abbreviation: evaluate the five background functions at $t$, feed those scalars (plus $K_X$) into sourceBL, and multiply by $(a,t)^3$. No lemmas, no tactics; the body is a single product. Downstream oddness and source-off lemmas unfold this def and reduce through linearity of sourceBL in $\dot\chi$.
why it matters
Supplies the integrand prefactor for relicChargeProfile, the comoving $B-L$ charge surviving to freeze-out. Parent lemmas a3SourceBL_odd and a3SourceBL_zero_of_chiDot_zero establish orientation reversal under $\dot\chi\mapsto -\dot\chi$ and the pointwise source-off gate $\dot\chi(t)=0\Rightarrow a^3 S_X(t)=0$. Those feed the integral-level falsifier relicChargeProfile_zero_of_chiDot_zero: frozen rolling field on the whole window kills the relic. In the staging loop this keeps the baryogenesis lane from faking a nonzero $B-L$ source when the rolling background is off, consistent with the module's sphaleron zero-protection obstruction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.