etaBFromYield_zero_of_YB_zero
plain-language theorem explainer
A zero frozen baryon yield forces the observable baryon-to-photon ratio to vanish, for any entropy-to-photon multiplier R. Cosmologists tracking the baryogenesis chain cite this as the terminal source-off gate: no upstream charge means no measured asymmetry. The proof unfolds the linear carrier and closes by ring.
Claim. For every real multiplier $R$, the baryon-to-photon ratio built from frozen yield vanishes when the yield is zero: $\eta_B(R,0) = R \cdot 0 = 0$.
background
This module stages honest theorem targets for the Steve baryogenesis derivation. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ charge that equilibrates leaves zero surviving baryon number. The file exists to block fake mechanisms and missing physics conditions.
The carrier etaBFromYield converts a frozen comoving yield $Y_B = n_B/s$ into the observable $\eta_B = n_B/n_\gamma$ by the dimensionless factor $R = s/n_\gamma$, via the product $\eta_B = R \cdot Y_B$. Both arguments are formal; no magnitude is fixed here. Upstream, the source-off chain runs $\dot{\chi} = 0$ on the freeze-out window to $Y_{B-L} = 0$ and then to $Y_B = 0$; this lemma is the last arrow into $\eta_B = 0$.
proof idea
One-line term proof. Unfold the definition of the carrier (the product $R \cdot Y_B$), substitute $Y_B = 0$, and finish with ring, which reduces $R \cdot 0$ to $0$. No external lemmas are required beyond the definition.
why it matters
Closes the propagation endpoint of the baryogenesis source-off gate: vanishing chemical-potential drive implies vanishing frozen $B-L$ yield, hence vanishing $Y_B$, hence vanishing observable $\eta_B$. The module doc frames this as part of the sphaleron zero-protection obstruction, the first invariant that keeps the baryogenesis lane from inventing asymmetry. No downstream consumers are wired yet (used_by is empty); the lemma is a staging lock so later magnitude claims cannot manufacture charge from a zero yield. It does not touch the forcing chain T0–T8 or the J-cost identity directly; it is pure bookkeeping on the cosmology side of the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.