eta_B_structural
plain-language theorem explainer
Defines the structural baryon-to-photon ratio as the Jarlskog CP invariant divided by the SM relativistic degree count g_★ = 106.75. Cosmologists cite it only for the sign theorem (matter over antimatter) and the weak bound η_B < 1. It is a one-line quotient scaffold, not a magnitude prediction: numerically ~3×10⁻⁷, roughly 500× the observed 6×10⁻¹⁰, because washout is underived.
Claim. The structural baryon-to-photon ratio is the real number $\eta_B^{\mathrm{struct}} := J_{CP}/g_\star$, where $J_{CP}$ is the structural Jarlskog invariant and $g_\star = 106.75$ is the SM relativistic degree-of-freedom count above the electroweak temperature.
background
In electroweak baryogenesis the baryon asymmetry has the textbook shape $\eta_B \propto (\varepsilon_{CP}/g_\star)\times(\text{washout})$, with $\varepsilon_{CP}$ proportional to the Jarlskog invariant $J_{CP}$. This module splits that skeleton honestly: the structural quotient is a scaffold used only for sign and smallness; the Planck-matched magnitude is a separate $\varphi$-rung hypothesis $\varphi^{-44}(1-\varphi^{-8})^2$ that does not involve $g_\star$.
Here $g_\star$ is the high-temperature SM bookkeeping value 106.75 (bosons 28, fermions 90 with the 7/8 weight; minimal-neutrino convention), assembled from the RS-sourced gauge group and three-generation count rather than postulated as a new RS number. The temperature-dependent step model in GStarThresholds recovers the same 427/4 at $T=200,\mathrm{GeV}$.
The module imports Sakharov-from-ledger conditions, Gray-code chirality (source of $J_{CP}>0$), and the CKM/Jarlskog stack. Observed $\eta_B\approx 6.1\times 10^{-10}$ comes from BBN and Planck 2018; the structural value is larger by the missing order-one washout factor $c$.
proof idea
Pure definition: the real is introduced as the quotient of the already-defined structural Jarlskog invariant by the constant $g_\star=106.75$. No tactics, no lemmas. Downstream positivity and smallness proofs unfold this name and apply div_pos / div_lt_one with jarlskog_positive and a numeric check on $g_\star$.
why it matters
This is the carrier object for the module's only theorem-grade content: the SIGN of the baryon asymmetry. eta_B_positive shows $\eta_B^{\mathrm{struct}}>0$ from $J_{CP}>0$; eta_B_small shows it is less than 1. Both feed derivation_chain_complete, which packages the full sign chain (three generations from $D=3$ face pairs, Gray-code chirality, positive Jarlskog, sphaleron $\Delta B=3$, hence positive $\eta_B$).
BaryonAsymmetryCert records eta_pos and eta_small alongside Sakharov conditions and a conditional EWFirstOrder hypothesis. EtaBCert in the interval module likewise requires structural positivity while the magnitude band is handled by the separate $\varphi^{-44}$ arithmetic.
Framework landmarks in play: three generations forced by $D=3$ (T8), chirality from the eight-tick Gray path (T7), and CP phase from the cube/CKM construction. The open physics is Boltzmann washout through the electroweak transition; the module header states explicitly that scaffold and rung match are not identified.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.