g_star_D3_eq
plain-language theorem explainer
At spatial dimension D = 3 the effective relativistic DOF count is exactly 106.75, the standard high-T SM value. Anyone citing the Fermion DOF / dimension-gap arithmetic certificate or positivity of g_star at D = 3 needs this identity. The proof unfolds the D-parameterized formula and rewrites with the imported bosonic (28) and fermionic (90) counts plus the 7/8 Fermi–Dirac weight, then closes by exact arithmetic.
Claim. With spatial dimension fixed at $D = 3$, the effective high-temperature relativistic degree-of-freedom count satisfies $g_\star(D) = 106.75$, i.e. $28 + \frac{7}{8}\times 90 = 106.75$.
background
This module sits in the Unification layer and proves only arithmetic identities that relate imported Standard Model degree-of-freedom counts to combinatorial quantities built from $D = 3$. It does not derive the SM spectrum. The honest split is: SM matter representations, the minimal-neutrino convention $g_f = 90$, the Fermi–Dirac thermal weight $7/8$, and the high-$T$ scope of $g_\star = 106.75$ are imported physics; $D = 3$ (T8 / DimensionForcing), the eight-tick period $2^D = 8$, and the generation count 3 are RS-derived upstream and only cited here.
The local definition $D := 3$ is the spatial dimension forced by T8. Upstream, bosonic_dof_eq records the standard bosonic count 28 (gauge + Higgs), and fermionic_dof_eq records the fermion helicity count $72 + 12 + 6 = 90$. The assembled formula is the usual $g_\star = g_b + \frac{7}{8} g_f$. The module’s point is that these known numbers also admit exact $D$-flavored re-expressions (e.g. $90 = 2 \times$ dimensionGap$(3)$, $7/8 = (2^3-1)/2^3$), checked by the kernel.
proof idea
Term-mode proof by unfolding and exact arithmetic. Unfold the definition of $g_\star(D)$. Rewrite with three facts: the Fermi–Dirac weight specialized at $D = 3$ equals $7/8$, the fermionic DOF identity (count $= 90$), and the bosonic DOF identity (count $= 28$). Close with norm_num, which evaluates $28 + (7/8)\times 90 = 106.75$ in exact rational arithmetic. No combinatorial or physical reasoning is performed in this step; it is pure assembly of already-proved equalities.
why it matters
This is the assembled high-$T$ identity that the module’s certificate packages. Downstream, fermion_dof_gap_certificate conjoins five kernel-checked facts, one of which is exactly $g_\star(D) = 106.75$; g_star_D3_positive rewrites through this equality and applies norm_num to get $0 < g_\star(D)$. In the Recognition framework the surrounding story ties $D = 3$ (T8) and the eight-tick octave $2^D = 8$ to $D$-flavored rewrites of the weight and the fermion count, but the module status note is explicit: a re-expression after the target number is known is not a derivation of that number. Closing a true RS derivation of $g_\star$ would still require deriving the gauge representations, Higgs doublet, chiral neutrino content, and the spin-statistics thermal integral from RS premises; none of that is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.