KXcoeff_ne_zero
plain-language theorem explainer
Nonzero eight-tick orientation ε and nonzero decay constant f_χ force the CKN source coefficient K_X = ε/f_χ to be nonzero. Cosmologists in the Steve baryogenesis loop cite this to keep the B−L chemical-potential source alive. The proof is a one-line appeal to real-division nonvanishing.
Claim. If $\varepsilon \neq 0$ and $f_\chi \neq 0$, then the CKN source coefficient $K_X(\varepsilon,f_\chi) := \varepsilon/f_\chi$ satisfies $K_X(\varepsilon,f_\chi) \neq 0$.
background
The baryogenesis staging module holds small, honest theorem targets for the Steve baryogenesis derivation. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ charge vanishes and sphalerons equilibrate, the surviving baryon number is zero.
Because $B-L$ is gauge-anomaly-free, the only allowed $\chi$ source is the derivative coupling $(\partial_\mu\chi/f_\chi)\cdot J^\mu_{B-L}$. That yields the chemical potential $\mu_{B-L}=\varepsilon,\dot\chi/f_\chi$, packaged as the CKN coefficient $K_X=\varepsilon/f_\chi$: sign $\varepsilon$ from the eight-tick orientation, magnitude from the decay constant $f_\chi$. No $\eta_B$ input enters the definition.
Upstream orientation-reversal results show the source background is linear in $\dot\chi$, so flipping the rolling direction flips the integrated $B-L$ source; the linear yield-to-$\eta_B$ carrier then carries that sign flip to the baryon-to-photon ratio.
proof idea
One-line term proof. Unfolding the definition, $K_X$ is the real quotient $\varepsilon/f_\chi$. Mathlib's division-nonvanishing lemma applied to the two hypotheses $\varepsilon\neq 0$ and $f_\chi\neq 0$ immediately gives $K_X\neq 0$. No algebraic rearrangement beyond the definition is required.
why it matters
Without a nonzero $K_X$, the chemical potential $\mu_{B-L}$ collapses and the sphaleron zero-protection obstruction forces final baryon number (hence $\eta_B$) to zero. This lemma is the gate that keeps the CKN source channel open under the standing nonzero hypotheses on orientation and decay constant.
The sign of $\varepsilon$ is the eight-tick orientation (forcing-chain T7, period $2^3$). Nonvanishing of $K_X$ is therefore the structural prerequisite for the orientation-oddness chain: flipping the eight-tick orientation flips the source and then $\eta_B$. The module's charter is to prevent the baryogenesis lane from faking a missing mechanism; a silently zero coefficient would be exactly such a fake.
No downstream consumers are wired yet. The result sits as staging infrastructure for the Steve baryogenesis loop rather than a cited step inside a finished parent theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.