relicChargeProfile_zero_of_chiDot_zero
plain-language theorem explainer
If the rolling scalar is frozen (χ̇ ≡ 0) on the whole integration window, the comoving B−L relic charge vanishes. Cosmologists and RS baryogenesis auditors cite this as the source-off falsifier that chains the B2 source gate into the B4 Boltzmann integral. The proof kills the integrand pointwise via the banked source-off lemma, then invokes the zero integral.
Claim. Let $a,\Gamma_w,c_\chi,T,\dot\chi:\mathbb{R}\to\mathbb{R}$ and $K_X,t_0,t_f\in\mathbb{R}$. If $\dot\chi(t')=0$ for every $t'$, then the Boltzmann relic $\int_{t_0}^{t_f} a(t')^3 S_X(t')\,\exp\bigl(-\int_{t'}^{t_f}\Gamma_w\bigr)\,dt'$ equals $0$.
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$ forces vanishing final baryon number once sphalerons equilibrate.
The rolling B−L source background is $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)$, built from the banked scalar sourceBL (itself linear in the chemical-potential factor $\mu_{BL}=K_X\dot\chi$). The survival kernel is the genuine Boltzmann factor $\exp(-\int_{t'}^{t_f}\Gamma_{\mathrm{wash}})$, not a polynomial shortcut. The relic charge profile is their product integrated from $t_0$ to freeze-out $t_f$.
Upstream, the pointwise gate already holds: $\dot\chi(t)=0$ kills $a^3 S_X$ at that instant by routing through sourceBL_zero_of_chiDot_zero. The present result lifts that gate from a single time to the full integral.
proof idea
Unfold the relic definition to an interval integral of $a^3 S_X(t')\cdot K(t',t_f)$. For each $t'$, apply the pointwise source-off lemma (a3SourceBL_zero_of_chiDot_zero) with the global hypothesis $\dot\chi(t')=0$, then zero_mul to kill the product with the kernel. The resulting integrand is identically zero, so intervalIntegral.integral_zero finishes.
why it matters
This is the B3/B4 source-off gate: $\dot\chi\equiv 0$ on the window implies no relic. Downstream, Bfinal_zero_of_chiDot_zero rewrites the frozen $B-L$ to zero and pushes the vanishing through the sphaleron reprocessing map, giving the first seam closure that chains the Boltzmann relic into the obstruction. The same zero feeds orientation and yield bookkeeping (BfinalFromRelicBL_odd, etaBFromYield_uses_postAnnihilation).
In the staging philosophy, the result is a falsifier rather than a production formula: any claimed baryon asymmetry that survives a frozen rolling field is immediately ruled out. It does not yet touch RS landmarks such as the eight-tick octave or the $\phi$-ladder mass formula; it only polices the cosmological source term before those constants enter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.