g_star_1GeV
plain-language theorem explainer
At T = 1 GeV the instantaneous-threshold SM count of relativistic degrees of freedom equals 247/4 = 61.75, after bottom, tau, and charm have dropped out. Cosmologists and RS auditors cite it as a machine-checked textbook spot check of g_★(T). The proof is a one-line native_decide on exact rational arithmetic.
Claim. Under the instantaneous-threshold step model for the Standard Model (minimal-neutrino convention), the relativistic degree-of-freedom count at temperature $T = 1\,\mathrm{GeV}$ equals $247/4$.
background
The module supplies the standard cosmology step function $g_\star(T)$: each SM species contributes its full relativistic weight while $T$ exceeds its mass threshold and drops out below it; the QCD switch near $0.15,\mathrm{GeV}$ replaces quark–gluon plasma content by pions. All sums are exact over $\mathbb{Q}$.
Mass thresholds are imported PDG rationals used only for ordering; particle weights match StandardModel.RelativisticDOF (gauge group and generation count RS-sourced; representations and the $7/8$ fermionic factor imported). Valid domain is $T\gtrsim 1,\mathrm{MeV}$.
At $T=1,\mathrm{GeV}$ one is below the bottom, tau, and charm thresholds, so those species are already decoupled, leaving the documented count $247/4=61.75$. The high-$T$ plateau recovers the familiar $106.75$.
proof idea
One-line tactic proof: native_decide evaluates the definition g_star 1 (i.e. g_starWith neutrinos at rational temperature 1) by exact arithmetic over $\mathbb{Q}$ and checks equality with the literal $247/4$. No lemmas are invoked; the kernel simply reduces the finite sum of active species weights.
why it matters
Closes one of the module's advertised textbook spot checks that answer the external-review complaint that the repository lacked a temperature-dependent $g_\star(T)$. It anchors the post-charm, pre-QCD window used in early-universe bookkeeping (entropy, Hubble rate, freeze-out estimates) without claiming a new RS mass prediction. No downstream theorems yet depend on it; it is infrastructure for later baryon-asymmetry and cosmology bridges that need epoch-dependent DOF rather than the single high-$T$ constant $106.75$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.