a3SourceBL_odd
plain-language theorem explainer
Flipping the rolling velocity χ̇ ↦ −χ̇ pointwise negates the a³-weighted B−L source background at each time. Cosmologists tracking the sign of the frozen baryon yield under eight-tick orientation reversal cite this identity. The proof unfolds the linear chain μ → n_eq → S_X → a³S_X and closes by ring arithmetic.
Claim. For real functions $a$, $\Gamma_w$, $c_\chi$, $T$, $\dot\chi$ and reals $K_X$, $t$, the rolling B−L source background satisfies $$a(t)^3 S_X\bigl(t;\,\dot\chi\mapsto -\dot\chi\bigr) = -\,a(t)^3 S_X(t;\,\dot\chi),$$ where $S_X=\Gamma_w\,c_\chi\,T^2\,K_X\,\dot\chi$ is built from chemical potential $\mu_{B-L}=K_X\dot\chi$ and susceptibility $c_\chi T^2$.
background
The baryogenesis staging module holds small honest targets for the Steve baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ charge forces vanishing surviving baryon number after equilibration.
The rolling source background is the banked scalar $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)$. It factors through chemical potential $\mu_{B-L}=K_X\dot\chi$, susceptibility $c_\chi T^2$, equilibrium density $n_{B-L}^{\mathrm{eq}}=\chi\mu_{B-L}$, and source $S_X=\Gamma,n_{B-L}^{\mathrm{eq}}$. Because $\mu_{B-L}$ is linear in $\dot\chi$, the whole product is odd under $\dot\chi\mapsto-\dot\chi$.
The doc-comment records that the integral-level sign flip then follows from linearity of $\int$, with integrability still tagged OPEN.
proof idea
Term proof by definitional expansion. simp only unfolds the five-layer stack (a³-weighted source, source, equilibrium density, susceptibility, chemical potential), exposing the explicit monomial $a(t)^3\cdot\Gamma_w(t)\cdot c_\chi(t)\cdot T(t)^2\cdot K_X\cdot\dot\chi(t)$. Replacing $\dot\chi(t)$ by $-\dot\chi(t)$ multiplies that product by $-1$; ring discharges the identity. No external lemmas are invoked.
why it matters
Downstream, sign preservation for the observable baryon-to-photon ratio uses the fact that a positive entropy/photon multiplier maps a positive frozen yield to positive $\eta_B$; the companion orientation-reversal comment states that flipping the eight-tick orientation flips $Y_B$ via this oddness and the linear carrier carries the flip to $\eta_B$. The nonzero orientation coefficient $K_X=\varepsilon/f_\chi$ is likewise recorded as the structural origin of the sign that reaches $\eta_B$ through this identity. The invertible sphaleron reprocessing map pins the required $B-L$ source to an equality, and the required source flips under target reversal in matching fashion.
In the Recognition framework this is the algebraic seed of baryon-asymmetry sign under ledger orientation reversal, sitting inside the eight-tick octave (T7) cosmology lane. Integrability of the Boltzmann survival kernel remains OPEN, so the integral-level flip is not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.