gStarCert
plain-language theorem explainer
Packages the high-T Standard Model relativistic DOF count into a single certificate: bosons 28, fermions 90, three generations, three colors, gluons 16, Higgs 4, and g_★ = 106.75 with positivity. Cosmology and SM bookkeeping cite it as the audited assembly of those equalities. The body is a structure instance wiring upstream equality theorems (and rfl for the Higgs count).
Claim. There is a certificate recording $g_b = 28$, $g_f = 90$, $N_{\mathrm{gen}} = 3$, $N_c = 3$, gluon DOF $= 16$, Higgs DOF $= 4$, the derived high-temperature value $g_\star = 106.75 = 427/4$, and $g_\star > 0$.
background
The module performs textbook high-temperature SM bookkeeping: $g_\star = g_b + (7/8) g_f = 28 + (7/8)\cdot 90 = 427/4 = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$ where every listed species is relativistic. Status is explicit bookkeeping over adopted SM content, not a novel RS prediction of a new number.
RS supplies the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ (from cube automorphisms) and the generation count $3$ (from $D=3$ face pairs). Imported physics includes the matter representations, the minimal-neutrino convention (left-handed only, 2 DOF per generation), and the thermal weight $7/8$ from Fermi–Dirac vs Bose–Einstein integrals. The structure GStarCert is the audited bundle of the component equalities that make this count machine-checkable.
proof idea
A structure instance, not a tactic proof. Each field is filled by an upstream equality: bosonic DOF from bosonic_dof_eq (28 via gauge generators, polarisations, Higgs), fermionic DOF from fermionic_dof_eq (90 = quarks + charged leptons + neutrinos), generations and colors from their equality lemmas, gluons from gluon_dof_eq (16), Higgs by rfl (definitionally 4), the aggregate $g_\star$ from g_star_derived_eq ($28 + (7/8)\cdot 90 = 427/4$), and positivity from g_star_derived_pos.
why it matters
Closes the assembly path advertised in the module doc: machine-checked SM $g_\star$ bookkeeping with RS-sourced gauge group and generation count. Upstream cosmology definitions (g_star in BaryonAsymmetryDerivation and the temperature-dependent g_star(T) in GStarThresholds) quote this assembly as the source of the constant $106.75 = 427/4$ at $T \sim 200,\mathrm{GeV}$.
Framework landmarks in play are T8 ($D=3$ forcing three generations) and the gauge group from the cube; the $7/8$ weight and matter reps remain imported. No downstream dependents are wired yet in this curated tree; the certificate is the stable handle for any later use that needs all component equalities at once. The Dirac-neutrino branch ($g_f=96$, $g_\star=112$) is deliberately separate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.