etaBFromYield_pos_of_pos
plain-language theorem explainer
Positive entropy-to-photon ratio and positive frozen baryon yield give a strictly positive baryon-to-photon ratio under the linear carrier η_B = R·Y_B. Cosmologists tracking the sign of the observed asymmetry through freeze-out cite this. The proof is a one-line unfold plus real multiplication positivity.
Claim. If $R > 0$ and $Y_B > 0$, then the baryon-to-photon carrier $\eta_B(R,Y_B) := R \cdot Y_B$ satisfies $\eta_B(R,Y_B) > 0$.
background
This module stages honest, small targets for the Steve baryogenesis loop. The first invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so vanishing sourced $B-L$ with equilibrated sphalerons forces vanishing surviving baryon number.
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 multiplier $R = s/n_\gamma$: $\eta_B = R \cdot Y_B$. Both factors are formal; no magnitude is fixed here. In the physical band one expects $R \in (7.0, 7.1)$ after $e^\pm$ annihilation.
Upstream, orientation reversal (a3SourceBL_odd) shows that flipping the rolling direction $\dot\chi \mapsto -\dot\chi$ flips the $B-L$ source (linearity in $\mu_{BL} = K_x \dot\chi$). The linear carrier then carries that sign flip to $\eta_B$.
proof idea
One-line term proof. Unfold the definition $\eta_B(R,Y_B) = R \cdot Y_B$, then apply the standard real-multiplication positivity lemma: product of two positive reals is positive. No cosmology-specific lemmas are needed beyond the carrier definition.
why it matters
Locks sign preservation for the B6 base carrier in the baryogenesis staging lane: with $R > 0$, $\mathrm{sign}(\eta_B) = \mathrm{sign}(Y_B)$. Combined with orientation reversal of the $B-L$ source, flipping the 8-tick rolling direction flips the observable asymmetry. That ties the sign of $\eta_B$ to the eight-tick octave structure (T7) without inventing a new mechanism.
No downstream users are wired yet (used_by empty); the lemma is a staging guard so later magnitude or washout arguments cannot silently drop the positivity hypothesis. It does not close the open integrability tag on the integral-level orientation flip, nor does it fix the numerical value of $R$ or $Y_B$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.