sphaleronConstraint_zero_iff
plain-language theorem explainer
The SU(2)_L sphaleron equilibrium constraint 3μ_q + μ_l vanishes if and only if the lepton chemical potential sits on the line μ_l = −3 μ_q. Anyone tracking the first Harvey–Turner row or the B−L zero-protection obstruction in electroweak baryogenesis would cite this. The proof is a two-line algebraic iff after unfolding the linear definition.
Claim. For rational chemical potentials $\mu_q$ and $\mu_l$, the sphaleron equilibrium functional $3\mu_q + \mu_l$ equals zero if and only if $\mu_l = -3\mu_q$.
background
This module stages honest, small targets for the Recognition Science baryogenesis derivation. The governing invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
The sphaleron constraint is the linear functional $3\mu_q + \mu_l$ on quark and lepton chemical potentials (per generation). The factor $3$ is $N_{\mathrm{color}}$, not a fit parameter: the sphaleron operator $\prod(qqq,l)$ couples three colored quark doublets to one lepton doublet and drives $3\mu_q + \mu_l \to 0$ in equilibrium. Upstream documentation stresses that this is the first row of the Harvey–Turner system whose full solution yields the familiar $28/79$ conversion, and is not itself the banked affine map $B_{\mathrm{final}} = (28/79)(B-L)$.
The ambient RS time quantum is the tick $\tau_0 = 1$, with the eight-tick octave as the fundamental evolution period; orientation remarks in the file tie global sign reversal of the potentials to 8-tick orientation reversal of sourced charge.
proof idea
Term-mode proof by unfolding the definition $3\mu_q + \mu_l$. One direction: if the sum is zero, linarith recovers $\mu_l = -3\mu_q$. Converse: substitute $\mu_l = -3\mu_q$ and close by ring. No external lemmas beyond the definition and elementary rational arithmetic.
why it matters
Pins the equilibrium locus of the first Harvey–Turner sphaleron row as an exact algebraic line, so later staging results (reprocessing factor, washout exponent, $B_{\mathrm{final}}$ zero-protection) can treat “constraint saturated” as the concrete relation $\mu_l = -3\mu_q$ rather than a black-box predicate. That is the local content of the module’s sphaleron zero-protection obstruction: if sourced $B-L$ is zero and sphalerons equilibrate, surviving baryon number is forced to zero.
No downstream dependents are recorded yet; the theorem is infrastructure for the curated baryogenesis loop. It sits in the cosmology lane rather than the T0–T8 forcing chain, but inherits the eight-tick orientation language used when global sign reversal of the potentials is discussed. It does not claim the full $28/79$ conversion or a nonzero baryon asymmetry; it only characterizes when the first constraint row is satisfied.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.