sphaleronReprocessingFactor_pos
plain-language theorem explainer
The Standard Model sphaleron reprocessing coefficient 28/79 is strictly positive. Cosmologists and RS baryogenesis auditors cite this to guarantee that equilibrium conversion B = (28/79)(B−L) is a genuine sign-preserving map, not the zero map. The proof is a one-line numerical check on the rational definition.
Claim. The Standard Model electroweak sphaleron reprocessing coefficient satisfies $0 < 28/79$. Equivalently, after sphaleron equilibration the map $(B-L)\mapsto B$ is a strictly positive rational multiple of the $B-L$ relic.
background
This module stages honest, small theorem targets for the RS baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ leaves vanishing baryon number after equilibration.
The reprocessing factor is the classical three-generation SM coefficient $$B = \frac{28}{79},(B-L)$$ after electroweak sphaleron equilibration. It is defined in-module as the rational $28/79$. Positivity of that coefficient is the minimal arithmetic fact that makes the conversion a real (sign-preserving) linear map rather than the zero map or a sign flip.
Downstream magnitude bounds and the nonzero-equilibrium statement all rewrite absolute values or nonzero products through this positivity fact.
proof idea
One-line term/tactic proof: unfold the definition sphaleronReprocessingFactor := 28/79 and discharge $0 < 28/79$ by norm_num. No lemmas beyond the definition and rational arithmetic are required.
why it matters
Positivity is the arithmetic hinge for three parent results in the same staging file. sphaleron_preserves_only_BminusL uses it to conclude that genuine $B\neq L$ yields nonzero equilibrium baryon number (the wall erases only the $B+L$ direction). The paired magnitude theorems sphaleron_cannot_amplify_magnitude and sphaleron_cannot_suppress_magnitude rewrite $|\mathrm{factor}\cdot(B-L)|$ via abs_of_pos, pinning the conversion to the closed $O(1)$ band
$$|B_{\mathrm{final}}|\in\bigl[|B-L|/3,,|B-L|/2\bigr].$$
Together they demote magnitude engineering off the B0 path: any suppression down to the observed $\eta_B$ must sit in the upstream $B-L$ yield, not in the $28/79$ factor. This keeps the baryogenesis lane from faking a missing mechanism, consistent with the module's staging charter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.