g_star_derived_eq
plain-language theorem explainer
The high-temperature SM effective relativistic DOF, assembled from explicit bosonic and fermionic helicity counts with the Fermi–Dirac factor 7/8, equals the exact rational 427/4 (= 106.75). Cosmologists and anyone wiring baryogenesis or g_⋆(T) thresholds cite this identity. The proof is pure definitional unfolding followed by rational arithmetic via norm_num.
Claim. The derived high-temperature effective relativistic degrees of freedom equal $427/4$: $g_\star^{\mathrm{der}} = g_b + \frac{7}{8} g_f = 28 + \frac{7}{8}\cdot 90 = \frac{427}{4}$.
background
Above the electroweak transition every Standard Model species is relativistic, so the effective DOF that enter the radiation energy density are the plain helicity counts with a Boltzmann weight: $g_\star = g_b + (7/8) g_f$. The bosonic side is gauge generators times two transverse polarisations plus the four real components of the complex Higgs doublet; the fermionic side sums quarks (flavours × colours × spin × particle/antiparticle), charged leptons, and left-handed neutrinos over three generations.
This module replaces the hand-entered real constant g_star := 106.75 from BaryonAsymmetryDerivation by an exact rational built from those counts. Upstream defs fix the pieces: gauge generators $8+3+1$, two polarisations, Higgs 4, fermionic total 90, and the exact Fermi–Dirac/Bose–Einstein ratio $7/8$ integrated against $T^3$. The local claim is that the assembled expression collapses to $427/4$.
proof idea
Unfold the entire definition stack: the derived $g_\star$, the fermionic Boltzmann factor $7/8$, bosonic DOF (gauge + Higgs), gauge DOF (generators × polarisations), Higgs DOF, fermionic DOF (quarks + charged leptons + neutrinos), and every multiplicity constant (flavours, colours, spins, particle/antiparticle). After full expansion the goal is a pure rational equality, discharged by norm_num.
why it matters
This is the arithmetic spine of the $g_\star$ derivation: the certificate gStarDerivationCert packages it with the bosonic/fermionic count lemmas and the bridge to the older real constant. Downstream, g_star_derived_eq_baryogenesis casts $427/4$ to $\mathbb{R}$ and matches BaryonAsymmetryDerivation.g_star; g_star_derived_eq_decimal records the decimal form 106.75; thresholds and RelativisticDOF reuse it so the high-T plateau is a function value, not a free number. The UnifiedForcingChain bridge t6_t8_to_cosmology_constants_bridge_holds routes cosmology constants through such theorem-backed surfaces once T6 ($\varphi$ forced) and T8 ($D=3$) are in hand. The counting is the SM content forced by the $Q_3$ chord-cube story in the module doc; the identity itself is exact $\mathbb{Q}$ arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.