reprocessing_conserves_BminusL
plain-language theorem explainer
The baryon and lepton sphaleron reprocessing coefficients differ by exactly one: 28/79 minus (-51/79) equals 1. Anyone citing B-L conservation under electroweak equilibration needs this cross-axis identity. The proof rewrites the baryon factor to its banked rational, unfolds the lepton factor, and closes by numerical normalization over Q.
Claim. The Standard Model sphaleron reprocessing coefficient for baryon number and the paired lepton-axis coefficient satisfy $\frac{28}{79}-\left(-\frac{51}{79}\right)=1$. Equivalently, if after equilibration $B=\frac{28}{79}(B-L)$ and $L=-\frac{51}{79}(B-L)$, then the difference of the two coefficients is identically one.
background
In the baryogenesis staging module, electroweak sphalerons redistribute baryon and lepton number while conserving $B-L$. The file holds small honest theorem targets so the derivation loop cannot fake a missing mechanism. The first invariant is the sphaleron zero-protection obstruction: if sourced $B-L$ is zero and sphalerons equilibrate, surviving baryon number is zero.
The baryon-axis coefficient is the standard three-generation SM factor $B=(28/79)(B-L)$. Its lepton partner is defined by $L=(-51/79)(B-L)$. An upstream value lemma pins the opaque banked baryon factor to the literal rational $28/79$, so obstruction and contraction statements refer to the same computed value.
This identity is the arithmetic content of "$B-L$ is the conserved combination." It is neither the kernel obstruction nor the relic contraction bound; those lemmas assume it.
proof idea
Short term-mode proof in three steps. Rewrite the baryon reprocessing factor via the upstream value lemma that equates it to $28/79$. Unfold the lepton factor definition $-51/79$. Close with norm_num, which evaluates $(28/79)-(-51/79)=1$ over the rationals.
why it matters
Feeds three parents in the same module. First, the fixed-point theorem that equilibrium output charges reproduce input $B-L$ for every source value: sphalerons drive $B$ and $L$ but leave $B-L$ invariant, the precise sense in which they cannot be a $B-L$ source. Second, the lepton-factor value theorem, which derives $-51/79$ from this identity rather than positing it. Third, the real-valued survival lower bound that sandwiches reprocessed baryon charge in $((B-L)/3,B-L)$ for positive frozen $B-L$.
In the Recognition cosmology lane this is the cross-axis arithmetic that makes the sphaleron zero-protection obstruction honest: without coefficient difference one, $B-L$ conservation would be a slogan rather than a proved relation between the two axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.