KXcoeff
plain-language theorem explainer
Defines the CKN source coefficient K_X = ε/f_χ that multiplies the axion-like velocity χ̇ into the B−L chemical potential. Cosmologists tracking Steve baryogenesis cite it as the unique linear prefactor from the derivative coupling to the anomaly-free B−L current. The body is a one-line quotient of orientation sign by decay constant; no η_B is smuggled in.
Claim. The CKN source coefficient is the real number $K_X(\varepsilon,f_\chi)=\varepsilon/f_\chi$, where $\varepsilon$ is the eight-tick orientation sign and $f_\chi$ is the decay constant of the $\chi$ field.
background
This module stages honest, small targets for the Steve baryogenesis loop. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ charge forces vanishing final baryon number after equilibration.
Because $B-L$ is gauge-anomaly-free, the only portal for the $\chi$ field is the derivative coupling $(\partial_\mu\chi/f_\chi)\cdot J^\mu_{B-L}$. That coupling produces a chemical potential linear in the velocity, $\mu_{B-L}=\varepsilon,\dot\chi/f_\chi$. The prefactor $K_X=\varepsilon/f_\chi$ isolates the orientation sign $\varepsilon$ (from the eight-tick structure) and the decay-constant scale $f_\chi$.
Sibling quantities in the same file include the chemical potential constructor muBL, the equilibrium density nEqBL, and the sphaleron reprocessing factor that converts frozen $B-L$ into final $B$.
proof idea
Pure definitional abbreviation: the body is the real division $\varepsilon/f_\chi$. There is no tactic proof and no lemma application; downstream equalities unfold this definition and reduce by rfl or ring.
why it matters
Pins the unique linear source coefficient that feeds every later chemical-potential and yield identity in the staging file. Downstream theorems establish: definitional unfolding (KXcoeff_eq); non-vanishing when orientation and decay constant are nonzero (KXcoeff_ne_zero); oddness under orientation reversal, the structural origin of the sign that propagates to $\eta_B$ via a3SourceBL_odd / etaBFromYield_odd (KXcoeff_orient_odd); and the linear map $\mu_{B-L}=K_X,\dot\chi$ together with its source-off limit at $\dot\chi=0$ (muBL_from_KXcoeff, muBL_from_KXcoeff_zero).
In the Recognition framework the sign $\varepsilon$ is the eight-tick orientation (T7), so baryon asymmetry inherits a discrete geometric parity rather than an ad-hoc CP phase. The definition deliberately carries no $\eta_B$ input, keeping the staging loop from faking the missing mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.