b0_closure_certificate
plain-language theorem explainer
Algebraic certificate that the electroweak sphaleron reprocessing factor 28/79 is a non-zero-divisor on rational B−L: (28/79)·(B−L)=0 iff B−L=0. Anyone closing the sphaleron zero-protection obstruction in the baryogenesis staging loop cites this. Proof is a two-sided case split on the zero-product law in ℚ, using the explicit hypothesis that 28/79 ≠ 0.
Claim. For any rational charge $B-L$, assuming $\frac{28}{79}\neq 0$, one has $\frac{28}{79}\cdot(B-L)=0$ if and only if $B-L=0$.
background
The module stages honest theorem targets for the RS baryogenesis derivation. Its first invariant is the sphaleron zero-protection obstruction: electroweak sphalerons conserve $B-L$, so if the sourced $B-L$ vanishes and sphalerons equilibrate, the surviving baryon number is zero.
In the Standard Model the equilibrium solution of the Harvey–Turner chemical-potential system converts a frozen $B-L$ into a final baryon number by the rational factor $28/79$. Sibling definitions package that factor as a sphaleron reprocessing map and state the physical claim $B_{\mathrm{final}}=0\Leftrightarrow B-L=0$. The present lemma isolates the purely algebraic half of that claim over $\mathbb{Q}$.
Upstream, the proof uses the ring fact that $\mathbb{Q}$ (and the logic-integer models isomorphic to it) has no zero divisors: $a\cdot b=0$ forces $a=0$ or $b=0$, together with the simplification $a\cdot 0=0$.
proof idea
Bidirectional constructor on the biconditional.
Forward: from $\frac{28}{79}\cdot(B-L)=0$, apply mul_eq_zero to obtain a disjunction. The left disjunct $\frac{28}{79}=0$ is discharged by absurd against the explicit hypothesis; the right disjunct is exactly $B-L=0$.
Reverse: substitute $B-L=0$ and rewrite by mul_zero.
No cosmology lemmas are invoked; the argument is pure field arithmetic on $\mathbb{Q}$.
why it matters
Closes the algebraic gate on the sphaleron zero-protection obstruction that the module exists to protect. Without a non-zero-divisor certificate, the banked affine map $B_{\mathrm{final}}=\frac{28}{79}(B-L)$ could in principle send a nonzero $B-L$ to a vanishing baryon relic, faking a baryogenesis failure mode that is not physical.
Sibling targets (Bfinal_zero_iff_BminusL_zero, obstruction_Bfinal, sphaleron_equilibrium_zero_of_zero_BminusL) package the physical reading; this lemma is the rational kernel they rely on. It does not itself touch the forcing chain (T0–T8), the Recognition Composition Law, or the $\phi$-ladder mass formula, but it keeps the cosmology lane from introducing fake axioms or True-as-physics stubs, which is the module's stated purpose.
Currently unused by downstream declarations (used_by_count = 0); it is a staging certificate ready for the next baryogenesis composition step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.