g_star_steps_antitone_chain
plain-language theorem explainer
At five standard temperature checkpoints (2 MeV through 200 GeV), the SM step-function relativistic DOF count rises strictly with T. Anyone quoting epoch-dependent g_★ values in RS cosmology cites this chain. The proof is a single native_decide on exact rational arithmetic, matching the textbook sequence 10.75 < 17.25 < 61.75 < 86.25 < 106.75.
Claim. Under the instantaneous-threshold SM model, the relativistic degree count satisfies $g_\star(1/500)<g_\star(7/50)\land g_\star(7/50)<g_\star(1)\land g_\star(1)<g_\star(10)\land g_\star(10)<g_\star(200)$ (temperatures in GeV). Equivalently, as the universe cools through those epochs one has the strict decrease $106.75>86.25>61.75>17.25>10.75$.
background
The module supplies a temperature-dependent $g_\star(T)$ for the minimal-SM neutrino convention. Each species contributes its full relativistic count while $T$ exceeds its mass threshold and drops out below it; the QCD confinement step at $T_{\mathrm{QCD}}\approx 0.15,\mathrm{GeV}$ switches the strong sector from quark–gluon plasma to pions. All arithmetic is exact over $\mathbb{Q}$.
Mass thresholds are imported PDG rationals used only for ordering; particle content per species matches the bookkeeping in StandardModel.RelativisticDOF. The high-$T$ value is the familiar $g_\star=106.75=427/4$, now recovered as the function evaluation $g_\star(200)$ rather than a free-standing constant.
Valid domain is $T\gtrsim 1,\mathrm{MeV}$ (above neutrino decoupling). The model is the standard leading step approximation: no Boltzmann tails, no lattice-QCD crossover EOS, and no $(4/11)^{4/3}$ neutrino reheating factor.
proof idea
One-line decision proof: native_decide evaluates the four strict inequalities on the concrete rational values of the step function at $T\in{1/500,,7/50,,1,,10,,200}$. Because $g_\star$ is defined by finite case splits on rational thresholds, each evaluation is an exact $\mathbb{Q}$ sum, and the kernel decides the comparisons without further lemmas.
why it matters
Closes the external-review gap that RS cosmology fixed a single $g_\star$ number instead of a temperature-dependent function with threshold decoupling. The chain certifies the five textbook epoch values used throughout the cosmology modules and underwrites the bridge that the old constant $106.75$ is simply $g_\star(200)$. No downstream theorems yet depend on it; it is a spot-check lemma that anchors the step model against standard SM cosmology tables. It does not touch the forcing chain (T0–T8) or the $\varphi$-ladder mass predictions; those supply the mass ordering used here only as imported thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.