obstruction_Lepton
plain-language theorem explainer
Multiplying a rational B−L charge by the SM lepton reprocessing coefficient −51/79 yields zero exactly when B−L itself vanishes. Cosmologists tracking sphaleron-equilibrated lepton relics cite this as the lepton-side twin of the baryon zero-protection obstruction. The proof is two-direction rational arithmetic: the coefficient is nonzero by numerical check, so the product vanishes iff the charge does.
Claim. For every rational charge $B-L$, $\bigl(-\frac{51}{79}\bigr)\,(B-L)=0$ if and only if $B-L=0$.
background
This module stages honest, small theorem targets for the baryogenesis derivation loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ together with sphaleron equilibration forces the surviving baryon number to zero. Loop targets must not fake physics conditions as True or introduce axioms.
In the Standard Model with three generations, chemical equilibrium among sphalerons and Yukawa interactions fixes the frozen charges in terms of the conserved $B-L$. The classical conversion factors are $B=\frac{28}{79}(B-L)$ and $L=-\frac{51}{79}(B-L)$. The coefficient $-\frac{51}{79}$ is therefore the lepton-sector reprocessing weight: it maps a frozen $B-L$ into the equilibrated lepton charge.
Upstream, physical_wall already packages the baryon-side gate: whenever sphalerons are super-Hubble across a window and frozen $B-L$ vanishes, the gated final baryon number is zero. A companion non-vacuity result shows the equilibrium predicate is not secretly always true, so the wall applies to a genuine physical regime.
proof idea
Bidirectional constructor on the rational equality.
Forward: assume $\bigl(-\frac{51}{79}\bigr),(B-L)=0$. A norm_num check gives $-\frac{51}{79}\neq 0$. If $B-L\neq 0$, then mul_ne_zero would make the product nonzero, contradicting the hypothesis; hence $B-L=0$.
Reverse: substitute $B-L=0$ and apply mul_zero.
No cosmology lemmas are invoked; the argument is pure field arithmetic over $\mathbb{Q}$.
why it matters
The module's stated purpose is to keep the baryogenesis lane from faking the missing mechanism. The baryon-side obstruction (vanishing $B-L$ plus equilibration forces $B_{\mathrm{final}}=0$) is already packaged in physical_wall and the sibling obstruction_Bfinal / Bfinal_zero_iff_BminusL_zero cluster. This declaration supplies the matching lepton-side algebraic gate: the SM weight $-\frac{51}{79}$ is a unit in $\mathbb{Q}^{\times}$, so it cannot manufacture a nonzero lepton relic from a zero $B-L$ seed, nor hide a nonzero seed behind a zero product.
That closes a bookkeeping hole in the Sakharov-from-ledger staging: both $B$ and $L$ channels inherit the same zero-protection from conserved $B-L$. No downstream consumer is wired yet (used_by is empty); the lemma is staged for later relic-charge and washout identities that quote the lepton conversion factor explicitly. Within Recognition Cosmology it is scaffolding arithmetic, not a new forcing-chain step (T0–T8), but it keeps the sphaleron ledger honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.