KXcoeff_eq

The module stages honest theorem targets for the Steve baryogenesis derivation. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with equilibrated sphalerons forces vanishing final baryon number.

$K_X$ is the prefactor in the chemical-potential relation $\mu_{B-L}=\varepsilon,\dot\chi/f_\chi$ that arises from the derivative coupling $(\partial_\mu\chi/f_\chi)\cdot J^\mu_{B-L}$. Because $B-L$ is gauge-anomaly-free, that coupling is the only $\chi$ source. The sign $\varepsilon$ is the eight-tick orientation; the magnitude is set by the decay constant $f_\chi$. No baryon asymmetry $\eta_B$ is fed in by hand.

The definition is simply $K_X(\varepsilon,f_\chi):=\varepsilon/f_\chi$. This theorem records that equality as a named fact for downstream rewriting.

One-line term proof by rfl: the left-hand side is definitionally $\varepsilon/f_\chi$, so the equality holds by reduction of the definition of KXcoeff.

Inside the baryogenesis staging lane this pins the CKN source coefficient before any freeze-out or washout algebra runs. The eight-tick orientation that supplies $\varepsilon$ is the same T7 octave structure used elsewhere in the forcing chain; keeping $K_X$ free of $\eta_B$ input prevents the lane from smuggling the observed asymmetry into the source term. No downstream consumers are wired yet (used_by is empty), so the lemma is presently a staging anchor rather than a load-bearing step in a finished relic-density theorem.