relicChargeProfile
plain-language theorem explainer
Defines the Boltzmann relic: comoving B−L charge that survives washout from t₀ to freeze-out tf. It is the integral of the rolling a³-weighted B−L source against the genuine exponential survival kernel. Cosmology and baryogenesis proofs cite it as the B4 acceptance shape. The body is a direct integral of two banked staging defs.
Claim. Given scale factor $a$, washout rate $\Gamma_w$, coupling $c_\chi$, temperature $T$, rolling velocity $\dot\chi$, constant $K_X$, and times $t_0,t_f$, the relic charge is $\displaystyle\int_{t_0}^{t_f} a(t')^3 S_X(t')\,\exp\!\Bigl(-\int_{t'}^{t_f}\Gamma_w(s)\,ds\Bigr)\,dt'$, where $S_X$ is the banked B−L source built from $\Gamma_w$, $c_\chi$, $T^2$, $K_X$, and $\dot\chi$.
background
This module stages honest theorem targets for the Steve baryogenesis loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ plus sphaleron equilibration forces vanishing surviving baryon number. Loop targets must not fake missing mechanism with axioms or True physics conditions.
The integrand factors are banked earlier in the file. The rolling source background is $a^3 S_X(t)=a(t)^3\cdot\Gamma_w(t)\cdot c_\chi(t)\cdot T(t)^2\cdot K_X\cdot\dot\chi(t)$, built from the B2 scalar source. The survival kernel is $\exp(-\int_{t'}^{t_f}\Gamma_w)$, the genuine Boltzmann factor (not a polynomial $(1-\varphi^{-8})^k$). A gate lemma already shows that $\dot\chi=0$ kills the pointwise source.
The definition packages those pieces into the standard comoving relic integral from $t_0$ to freeze-out $t_f$: source times exponential survival under the integral. That is the B4 acceptance shape used by the obstruction chain.
proof idea
Definition, not a proof. The body is the interval integral of the product of the banked rolling source background a3SourceBL and the exponential survival kernel kernelBL. No tactics; the mathematical content is exactly that Boltzmann convolution.
why it matters
This is the B4 carrier that the baryogenesis staging loop actually integrates against. Downstream, the source-off gate relicChargeProfile_zero_of_chiDot_zero shows that $\dot\chi\equiv 0$ on the window forces the relic to vanish, composing B2 into B4. That zero then propagates through the sphaleron wall: Bfinal_zero_of_chiDot_zero is the seam closure that chains the Boltzmann relic into the obstruction, and BfinalGated_zero_of_chiDot_zero extends it through the equilibrium gate. The dilution-invariant yield statement baryonYield_zero_of_chiDot_zero rides the same carrier. The module's sphaleron teeth (sphaleron_preserves_only_BminusL) sit beside this: sphalerons erase $B+L$ only, so a zero $B-L$ relic is fatal for baryon number. In the Recognition staging program this keeps the baryogenesis lane from faking a CP-odd source: no rolling $\dot\chi$, no relic, no $Y_B$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.