BfinalFromRelicBL_gt_third_of_pos
plain-language theorem explainer
For any positive frozen B−L charge, sphaleron reprocessing yields a baryon number strictly larger than one-third of that charge. Cosmologists tracking the quantitative obstruction in electroweak baryogenesis cite this bound. The proof rewrites the endpoint as multiplication by 28/79 and finishes by linear arithmetic.
Claim. Let $B-L \in \mathbb{R}$ with $B-L > 0$. Write $B_{\mathrm{final}}(B-L) := (28/79)\,(B-L)$ for the sphaleron-reprocessed baryon charge. Then $(B-L)/3 < B_{\mathrm{final}}(B-L)$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The governing invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ forces vanishing surviving baryon number after equilibration.
The real-valued endpoint BfinalFromRelicBL multiplies a frozen Boltzmann relic charge by the SM factor $28/79$, the same rational that appears on the discrete wall. Upstream, BfinalFromRelicBL_eq_factor records that identity by definitional equality, and reprocessing_conserves_BminusL closes the arithmetic content of $B-L$ conservation: the baryon and lepton equilibrium coefficients differ by exactly one, $(28/79)-(-51/79)=1$.
The companion magnitude obstruction already gives the strict contraction $|B_{\mathrm{final}}| < |B-L|$ whenever $B-L \neq 0$. The present lower bound supplies the matching floor.
proof idea
One-line term proof. Rewrite the goal via BfinalFromRelicBL_eq_factor, replacing the endpoint by $(28/79),\mathrm{BmL}$. The inequality becomes $\mathrm{BmL}/3 < (28/79),\mathrm{BmL}$. With the hypothesis $\mathrm{BmL}>0$, nlinarith discharges the comparison $28/79 > 1/3$ (equivalently $84 > 79$).
why it matters
Fills the quantitative survival lower bound advertised in the staging loop: together with the banked strict contraction, the reprocessed endpoint is sandwiched in $((B-L)/3,, B-L)$. The obstruction is therefore leaky but order-unity efficient; sphalerons cannot erase a positive frozen $B-L$ down to a negligible residue.
The factor $28/79$ is not free: it is forced by SM equilibrium counting and by the banked identity that baryon and lepton reprocessing coefficients differ by one. No downstream consumers are wired yet; the lemma is a ready citation point for any later bound that needs a uniform positive fraction of relic $B-L$ to survive freeze-out. It does not itself invoke the Recognition forcing chain (T0–T8) or the mass ladder; it is pure SM-arithmetic staging inside the cosmology lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.