sphaleronReprocessingFactor_lt_one
plain-language theorem explainer
The Standard Model sphaleron reprocessing coefficient equals 28/79 and is strictly less than one. Cosmology and baryogenesis arguments that convert a frozen B−L relic into net baryon number after electroweak equilibration cite this bound. The proof is a one-line numerical check on the rational definition.
Claim. The Standard Model sphaleron reprocessing coefficient $28/79$ satisfies $28/79 < 1$.
background
In the Standard Model with three generations, electroweak sphalerons drive the system toward chemical equilibrium while conserving $B-L$. The equilibrium relation is $B = (28/79),(B-L)$: only a fixed fraction of any preexisting $B-L$ charge is reprocessed into baryon number, and the complementary fraction is carried by lepton number.
This module stages honest, small theorem targets for the baryogenesis derivation loop. Its first invariant is the sphaleron zero-protection obstruction: if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon excess is zero. The reprocessing factor is the rational coefficient in that conversion law.
Upstream, sphaleronReprocessingFactor is defined exactly as the rational $28/79$, matching the textbook three-generation SM value.
proof idea
One-line tactic proof. Unfold the definition of the reprocessing factor to the rational $28/79$, then apply norm_num to discharge $28/79 < 1$ by exact rational arithmetic. No lemmas beyond the definition are required.
why it matters
The strict inequality records that sphalerons reprocess a $B-L$ relic rather than copy it unchanged. Together with the sibling positivity statement and the zero-protection theorems (sphaleron_equilibrium_zero_of_zero_BminusL, Bfinal_zero_iff_BminusL_zero), it keeps the baryogenesis lane from treating the conversion factor as identity or as a free parameter.
No downstream consumers are wired yet; the declaration is a staging guardrail inside the Steve baryogenesis loop. It sits under the Sakharov-from-ledger and sphaleron-rate imports and supports later relic-charge and washout constructions that fold source terms against survival kernels. It does not itself invoke the Recognition forcing chain (T0–T8) or the J-cost identity; it is SM bookkeeping needed before RS-specific source mechanisms can be attached.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.