GStarDerivationCert
plain-language theorem explainer
A Prop-valued certificate that packages the high-T SM relativistic DOF count: 28 bosonic helicities, 90 fermionic helicities, and the exact rational g_★ = 427/4, together with equality to the hand-entered baryogenesis constant. Cosmology and forcing-chain authors cite it when they need a single kernel-only witness that the derived bookkeeping matches the imported 106.75. The structure itself is pure data; the inhabiting theorem fills the four fields from the counting lemmas.
Claim. A certificate asserting four facts: the bosonic helicity count equals $28$; the fermionic helicity count equals $90$; the derived high-temperature effective degrees of freedom equal the rational $427/4$; and that rational, cast to $\mathbb{R}$, equals the constant $g_\star = 106.75$ used in the baryon-asymmetry module.
background
Above the electroweak transition every Standard Model species is relativistic. The effective DOF count is then $g_\star = g_b + (7/8) g_f$, with the $7/8$ factor the integrated Bose–Fermi thermal weight. The module derives this from Q₃-forced SM content rather than leaving $106.75$ as a magic constant.
Bosonic count: SU(3)×SU(2)×U(1) gives $8+3+1=12$ generators times two polarisations (massless W/Z before breaking), plus four real Higgs scalars from one complex doublet, totaling $g_b = 28$. Fermionic count (three generations): quarks $6\times 3\times 2\times 2 = 72$, charged leptons $12$, neutrinos $6$ (one helicity each), totaling $g_f = 90$. The derived quantity is the exact rational $(28)+(7/8)\cdot 90 = 427/4$.
Upstream, BaryonAsymmetryDerivation.g_star is the noncomputable real $106.75$ that this certificate must match. Sibling defs bosonic_dof, fermionic_dof, and g_star_derived perform the explicit ℕ/ℚ arithmetic.
proof idea
No proof body: the declaration is a Prop-structure with four fields. Inhabitation is deferred to the sibling theorem that builds a term by supplying bosonic_dof_eq (bosonic count is 28), fermionic_dof_eq (fermionic count is 90), g_star_derived_eq (rational equals $427/4$), and g_star_derived_eq_baryogenesis (cast equality to the baryogenesis constant). All four lemmas are exact ℚ/ℕ arithmetic closed by native_decide or definitional unfolding; nothing analytic is required.
why it matters
Closes the gap between a hand-entered cosmology constant and an explicit SM helicity census forced by the Q₃ chord-cube content (gauge group, three generations, D=3 polarisation count). The inhabiting theorem gStarDerivationCert is the kernel-only witness. Downstream, T6T8_To_CosmologyConstants_Bridge in the unified forcing chain consumes this certificate so that T6 (φ uniqueness) and T8 (D=3) can route into cosmology constants without an external $g_\star$ postulate. The module doc frames the count as imported SM content with RS-sourced gauge group and generation number, not an independent prediction of a new numerical value; the contribution is machine-checked assembly and the bridge identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.