GStarCert
plain-language theorem explainer
Certificate structure packing the high-temperature SM relativistic DOF equalities: bosons 28, fermions 90, three generations and colors, gluons 16, Higgs 4, and g_★ = 106.75 with positivity. Cosmology and SM bookkeeping cite it as the typed bundle of those facts. It is a pure structure definition; the equalities are discharged by the companion instance gStarCert.
Claim. A certificate is a record of the equalities $g_b = 28$, $g_f = 90$, $N_{\mathrm{gen}} = 3$, $N_c = 3$, gluon DOF $= 16$, Higgs DOF $= 4$, the derived $g_\star = 106.75$, and $g_\star > 0$, where $g_\star = g_b + (7/8) g_f$ in the high-$T$ minimal-neutrino SM count.
background
This module assembles the textbook high-temperature Standard Model relativistic degree-of-freedom count $g_\star = g_b + (7/8) g_f = 28 + (7/8)\cdot 90 = 427/4 = 106.75$ as exact rational arithmetic. Scope is bookkeeping over adopted SM content, valid only for $T \gtrsim T_{\mathrm{EW}}$ where all listed species are relativistic.
Upstream, bosonic_dof is gauge plus Higgs DOF; higgs_dof is the four real components of the complex $SU(2)$ doublet above the electroweak transition; fermionic_dof sums quarks, charged leptons, and neutrinos over generations; g_star_derived is the rational $g_b + (7/8) g_f$. Generation count 3 and the gauge group enter from RS-sourced inputs (ParticleGenerations, GaugeFromCube); matter representations, the 7/8 thermal weight, and the left-handed-only neutrino convention are imported SM content.
The companion cosmology defs fix the same number as a real constant and as a temperature-dependent threshold function; this structure is the typed master bundle of the component equalities.
proof idea
No proof body: this is a structure (record type) whose fields are propositions. Each field names an equality or inequality that a later instance must supply. The companion definition gStarCert fills those fields by applying the component lemmas bosonic_dof_eq, fermionic_dof_eq, n_generations_eq, n_colors_eq, gluon_dof_eq, and the corresponding Higgs, $g_\star$, and positivity results. The structure itself only declares the interface.
why it matters
Part 6 of the module (Master Certificate) packages the full high-$T$ $g_\star$ bookkeeping so downstream cosmology can depend on one typed object rather than a scatter of lemmas. The sole direct consumer is gStarCert, the inhabited instance.
In the Recognition framework this sits on the bookkeeping side of the ledger: RS supplies the gauge group from cube automorphisms and $N_{\mathrm{gen}} = 3$ from $D = 3$ face pairs (forcing-chain landmarks T7/T8 and ParticleGenerations), while the representation content and 7/8 weight remain standard physics. The certificate makes that split auditable. It does not close an open prediction; it locks the assembly used by baryon-asymmetry and threshold $g_\star(T)$ pipelines that quote $g_\star = 106.75$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.