g_star_10GeV
plain-language theorem explainer
At temperature T = 10 GeV the instantaneous-threshold SM count of relativistic degrees of freedom equals 345/4 = 86.25, after the top, Higgs, Z, and W have dropped out. Cosmologists and RS auditors cite it as a textbook spot-check of the step-function g_★(T). The proof is a one-line native_decide on exact rational arithmetic.
Claim. Under the instantaneous-threshold model with the minimal-SM neutrino convention, the relativistic degree-of-freedom count at $T = 10\,\mathrm{GeV}$ equals $345/4$ (i.e. $86.25$), after the top quark, Higgs, $Z$, and $W$ have decoupled.
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, with a QCD switch at $T_{\mathrm{QCD}}\approx 0.15,\mathrm{GeV}$ from quark–gluon plasma to pions. All sums are exact over $\mathbb{Q}$.
The local definition is $g_\star(T) := g_{\star\mathrm{With}}(\mathrm{neutrinos}, T)$, using the same imported SM bookkeeping as StandardModel.RelativisticDOF (gauge group and generation count RS-sourced; matter representations and the $7/8$ fermionic weight imported). Mass thresholds are PDG-rounded rationals used only for ordering, not re-derived from the $\varphi$-ladder.
At high $T$ the constant $g_\star = 106.75 = 427/4$ recovers the usual SM total (bosons 28, fermions 90). The $T = 10,\mathrm{GeV}$ slice sits below the electroweak scale, so $t$, $H$, $Z$, and $W$ are already non-relativistic.
proof idea
Term-mode proof by native_decide. The definition of $g_\star(T)$ expands to a finite rational sum of species contributions gated by threshold comparisons; at the concrete rational $T = 10$ those comparisons are decidable, the sum collapses to $345/4$, and the kernel checks the equality by exact arithmetic. No lemmas are invoked beyond the definitional unfolding of the step function.
why it matters
Closes one of the module's advertised textbook spot-checks (doc-comment: "$T = 10,\mathrm{GeV}$: $t$, $H$, $Z$, $W$ decoupled $\to 345/4 = 86.25$"). The module itself was built to answer the external-review objection that the repository fixed a single $g_\star$ and lacked a temperature-dependent threshold model. Together with the sibling evaluations at 200 GeV, 1 GeV, etc., it certifies that the step function reproduces the standard epoch-dependent values used in freeze-out and baryogenesis calculations, while remaining honest that it is a MODEL over adopted SM content rather than a pure RS derivation of particle content.
No downstream theorems currently depend on this particular evaluation; it is infrastructure for any later cosmology argument that needs $g_\star$ below the electroweak scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.