BfinalFromRelicBL_eq_factor
plain-language theorem explainer
The sphaleron-reprocessed final baryon charge on a real frozen B−L equals multiplication by the SM factor 28/79. Anyone proving magnitude bounds or survival windows after electroweak freeze-out cites this identity. The proof is pure definitional reflexivity: the endpoint map is defined as that scalar product.
Claim. For every real frozen $B-L$ charge $x$, the sphaleron-reprocessed baryon number equals $\frac{28}{79}\, x$.
background
This module stages honest theorem targets for the baryogenesis lane. 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 endpoint map takes a frozen Boltzmann-relic $B-L$ charge and returns the reprocessed baryon number. By definition it is scalar multiplication by the Standard Model factor $28/79$ (the same rational that appears as reprocessingFactorOf 3 1 on the integer wall), lifted to $\mathbb{R}$ where the relic charge profile lives.
That factor is strictly between $0$ and $1$, so reprocessing is a contraction on magnitude rather than a mere relabel of charge.
proof idea
One-line wrapper by rfl. The endpoint is defined as $(28/79)\cdot x$ on $\mathbb{R}$, so the stated equality is definitional and needs no algebraic lemmas.
why it matters
This identity is the algebraic hinge for the quantitative obstruction suite in the same module. The strict contraction $|B_{\mathrm{final}}| < |B-L|$ for nonzero frozen $B-L$ rewrites through it and then uses $0 < 28/79 < 1$. The non-creation bound $|B_{\mathrm{final}}| \le |B-L|$ (including the zero wall) cases on zero versus nonzero and routes the zero case through this equality. The survival lower bound $B-L/3 < B_{\mathrm{final}}$ for positive $B-L$ likewise rewrites and finishes by linear arithmetic, sandwiching the endpoint in $((B-L)/3, B-L)$.
In the staging narrative this keeps the sphaleron step honest: conversion is leaky but order-unity efficient, never a free source of baryon number when $B-L=0$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.