gStarDerivationCert
plain-language theorem explainer
The high-temperature SM effective DOF count g_⋆ equals exactly 427/4 = 106.75, obtained by counting bosonic helicities (28) and fermionic helicities (90) with the 7/8 Fermi factor. Cosmologists citing the baryon-asymmetry pipeline use this certificate to replace the hand-entered constant. The proof is a four-field structure inhabitant wiring the four already-proved equalities.
Claim. The certificate holds: bosonic helicity DOF equal $28$, fermionic helicity DOF equal $90$, the derived $g_\star = 28 + (7/8)\cdot 90$ equals the rational $427/4$, and casting that rational to $\mathbb{R}$ recovers the $g_\star$ constant used in the baryon-asymmetry derivation.
background
Above the electroweak transition every Standard Model species is relativistic. The effective number of degrees of freedom is then $g_\star = g_b + (7/8) g_f$, where the $7/8$ is the exact Bose–Fermi integral ratio against $T^3$. The module counts $g_b$ and $g_f$ from Q₃-forced SM content rather than inserting 106.75 by hand.
Bosonic side: SU(3)×SU(2)×U(1) gives 12 generators × 2 polarisations = 24 gauge DOF, plus 4 real Higgs scalars from one complex doublet, totaling 28. Fermionic side (three generations): 72 quark + 12 charged-lepton + 6 neutrino helicity states = 90. Multiplying out yields the exact rational $427/4$.
Upstream, bosonic_dof_eq and fermionic_dof_eq discharge the two counts by unfolding and decide/rw; g_star_derived_eq multiplies the formula to $427/4$; g_star_derived_eq_baryogenesis casts and matches the existing real constant in BaryonAsymmetryDerivation.
proof idea
Term-mode structure inhabitant. The four fields of GStarDerivationCert are filled by the four named equalities already proved in-module: bosonic count via bosonic_dof_eq, fermionic count via fermionic_dof_eq, rational formula via g_star_derived_eq, and real bridge via g_star_derived_eq_baryogenesis. No further tactics; the certificate is just the bundle.
why it matters
Closes the gap between a hand-entered cosmology constant and an explicit SM helicity count forced by the Q₃ chord-cube particle content. Downstream, t6_t8_to_cosmology_constants_bridge_holds in the Unified Forcing Chain routes T6/T8 (φ forced, D = 3) through theorem-backed cosmology surfaces; this certificate supplies the exact $g_\star$ identity that bridge consumes, keeping empirical bands separate from exact identities. It is the load-bearing link that lets baryon-asymmetry numerics inherit a derived rather than stipulated DOF count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.