g_star_D3_positive
plain-language theorem explainer
At the forced spatial dimension D = 3, the D-parameterized high-T relativistic degree count is strictly positive. Cosmology and unification proofs that need a positive g_★ factor in thermodynamic prefactors would cite this. The proof rewrites to the closed arithmetic form and evaluates it by norm_num.
Claim. Let $D = 3$ be the spatial dimension forced by the dimension-forcing chain. The $D$-parameterized relativistic degree-of-freedom count satisfies $0 < g_\star(D)$.
background
This module records exact arithmetic identities that re-express Standard Model high-temperature degree-of-freedom bookkeeping in D-flavored notation. It does not derive the SM spectrum: gauge representations, the Higgs doublet, chiral neutrino content, and the Fermi–Dirac 7/8 thermal weight are imported; only the numerical identities are kernel-checked here.
The spatial dimension $D$ is the constant 3 forced upstream by T8 (DimensionForcing). The ordinary high-T SM count is the familiar $g_\star = 106.75 = 28 + (7/8)\cdot 90$ (bosons 28, fermions 90 in the minimal-neutrino convention). The local object $g_\star(D)$ is the same assembly written against the D-parameterized fermionic and gap quantities developed in this file (dimension gap, dof-per-generation, eight-tick period $2^D$).
Upstream, $g_\star$ appears as an imported constant in Cosmology.BaryonAsymmetryDerivation and as the temperature-dependent step model in Cosmology.GStarThresholds; both document 106.75 as standard SM bookkeeping, not an independent RS prediction.
proof idea
Term-mode one-liner. Rewrite the goal with the closed-form evaluation g_star_D3_eq (which identifies $g_\star(D)$ at $D=3$ with the explicit rational 106.75), then discharge positivity by norm_num. No induction, no case split, no external analytic lemma.
why it matters
Positivity of the high-T degree count is the elementary side condition needed whenever $g_\star$ enters a thermodynamic prefactor (entropy density, energy density, freeze-out rates) inside the unification and cosmology layers. The parent module’s honest split is important: the identity $28 + (7/8)\cdot 90 = 106.75$ and the gap re-expression $90 = 2\times\mathrm{dimensionGap}(3)$ are proved arithmetic, while the SM content itself remains imported.
Framework landmarks in play are only T8 ($D=3$) and the eight-tick period $2^D=8$ used to write the Fermi weight as $(2^D-1)/2^D$. No claim is made on the forcing chain T0–T7, on RCL/J-uniqueness, or on the $\alpha$ band. Downstream use count is currently empty; the lemma is infrastructure for later gap-bridge and cosmology assemblies rather than a cited parent theorem today.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.