muBL_from_KXcoeff_zero
plain-language theorem explainer
When the CKN source coefficient is K_X = ε/f_χ and the axion-like velocity vanishes, the B−L chemical potential is exactly zero. Cosmologists working the Steve baryogenesis staging loop cite this as the coefficient-level source-off limit. The proof rewrites via the linear identity μ = ε·χ̇/f_χ and closes by ring.
Claim. For all real $\varepsilon$ and $f_\chi$, if $K_X = \varepsilon/f_\chi$, then $\mu_{B-L}(K_X,\,0) = 0$. Equivalently, the chemical potential sourced by the derivative coupling $(\partial_\mu\chi/f_\chi)\cdot J^\mu_{B-L}$ vanishes whenever $\dot\chi = 0$.
background
This module stages honest, small targets for the Steve baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ charge plus sphaleron equilibration forces surviving baryon number to zero.
The CKN source coefficient is $K_X = \varepsilon/f_\chi$: sign $\varepsilon$ from eight-tick orientation, magnitude from the decay constant $f_\chi$. Because $B-L$ is gauge-anomaly-free, the only $\chi$ source is the derivative coupling $(\partial_\mu\chi/f_\chi)\cdot J^\mu_{B-L}$, which yields $\mu_{B-L} = \varepsilon,\dot\chi/f_\chi$. The chemical potential itself is the product $\mu_{B-L}(K_X,\dot\chi) := K_X\cdot\dot\chi$.
Upstream, muBL_from_KXcoeff already records the linear identity $\mu_{B-L} = \varepsilon,\dot\chi/f_\chi$ and notes that the source is off at $\dot\chi = 0$. The present statement isolates that source-off limit at the coefficient level.
proof idea
One-line term proof. Rewrite with the upstream identity muBL_from_KXcoeff, which expands $\mu_{B-L}(K_X(\varepsilon,f_\chi),\dot\chi)$ to $\varepsilon,\dot\chi/f_\chi$. Specialize to $\dot\chi = 0$ and finish by ring, which reduces $\varepsilon\cdot 0/f_\chi$ to $0$.
why it matters
Inside the baryogenesis staging loop this pins the coefficient-level source-off fact that feeds the sphaleron zero-protection obstruction: if sourced $B-L$ vanishes and sphalerons equilibrate, the relic baryon number is zero. The eight-tick orientation enters only as the sign $\varepsilon$ in $K_X$; no $\eta_B$ input is smuggled in.
No downstream consumers are wired yet (used_by is empty). The declaration sits as a clean algebraic guard so later staging targets (freeze-out windows, washout exponents, $B_{\mathrm{final}}$ obstruction lemmas) can invoke a proved source-off limit rather than an ad-hoc hypothesis. It does not close the full Sakharov or sphaleron-rate story; it only locks the $\dot\chi = 0$ corner of the CKN chemical-potential map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.