BfinalFromRelicBL_abs_lt_of_ne
plain-language theorem explainer
For any nonzero frozen B−L charge, electroweak sphaleron reprocessing yields a strictly smaller baryon number in absolute value. The map is multiplication by the SM factor 28/79, a genuine contraction on ℝ\{0}. Cosmologists citing the quantitative Sakharov obstruction use this; the proof is a short absolute-value reduction plus 0 < 28/79 < 1.
Claim. Let $B-L \in \mathbb{R}$ with $B-L \neq 0$. Write $B_{\mathrm{final}}(B-L) := (28/79)\,(B-L)$ for the sphaleron-reprocessed baryon number. Then $|B_{\mathrm{final}}(B-L)| < |B-L|$.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The governing 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 real-valued reprocessing map is $B_{\mathrm{final}}(B-L) = (28/79),(B-L)$, the SM factor $28/79 = \mathrm{reprocessingFactorOf},3,1$ lifted from the rational wall to the field where the Boltzmann relic charge lives. An upstream identity records that this definition is literally multiplication by that factor.
The present statement is the strict magnitude form of the quantitative obstruction: reprocessing is a contraction on nonzero frozen $B-L$, not a mere relabeling of charge.
proof idea
Rewrite the reprocessed charge via the factor identity, so the claim is $|(28/79),(B-L)| < |B-L|$. Factor the absolute value as a product. The coefficient satisfies $0 < 28/79 < 1$ by norm_num, hence $|(28/79)| = 28/79$. Nonzeroness of $B-L$ gives $0 < |B-L|$. Finish by linear arithmetic on the product of a positive factor strictly less than one with a positive absolute value.
why it matters
Feeds the non-strict companion $|B_{\mathrm{final}}| \le |B-L|$, which covers the $B-L = 0$ wall by case split and quotes this theorem on the nonzero branch. Together they pin the module's first invariant: sphalerons never create net baryon charge from a frozen $B-L$ seed, and for nonzero seed they strictly shrink it.
In the staging loop this blocks fake mechanisms that would invent baryon number after freeze-out. It is the magnitude half of the quantitative obstruction ($0 < 28/79 < 1$), complementary to the zero-protection iff statement. Downstream baryogenesis claims that need a strict washout or contraction step cite this rather than the weak inequality alone.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.