g_star_derived_pos
plain-language theorem explainer
The derived high-temperature SM relativistic degree-of-freedom count is strictly positive. Cosmology and electroweak bookkeeping cite it whenever a certificate or inequality needs 0 < g_★ rather than the bare rational. The proof rewrites to the closed form 427/4 and finishes by numeric evaluation.
Claim. The exact rational $g_\star$ assembled from SM bosonic and fermionic relativistic degrees of freedom satisfies $0 < g_\star$. Equivalently, $0 < 427/4$.
background
This module performs textbook high-temperature Standard Model bookkeeping: $g_\star = g_b + (7/8) g_f = 28 + (7/8)\cdot 90 = 427/4 = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$ where all listed species are relativistic. Recognition Science supplies the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ (from cube automorphisms) and the generation count 3 (from $D=3$ face pairs); the matter representations, minimal-neutrino convention, and the integral value $7/8$ are imported SM content.
Upstream, g_star_derived is the exact rational
$(\mathrm{bosonic_dof}:\mathbb{Q}) + \mathrm{fermion_boltzmann}\cdot(\mathrm{fermionic_dof}:\mathbb{Q})$.
The companion equality states $g_\star = 28 + (7/8)\times 90 = 427/4$. Parallel hand-entered constants appear in baryon-asymmetry and threshold modules as the real $106.75$ or the step function $g_\star(T)$.
proof idea
One short tactic proof. Rewrite the goal with the closed-form equality $g_\star = 427/4$, then norm_num discharges the concrete inequality $0 < 427/4$ over the rationals. No case splits or induction.
why it matters
Positivity is the minimal well-formedness fact needed before $g_\star$ enters certificates or denominators. Downstream it feeds gStarCert, the structured certificate packing bosonic/fermionic equalities, generation and color counts, and gluon DOF into one record for Standard Model relativistic bookkeeping.
In the Recognition framework this sits on the bookkeeping side of the ledger: RS-sourced inputs are the gauge group (GaugeFromCube) and three generations (ParticleGenerations, from $D=3$ in the forcing chain T8), while the numerical assembly $106.75$ itself is not claimed as a novel RS prediction. The temperature-dependent cousin lives in Cosmology.GStarThresholds; the high-$T$ plateau value is the one certified here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.