g_star_derived_eq
plain-language theorem explainer
The high-temperature Standard Model effective relativistic degree count equals exactly 106.75. Cosmologists and anyone wiring RS gauge/generation inputs into g_⋆ bookkeeping cite this equality. The proof unfolds the rational definition, substitutes the proved bosonic count 28 and fermionic count 90 with weight 7/8, then closes by numeric normalization.
Claim. The derived high-temperature effective relativistic degree of freedom count equals $106.75$: $g_\star = g_b + \frac{7}{8} g_f = 28 + \frac{7}{8}\cdot 90 = 106.75$.
background
In the high-temperature Standard Model (T ≳ T_EW), the energy-density effective DOF count is the textbook combination g_⋆ = g_b + (7/8) g_f. Bosons contribute with weight 1; fermions with the Fermi–Dirac thermal weight 7/8, the ratio of the integrals ∫ x³/(eˣ+1) dx over ∫ x³/(eˣ−1) dx. That integral value is imported statistical mechanics; RS supplies only the Fermi vs Bose sign via the eight-tick spin-statistics theorem.
This module treats the count as exact rational bookkeeping over adopted SM content, not a novel RS prediction. RS-derived inputs used upstream are the gauge group SU(3)×SU(2)×U(1) from cube automorphisms and the generation count 3 from D = 3 face pairs. Imported inputs include the SM fermion representations, the minimal (left-handed) neutrino convention, and the high-T scope itself.
Locally, bosonic_dof_eq proves g_b = 28 (gluons, electroweak vectors in the symmetric phase, Higgs). fermionic_dof_eq proves g_f = 90 (quarks, charged leptons, neutrinos across three generations). The definition g_star_derived assembles g_b + fermi_dirac_weight · g_f with fermi_dirac_weight = 7/8.
proof idea
Short tactic proof. Unfold the definition of the derived count and the constant fermi_dirac_weight (= 7/8). Rewrite with the two counting lemmas bosonic_dof_eq (g_b = 28) and fermionic_dof_eq (g_f = 90). The goal reduces to the rational identity 28 + (7/8)·90 = 106.75, discharged by norm_num.
why it matters
Pins the single high-T number that cosmology modules treat as g_⋆. Downstream, gStarCert and the Cosmology twin gStarDerivationCert package it with the bosonic and fermionic counting lemmas. Bridges cast it to the baryogenesis constant (g_star_derived_eq_baryogenesis) and to the decimal form 106.75 (g_star_derived_eq_decimal). GStarThresholds uses it so the old fixed 106.75 becomes the high-T evaluation of g_⋆(T) rather than a free-standing constant (g_star_high_matches_derived).
In the forcing chain it appears on the T6/T8-to-cosmology-constants bridge, routing active cosmology constants through theorem-backed surfaces while keeping empirical bands separate. Framework landmarks in play are T7 (eight-tick octave, spin-statistics sign) and T8 (D = 3, three generations). The module status tag is explicit: bookkeeping over adopted SM content, not an RS-first-principles derivation of the matter representations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.