sphaleronReprocessingFactor
plain-language theorem explainer
The Standard Model electroweak sphaleron reprocessing coefficient is the rational 28/79: after equilibration with three generations and one Higgs doublet, the surviving baryon density is B = (28/79)(B−L). Cosmology and baryogenesis proofs cite it as the fixed SM conversion factor. It is a bare rational definition, not a derived theorem.
Claim. The Standard Model sphaleron reprocessing coefficient (three fermion generations, one Higgs doublet) is the rational number $28/79$. After electroweak sphaleron equilibration, the baryon number satisfies $B = \frac{28}{79}(B-L)$.
background
This module stages honest theorem targets for the baryogenesis derivation. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ leaves zero baryon number after equilibration.
In the Standard Model chemical-potential analysis, rapid $B+L$-violating sphaleron processes redistribute charge among quarks and leptons while holding $B-L$ fixed. For $N=3$ generations and $n_H=1$ Higgs doublet the equilibrium projection onto baryon number is the classical factor $28/79$; the complementary lepton coefficient is $-51/79$, and their difference is exactly 1.
The constant is the $N=3$, $n_H=1$ specialization of a more general reprocessing formula used elsewhere in the file. Downstream lemmas treat it as the banked SM value against which conservation, contraction, and obstruction statements are proved by arithmetic.
proof idea
Pure definition: the identifier is bound to the rational literal $28/79$ in $\mathbb{Q}$. No tactic proof, no upstream lemma application. Sibling theorems unfold this binding and discharge equalities by norm_num or ring.
why it matters
This constant is the arithmetic spine of the baryogenesis staging lane. It feeds reprocessing_conserves_BminusL (the identity $(28/79)-(-51/79)=1$), output_BminusL_eq_input (equilibrium output reproduces input $B-L$), and fixed_point_zero_iff (no iteration manufactures baryon number from vanishing $B-L$).
It also underwrites lepton_exceeds_baryon_reprocessing ($28/79 < 51/79$), sphaleron_cannot_amplify_magnitude, reprocessing_of_required (exact inversion of the source needed for a target relic), and the specialization theorem that the general formula at $(N,n_H)=(3,1)$ equals this banked value.
Within Recognition Science cosmology this is the SM-side conversion that turns a sourced $B-L$ (from the ledger/Sakharov staging) into a relic $B$. It does not itself derive the source; it locks the reprocessing step so the lane cannot fake equilibration or washout.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.