fermi_dirac_weight
plain-language theorem explainer
The Fermi–Dirac thermal weight is the constant 7/8: each fermionic degree of freedom contributes 7/8 the energy density of a bosonic one in equilibrium. Anyone assembling high-T g_* from SM species counts cites this factor. It is a bare rational definition importing the standard integral ratio, not a derived theorem.
Claim. The Fermi–Dirac weighting factor equals $7/8$, i.e. $\int_0^\infty x^3/(e^x+1)\,dx = (7/8)\int_0^\infty x^3/(e^x-1)\,dx$. Fermions therefore contribute $7/8$ as much energy density per degree of freedom as bosons in thermal equilibrium.
background
This module performs textbook high-temperature SM bookkeeping: $g_\star = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 106.75$, valid only for $T\gtrsim T_{\mathrm{EW}}$ where all listed species are relativistic. Status is bookkeeping over adopted SM content, not a novel RS prediction.
RS supplies the gauge group from cube automorphisms, three generations from $D=3$, and the Fermi vs Bose sign via the eight-tick spin-statistics theorem. The numerical ratio $7/8$ itself is imported standard statistical mechanics; the energy-density integrals are not formalized here.
Sibling counts (gluon, weak-boson, Higgs, quark, lepton DOF) feed the same assembly. The temperature-dependent step function lives downstream in Cosmology.GStarThresholds.
proof idea
One-line definition: the real constant is assigned the rational value $7/8$. No lemmas, tactics, or integral formalization. Downstream positivity is a separate norm_num check on this constant.
why it matters
This constant is the fermionic multiplier in every $g_\star$ assembly in the module: $g_\star^{\mathrm{derived}} = g_b + (7/8)g_f$ (minimal neutrinos, $106.75$) and the Dirac-neutrino branch $g_\star^{\mathrm{Dirac}}$ ($112$). Equality theorems unfold it and reduce by norm_num.
Cosmology.GStarThresholds reuses the same weight when building species energy-density contributions below $T_{\mathrm{QCD}}$. Framework landmark: the sign (Fermi–Dirac $+1$ vs Bose–Einstein $-1$) is the RS-sourced piece, tied to the eight-tick spin-statistics theorem (T7 octave); the integral value $7/8$ is deliberately marked imported. Closes no open forcing-chain step; it is honest SM thermal bookkeeping with an RS-sourced sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.