source_exceeds_relic
plain-language theorem explainer
Any nonzero B−L charge, after electroweak sphaleron reprocessing by the SM factor 28/79, yields a strictly smaller equilibrium |B|. Cosmologists citing the Sakharov ledger obstruction use this as the usable floor form of zero-protection. The proof rewrites via the exact magnitude identity and finishes by rational arithmetic on 0 < 28/79 < 1.
Claim. Let $B-L \in \mathbb{Q}$. If the reprocessed charge $(28/79)\,(B-L)$ is nonzero, then $\bigl|(28/79)\,(B-L)\bigr| < |B-L|$. Equivalently, any nonzero equilibrium baryon asymmetry forces a strictly larger $|B-L|$ source.
background
This module stages honest theorem targets for the baryogenesis derivation loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with sphaleron equilibration leaves zero surviving baryon number.
The Standard Model reprocessing coefficient for three generations is the rational constant $28/79$: after equilibration one has $B = (28/79),(B-L)$. The upstream identity sphaleron_source_floor states the magnitude form $\bigl|(28/79),(B-L)\bigr| = (28/79),|B-L|$. Its doc-comment frames the contrapositive as a hard lower bound: producing equilibrium baryon size $b$ requires a $B-L$ source of size $(79/28),b$.
The present statement is that floor in comparison form. Because $0 < 28/79 < 1$, any nonzero source is strictly diluted in absolute value by reprocessing.
proof idea
First extract $B-L \neq 0$ from the hypothesis that the product with the reprocessing factor is nonzero (if $B-L=0$ the product vanishes). Rewrite the left-hand side by the upstream magnitude identity sphaleron_source_floor, replacing $\bigl|(28/79),(B-L)\bigr|$ with $(28/79),|B-L|$. Obtain $|B-L| > 0$ from the nonzero fact, then close with nlinarith using positivity of $|B-L|$ and the rational bounds on $28/79$. Pure arithmetic; no physics hypotheses beyond the banked factor.
why it matters
Closes the usable comparison form of the quantitative zero-protection floor (B0) in the baryogenesis staging lane. The module's purpose is to keep the Steve baryogenesis loop from faking the missing mechanism: sphalerons conserve $B-L$, and the SM factor $28/79$ is forced, never fitted. Together with sphaleron_source_floor and the reciprocal source identity (upstream $B-L$ must be exactly $(79/28),B$ to hit target $B$), this pins that every nonzero relic $|B|$ demands a strictly larger $|B-L|$ source.
No downstream consumers are wired yet (used_by empty); it sits as a ready lemma for freeze-out window and washout arguments in the same namespace. It does not itself derive the Jarlskog CP source or the EW phase-transition dynamics; those remain separate imports in the staging file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.