obstruction_Bfinal
plain-language theorem explainer
For any rational B−L charge, the SM sphaleron equilibrium map multiplies by 28/79 and yields zero if and only if B−L itself is zero. Cosmologists tracking the Steve baryogenesis staging loop cite this as the zero-protection obstruction: equilibrated sphalerons cannot manufacture a baryon relic from a vanishing B−L source. The proof is a short rational-arithmetic discharge (nonzero scalar cancellation over ℚ).
Claim. For every rational $B-L$, $\frac{28}{79}\,(B-L)=0$ if and only if $B-L=0$. Equivalently, the SM electroweak sphaleron reprocessing coefficient $\frac{28}{79}$ is nonzero, so the equilibrium baryon density vanishes precisely when the conserved $B-L$ charge vanishes.
background
The module stages honest, small targets for the Steve baryogenesis derivation. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ is zero and sphalerons equilibrate, the surviving baryon number is zero.
In the Standard Model with three generations and one Higgs doublet, the equilibrium reprocessing coefficient that converts a frozen $B-L$ into baryon number is the Harvey–Turner rational $28/79$. Downstream arithmetic pins that constant by anomaly coefficients: numerator $8\cdot 3+4\cdot 1=28$, denominator $22\cdot 3+13\cdot 1=79$. The lepton-axis partner is $-51/79$, and the two coefficients differ by exactly one, which is the arithmetic content of "$B-L$ is the conserved combination."
This lemma isolates the kernel statement alone: multiplication by that nonzero rational is injective at zero.
proof idea
Term-mode proof over $\mathbb{Q}$. A first cascade tries reflexivity, linear and nonlinear arithmetic, congruence, positivity, norm_num, ring/abel/field simplification, omega, simplification, aesop/tauto/decide, and a few intro/constructor wrappers with linarith or simp_all. The goal is pure field arithmetic: $\frac{28}{79}\neq 0$ in $\mathbb{Q}$, so the product vanishes exactly on the zero charge. No cosmology lemmas are invoked; the only named upstream hits are reflexivity facts pulled in by the tactic search.
why it matters
This is the kernel half of the sphaleron zero-protection obstruction advertised in the module header. It guarantees that the staged baryogenesis lane cannot fake a nonzero relic baryon number from a vanishing $B-L$ source once sphalerons equilibrate.
It is consumed when pinning the SM reprocessing factor to $28/79$ and when introducing the lepton-axis partner $-51/79$. The paired closure note stresses that coefficient difference-by-one is separate from this kernel statement: here one only needs that $28/79$ does not annihilate a nonzero charge. In the broader Recognition cosmology stack this keeps the baryogenesis loop honest until a genuine $B-L$ source (leptogenesis or otherwise) is supplied; it does not itself produce the asymmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.