sphaleronReprocessingFactor_gt_third
plain-language theorem explainer
The Standard Model three-generation sphaleron reprocessing coefficient is strictly larger than one third. Cosmologists tracking post-equilibration baryon yield from a sourced B-L charge cite this bound. The proof rewrites the banked factor to the literal rational 28/79 and discharges the inequality by numerical normalization.
Claim. The Standard Model three-generation sphaleron reprocessing coefficient $c_{\mathrm{sph}}$ (the factor in $B = c_{\mathrm{sph}}\,(B-L)$ after electroweak equilibration) satisfies $\tfrac{1}{3} < c_{\mathrm{sph}}$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
The reprocessing coefficient is the Standard Model three-generation factor in $B = (28/79),(B-L)$ after equilibration. It is defined as the rational $28/79$ and pinned by an upstream equality theorem so that every downstream reference uses the same computed value.
Sibling facts already record positivity and the strict upper bound below one half. The present claim supplies the matching strict lower bound away from one third.
proof idea
One-line wrapper. Rewrite the banked coefficient via the upstream value theorem that equates it to $28/79$, then run norm_num to check $\tfrac{1}{3} < 28/79$ over the rationals.
why it matters
Doc-comment content: three-generation SM physics forces the reprocessing factor into the open interval $(1/3, 1/2)$, with $28/79 \approx 0.3544$. The lower bound is the new piece: conversion efficiency is bounded away from zero by a fixed rational, not merely shown positive.
In the staging module this keeps the baryogenesis lane from treating the sphaleron map as an unspecified positive scalar. Together with the existing upper bound below one half, it pins the efficiency window used when converting a sourced $B-L$ into a final baryon excess. No downstream consumers are wired yet; the lemma is a local honesty target for the Steve baryogenesis loop.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.