g_star_140MeV
plain-language theorem explainer
At $T=0.14\,\mathrm{GeV}$ (just below $T_\mathrm{QCD}$), the SM step-function $g_\star(T)$ equals $69/4=17.25$, with active species $\gamma,\pi,\mu,e,\nu$. Cosmologists auditing the RS temperature-dependent DOF model against textbook thresholds cite this. Proof is exact rational evaluation via `native_decide`.
Claim. The temperature-dependent relativistic degree-of-freedom count satisfies $g_\star(7/50)=69/4$, where the argument $T=7/50=0.14\,\mathrm{GeV}$ lies just below the QCD confinement threshold, so the active content is photons, pions, muons, electrons, and neutrinos ($69/4=17.25$).
background
The module implements the standard instantaneous-threshold step function $g_\star(T)$: each SM species contributes its full relativistic weight while $T$ exceeds its mass threshold and drops out below it. At the QCD transition $T_\mathrm{QCD}\approx 0.15,\mathrm{GeV}$ the strong sector switches from quark–gluon plasma (gluons + $u,d,s$) to hadronic content (pions). All arithmetic is exact over $\mathbb{Q}$.
The local definition is $g_\star(T):=g_\starWith,\mathrm{neutrinos},T$ under the minimal-neutrino convention, valid for $T\gtrsim 1,\mathrm{MeV}$. Mass thresholds are imported PDG rationals used only for ordering; particle content matches StandardModel.RelativisticDOF. The high-$T$ plateau recovers the familiar $g_\star=106.75=427/4$.
This spot check sits just below $T_\mathrm{QCD}$: pions remain, quarks/gluons are already confined out, and heavier species ($\tau,c,\ldots$) have long since dropped.
proof idea
One-line term proof: native_decide evaluates the closed rational definition of the step-function $g_\star$ at the concrete input $7/50$ and checks equality with $69/4$. No lemmas are invoked; the kernel decides the finite Boolean combination of threshold comparisons and the weighted species sum over $\mathbb{Q}$.
why it matters
Closes one of the module's advertised textbook spot checks (doc-comment: "$T=0.14,\mathrm{GeV}$ just below $T_\mathrm{QCD}$: $\gamma,\pi,\mu,e,\nu\to 69/4=17.25$"). The module itself was built to answer the external-review gap that RS fixed a single $g_\star$ number and lacked a temperature-dependent threshold model. No downstream consumers yet (used_by empty); the result is infrastructure for later epoch-dependent cosmology (BBN, baryon asymmetry, entropy dumps) that need $g_\star$ at the hadronic window. It does not touch the forcing chain T0–T8 or the $\varphi$-ladder masses; those supply independent mass orderings that this module only consumes as thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.