etaBFromYield
plain-language theorem explainer
The base conversion from frozen baryon yield Y_B = n_B/s to the observed baryon-to-photon ratio η_B = n_B/n_γ is ordinary multiplication by the post-annihilation entropy-per-photon factor R = s/n_γ. Cosmologists in the baryogenesis staging lane cite it as the B6 carrier that cannot invent asymmetry. The body is a one-line product definition with no magnitude choice.
Claim. Define the observable baryon-to-photon ratio by $\eta_B(R,Y_B) := R \cdot Y_B$, where $Y_B = n_B/s$ is a frozen comoving yield and $R = s/n_\gamma$ is the dimensionless entropy-per-photon multiplier (intended at the post-$e^+e^-$ annihilation epoch).
background
The BaryogenesisStaging module holds small honest targets for the Steve baryogenesis loop. Its first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ with equilibrated sphalerons forces surviving baryon number to zero.
The upstream epoch tag entropyPhotonRatioPostAnnihilation records that $R = s/n_\gamma$ must be evaluated today, after $e^+e^-$ annihilation has dumped entropy into the photon bath. Before annihilation the ratio differs because $e^\pm$ are still relativistic; the tag forbids silently using the wrong multiplier. Numerically $R$ sits in the band $(7.0, 7.1)$.
Both $Y_B$ (charge per entropy) and $R$ (entropy per photon) are dimensionless formal arguments. Their product is the dimensionless observable $n_B/n_\gamma$. No magnitude is fixed at this layer.
proof idea
Pure definition: the carrier is the real product $R \cdot Y_B$. There is no lemma application, tactic script, or algebraic reduction beyond the equality that defines the map. Downstream lemmas unfold this definition and finish by ring or mul_pos.
why it matters
This is the B6 base carrier in the baryogenesis staging lane. It feeds the source-off gate (zero frozen yield gives zero observable), linearity in the yield (the map cannot manufacture asymmetry), sign preservation under positive $R$, and orientation reversal (oddness under $Y_B \mapsto -Y_B$, tying to eight-tick orientation flips upstream).
It also appears in the epoch-tag identity that the carrier consumes exactly the post-annihilation multiplier, and in the broader sphaleron magnitude-exclusion story: reprocessing cannot amplify a relic beyond a factor $1/2$, so the observable remains pinned to an $O(1)$ band of the frozen $B-L$ charge. The definition keeps the conversion layer transparent so the loop cannot fake a missing mechanism by hiding a nonlinear map.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.