etaBFromYield_odd
plain-language theorem explainer
The linear carrier that turns a frozen comoving baryon yield into the observable baryon-to-photon ratio is odd in the yield: flipping Y_B flips η_B. Cosmologists tracking the sign of η_B under 8-tick orientation reversal cite this. The proof is a one-line unfold-and-ring on the product definition η_B = R · Y_B.
Claim. For all real $R$ and $Y_B$, if $\eta_B(R,Y_B) := R\cdot Y_B$ converts a frozen comoving yield $Y_B=n_B/s$ into the baryon-to-photon ratio via the entropy-to-photon multiplier $R=s/n_\gamma$, then $\eta_B(R,-Y_B)=-\eta_B(R,Y_B)$.
background
BaryogenesisStaging holds small honest 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 base carrier etaBFromYield is the dimensionless map $\eta_B=R\cdot Y_B$. Here $Y_B=n_B/s$ is charge per entropy and $R=s/n_\gamma$ is entropy per photon; both arguments are formal, so no magnitude is fixed. Upstream orientation lemmas (e.g. oddness of the $a_3$ $B-L$ source under 8-tick flip) supply the sign change of $Y_B$; this lemma only transports that sign through the linear carrier.
The 8-tick octave (period $2^3$) is the fundamental evolution period in RS units ($\tau_0=1$ tick). Orientation of that cycle fixes the sign $\varepsilon$ that later enters the CKN source coefficient $K_X=\varepsilon/f_\chi$.
proof idea
One-line term proof. Unfold the definition $\eta_B(R,Y_B)=R\cdot Y_B$, then ring discharges the elementary identity $R\cdot(-Y_B)=-(R\cdot Y_B)$ over $\mathbb{R}$. No external lemmas are required beyond the definition of the carrier.
why it matters
Closes the sign-transport step in the baryogenesis staging chain: orientation reversal flips $Y_B$ (via upstream $a_3$ source oddness), and this lemma carries the flip to the observable $\eta_B$. Downstream, the CKN source-coefficient block records that orientation reversal negates $K_X=\varepsilon/f_\chi$, "structural origin of the sign carried to $\eta_B$ via a3SourceBL_odd / etaBFromYield_odd."
In the Recognition framework this sits on the eight-tick octave (T7): the discrete orientation of the $2^3$-period cycle is the only place the global sign of baryon excess is chosen. Without oddness of the carrier, a flipped ledger orientation could not be guaranteed to flip the predicted $\eta_B$. The module's honesty rule (no fake axioms, no admit) makes this algebraic bridge a required proved link rather than an assumed sign convention.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.