sphaleronReprocessingFactor_lt_half
plain-language theorem explainer
The Standard Model sphaleron reprocessing coefficient 28/79 is strictly less than one half. Cosmologists tracking electroweak baryon survival after sphaleron equilibration cite this when sandwiching final baryon charge between (B−L)/3 and B−L. The proof rewrites the banked factor to its literal rational and discharges the inequality by numeric normalization.
Claim. The Standard Model sphaleron reprocessing coefficient satisfies $\frac{28}{79} < \frac{1}{2}$, where that coefficient is the rational factor relating equilibrated baryon number to frozen $B-L$ via $B = \frac{28}{79}(B-L)$.
background
In the electroweak epoch, sphaleron processes redistribute baryon and lepton number while conserving $B-L$. For three Standard Model generations the equilibrium relation is $B = (28/79)(B-L)$. This staging module banks that coefficient as a single rational so zero-protection, washout, and relic-charge arguments share one pinned value.
The module's first invariant is the sphaleron zero-protection obstruction: if no $B-L$ is sourced and sphalerons equilibrate, the surviving baryon excess vanishes. Sibling facts already place the coefficient in $(0,1)$; the half-bound sharpens the survival window used in the leaky-but-order-unity sandwich.
Upstream, the value theorem identifies the opaque definition with the literal $28/79$, matching the SM reprocessing factor computed elsewhere in the Sakharov ledger path.
proof idea
Short tactic proof. Rewrite the left-hand side with the value theorem that pins the banked coefficient to $28/79$, then run norm_num to discharge the concrete rational inequality $28/79 < 1/2$.
why it matters
Supports the baryogenesis staging sandwich: with a lower survival bound of order $(B-L)/3$ and the strict contraction $|B_{\mathrm{final}}| < |B-L|$, the half-bound confirms reprocessing is leaky but order-unity efficient. No wired downstream users yet, but siblings on zero-protection, final-$B$ obstruction, positivity, and the unit upper bound sit in the same lane. Anchors the Steve baryogenesis derivation loop's honest obstruction targets without new axioms or fake physics conditions. Not a T0–T8 forcing step; it is SM-input cosmology infrastructure for the Sakharov-from-ledger path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.