baryonYield_zero_of_chiDot_zero
plain-language theorem explainer
If the CP-odd source rate vanishes identically over the freeze-out window, the entropy-normalized baryon yield is zero. Cosmologists tracking Sakharov staging cite this to move the source-off obstruction from the raw sphaleron endpoint onto the dilution-invariant carrier Y_B. The proof unfolds the yield definition and rewrites via the banked zero of the reprocessed relic, then uses zero divided by entropy.
Claim. Let $a,\Gamma_w,c_\chi,T,\dot\chi:\mathbb{R}\to\mathbb{R}$ and $K_x,t_0,t_f,s\in\mathbb{R}$. If $\dot\chi(t')=0$ for every $t'$, then the baryon yield $Y_B:=n_B/s$ built from the sphaleron-reprocessed frozen $B-L$ charge (the Boltzmann relic profile of those backgrounds, mapped by the factor $28/79$) satisfies $Y_B=0$.
background
The module stages honest targets for electroweak baryogenesis so the lane cannot fake a missing source. The governing invariant is sphaleron zero-protection: electroweak sphalerons conserve $B-L$, so a vanishing sourced $B-L$ at equilibrium forces vanishing surviving baryon number.
The dilution-invariant carrier is the baryon yield $Y_B:=n_B/s$. The reprocessed baryon density is $n_B=(28/79)\cdot(B-L){\mathrm{frozen}}$, where the frozen charge is the Boltzmann relic profile of the backgrounds $(a,\Gamma_w,c\chi,T,\dot\chi)$ over $[t_0,t_f]$. The factor $28/79$ is the SM sphaleron reprocessing coefficient for three generations and one Higgs.
Upstream, Bfinal_zero_of_chiDot_zero already closes the seam from source-off through the sphaleron wall: if $\dot\chi\equiv 0$, the relic profile vanishes, hence the reprocessed $n_B$ vanishes. The present statement lifts that zero onto $Y_B$.
proof idea
One-line tactic chain. Unfold $Y_B=n_B/s$. Rewrite the numerator by the upstream theorem that source-off forces the sphaleron-reprocessed relic to zero. Conclude with the arithmetic fact $0/s=0$. No new analysis of the Boltzmann integral or of the $28/79$ factor is required; both are already banked.
why it matters
This is the first node where the source-off limit lives on the dilution-invariant yield rather than on the raw relic. In the staging loop that prevents fake baryogenesis mechanisms, it moves the cursor off the sphaleron endpoint: the factor $28/79$ stays a bounded coefficient inside $n_B$, never the trunk of the argument.
It sits downstream of the seam-closure theorem that chains the Boltzmann relic into the obstruction, and of the forcing direction that a nonzero relic forces nonzero $B-L$. Together they encode the Sakharov obstruction in RS cosmology: without a CP-odd $\dot\chi$ source, no baryon asymmetry survives equilibration. No downstream consumers are wired yet; the declaration is a staging target for later eta-conversion and observational matching.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.