BfinalFromRelicBL_abs_le
plain-language theorem explainer
Sphaleron reprocessing never amplifies frozen B−L charge: the absolute final baryon number is at most the absolute input |B−L|, including equality at the zero wall. Cosmologists tracking Sakharov staging and washout bounds cite this as the non-strict magnitude envelope around the 28/79 factor. The proof splits on vanishing versus nonzero B−L, using the factor identity at zero and the strict contraction lemma off zero.
Claim. For every real frozen $B-L$ charge $X$, if $B_{\mathrm{final}}(X) := (28/79)\,X$ is the sphaleron-reprocessed baryon number, then $|B_{\mathrm{final}}(X)| \le |X|$. Equality holds when $X = 0$.
background
This module stages honest, small targets for the baryogenesis derivation loop. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with equilibrated sphalerons forces vanishing surviving baryon number.
The map BfinalFromRelicBL lifts the SM three-generation reprocessing factor $28/79$ to real frozen $B-L$ from the Boltzmann relic: $B_{\mathrm{final}}(X) = (28/79) X$. Upstream, BfinalFromRelicBL_eq_factor records that identity by definition, and BfinalFromRelicBL_abs_lt_of_ne gives the quantitative obstruction: for $X \ne 0$, $|B_{\mathrm{final}}(X)| < |X|$ because $0 < 28/79 < 1$.
The present statement closes the envelope by allowing equality at the wall $X = 0$, matching the doc-comment claim that conversion never creates charge.
proof idea
Case split on whether the frozen charge vanishes.
If $X = 0$, rewrite via BfinalFromRelicBL_eq_factor and simplify: both sides are zero, so $|B_{\mathrm{final}}| \le |X|$ holds with equality.
If $X \ne 0$, apply BfinalFromRelicBL_abs_lt_of_ne to obtain the strict inequality $|B_{\mathrm{final}}(X)| < |X|$, then weaken with le_of_lt.
No new arithmetic: the contraction content lives entirely in the strict lemma ($0 < 28/79 < 1$ via norm_num).
why it matters
In the Sakharov-from-ledger staging lane, this is the non-strict magnitude companion to the strict contraction and the zero-protection wall. Together they pin that sphaleron reprocessing is a genuine contraction of charge magnitude, never a source: $|B_{\mathrm{final}}| \le |B-L|$ always, with equality only when the input vanishes.
The factor $28/79$ is the SM three-generation content (reprocessing factor of three generations, one Higgs), forced into $(1/3, 1/2)$. Downstream consumers of relic-to-baryon maps can quote this bound without casework on the wall. No used_by edges are recorded yet; the lemma is a staging closure for the magnitude half of the obstruction package rather than a leaf of a larger proved chain.
It does not itself derive the Sakharov conditions or compute a numerical $\eta_B$; it only seals the absolute-value envelope of the reprocessing map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.