obstruction_via_derivedFactor
plain-language theorem explainer
For any integer generation and Higgs-doublet counts, the sphaleron equilibrium reprocessing factor multiplies zero charge to zero in rationals. Cosmologists tracking the B−L zero-protection obstruction cite this when the equilibrium map uses the derived Harvey–Turner factor rather than a fixed SM rational. The proof is a one-line simplification of multiplication by zero.
Claim. For all integers $N$ and $n_H$, if $f(N,n_H)=\frac{8N+4n_H}{22N+13n_H}$ is the sphaleron reprocessing factor, then $f(N,n_H)\cdot 0=0$ in $\mathbb{Q}$. Equivalently, vanishing $B-L$ input is sent to vanishing reprocessed baryon charge for arbitrary gauge content.
background
This module stages honest theorem targets for the baryogenesis lane. The first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ charge is zero and sphalerons equilibrate, the surviving baryon number is zero.
The reprocessing factor is the chemical-potential balance map of Harvey and Turner (1990): anomaly plus Yukawa equilibrium plus hypercharge neutrality give $f(N,n_H)=(8N+4n_H)/(22N+13n_H)$. The Standard Model banked constant $28/79$ is the special case $N=3$, $n_H=1$. Here the factor is kept parametric in generation count $N$ and Higgs-doublet count $n_H$.
Downstream siblings package the same obstruction as $B_{\mathrm{final}}=f\cdot(B-L)$ and as an iff with nonvanishing anomaly numerator and denominator. This declaration isolates the pure algebraic zero map through that derived factor.
proof idea
Term-mode proof discharged by a single simp. In $\mathbb{Q}$, any rational times zero is zero, so the product of reprocessingFactorOf N nH with the literal $0$ reduces immediately. No case split on $N$ or $n_H$, and no appeal to positivity or nonvanishing of the anomaly coefficients, is required for this identity alone.
why it matters
It locks the zero-protection obstruction to the derived Harvey–Turner factor for arbitrary gauge content, not to one magic SM rational. The staging doc states the invariant: if sourced $B-L$ vanishes and sphalerons equilibrate, surviving $B$ vanishes. Nearby comments sharpen that $B_{\mathrm{final}}=f\cdot(B-L)$ vanishes iff $B-L$ vanishes when the anomaly numerator $8N+4n_H$ and denominator $22N+13n_H$ are nonzero; protection is tied to that nonvanishing numerator.
No downstream consumers are wired yet (used_by empty). The declaration still anchors the curated loop that forbids faking a baryogenesis mechanism when $B-L$ was never sourced. It sits beside siblings such as the $B_{\mathrm{final}}=0$ iff $B-L=0$ package and the fixed-factor obstruction lemmas, keeping the lane honest before any RS mass-ladder or eight-tick input is claimed to generate net $B$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.