baryonYield
plain-language theorem explainer
Defines the dilution-invariant baryon yield $Y_B = n_B/s$ as the entropy-normalized baryon density. Cosmologists tracking electroweak baryogenesis cite it as the epoch-stable carrier that the sphaleron-reprocessed charge feeds, before conversion to $\eta_B$. The body is a one-line quotient of two reals.
Claim. The baryon yield is the real number $Y_B(n_B,s) := n_B/s$, where $n_B$ is the baryon number density and $s$ is the entropy density.
background
In the Baryogenesis Staging module the goal is honest, small theorem targets for the Steve baryogenesis loop. The 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 classical baryon-to-entropy ratio $Y_B = n_B/s$ is the dilution-invariant object that survives cosmic expansion. The already-banked conversion $\eta_B = R\cdot Y_B$ (via etaBFromYield) then recovers the photon-normalized asymmetry. Upstream, Bfinal_zero_of_chiDot_zero shows that a vanishing source $\dot\chi\equiv 0$ forces the sphaleron-reprocessed final baryon number to zero, chaining the Boltzmann relic into the obstruction.
proof idea
Pure definition: the body is the real division $n_B/s$. No lemmas, no tactics. Downstream proofs simply unfold this carrier and reduce.
why it matters
Introducing $Y_B$ as its own carrier moves the magnitude off the sphaleron endpoint: the classic $28/79$ reprocessing factor stays a bounded coefficient inside $n_B$, never the trunk of the argument. The immediate parent is baryonYield_zero_of_chiDot_zero, which lifts the source-off limit from the raw relic through the banked sphaleron map onto this dilution-invariant carrier: with $\dot\chi\equiv 0$ one gets $n_B=0$ hence $Y_B=0$. That is the first node where the obstruction lives on the object the cursor actually tracks. It sits inside the broader Sakharov-from-ledger and sphaleron-rate staging that keeps the baryogenesis lane from faking a missing mechanism.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.