g_star_derived_eq_decimal
plain-language theorem explainer
The derived high-temperature SM effective DOF count equals the exact rational 10675/100 (i.e. 106.75). Cosmologists matching the machine-checked particle tally to the conventional decimal bookkeeping cite this equality. The proof rewrites via the 427/4 form and finishes by rational arithmetic.
Claim. The derived high-temperature relativistic effective degree-of-freedom count equals $10675/100$ as an exact rational: $g_\star^{\mathrm{der}} = 10675/100$. Equivalently, $427/4 = 106.75$ in $\mathbb{Q}$.
background
In the high-temperature Standard Model (above the electroweak transition) every SM species is relativistic. The effective count is $g_\star = g_b + (7/8) g_f$, with bosonic helicity states $g_b = 28$ and fermionic states $g_f = 90$, so $g_\star = 106.75$. The Boltzmann weight $7/8$ is the integrated Fermi–Dirac versus Bose–Einstein factor against $T^3$.
This module rebuilds that number from an explicit Q₃-forced SM tally: gauge generators $8+3+1$ times two polarisations, four real Higgs scalars, and three-generation quark, charged-lepton, and neutrino helicity counts. The assembly is pure rational arithmetic: g_star_derived is defined as bosonic DOF plus $(7/8)$ times fermionic DOF.
Upstream, g_star_derived_eq already proves the closed form $427/4$. The older baryogenesis module still carries a hand-entered real constant $106.75$; the present equality is the decimal-rational twin of that fraction.
proof idea
One rewrite plus numeric normalisation. Apply g_star_derived_eq, which states g_star_derived = 427/4, then norm_num discharges the pure rational identity $427/4 = 10675/100$ in $\mathbb{Q}$. No particle-content unfolding is repeated here; that work lives in the upstream equality.
why it matters
Closes the last arithmetic step that exhibits the derived $g_\star$ in the conventional decimal form used throughout cosmology literature and in BaryonAsymmetryDerivation.g_star. The module doc frames the whole file as promoting a hand-entered constant to a counted rational; this theorem is the decimal face of that promotion ($427/4 = 106.75$).
It sits inside the RS cosmology stack where SM content is treated as Q₃-forced (gauge group, three generations, helicity bookkeeping) rather than an independent free parameter. No downstream Lean users are recorded yet; the intended consumer is the bridge that identifies the derived rational with the existing real constant used in baryon-asymmetry estimates. Landmark contact is indirect: the count assumes the forced SM spectrum, not a fresh T0–T8 step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.