obstruction_via_derivedFactor_iff
plain-language theorem explainer
For arbitrary generation count N and Higgs-doublet count nH, the sphaleron reprocessing factor times B−L vanishes if and only if B−L itself vanishes, once the anomaly numerator 8N+4nH and denominator 22N+13nH are nonzero. Cosmologists citing the content-independent zero-protection wall use this. The proof is a short rational algebra case-split on the zero-product law after unfolding the Harvey–Turner quotient.
Claim. Let $N,n_H\in\mathbb{Z}$ and $B-L\in\mathbb{Q}$. If $8N+4n_H\neq 0$ and $22N+13n_H\neq 0$, then $$\frac{8N+4n_H}{22N+13n_H}\cdot(B-L)=0 \iff B-L=0.$$
background
The staging module isolates honest theorem targets for the baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ is zero and sphalerons equilibrate, the surviving baryon number is zero.
The reprocessing factor is the Harvey–Turner (1990) chemical-potential balance quotient $$f(N,n_H)=\frac{8N+4n_H}{22N+13n_H},$$ obtained from sphaleron anomaly, Yukawa equilibrium, and hypercharge neutrality. The banked SM value $28/79$ is the special case $N=3$, $n_H=1$. Under equilibrium the final baryon density is proportional to $f\cdot(B-L)$.
The hypotheses simply demand that the anomaly numerator and denominator are nonzero as rationals, so $f$ is a well-defined nonzero rational rather than a magic constant.
proof idea
Unfold the definition of the reprocessing factor to the explicit quotient. Rewrite the product as a single fraction via div_mul_eq_mul_div, then apply div_eq_zero_iff. After push_cast, the zero condition becomes a three-way disjunction by mul_eq_zero: numerator vanishes, $B-L$ vanishes, or denominator vanishes. The forward direction discards the numerator and denominator cases by the two nonzero hypotheses (absurd), leaving $B-L=0$. The reverse direction injects $B-L=0$ into the middle disjunct. Pure rational algebra; no physics lemmas beyond the definition.
why it matters
This is the content-independent zero-protection lemma. It feeds nonzero_relic_forces_BminusL_general, whose doc-comment states the physical payload: for any SM-like content with nonvanishing anomaly numerator/denominator, a nonzero baryon relic at sphaleron equilibrium forces a nonzero $B-L$ source. That upgrades the banked SM-specific $28/79$ wall so "no choice of generation or Higgs count escapes it."
In the staging loop this is the FORCING direction that ejects the argument from sphaleron internals into the need for an upstream CP-odd $B-L$ source (the B2 out-of-orbit channel). It does not itself produce baryons; it certifies that any successful baryogenesis claim must source $B-L\neq 0$ before freeze-out, independent of gauge-content bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.