g_star_via_gap
plain-language theorem explainer
High-temperature effective DOF count equals bosonic DOF plus the Fermi–Dirac weight times twice the dimension gap: g_* = 28 + (7/8)(2×45). Cosmologists auditing the RS g_* arithmetic cite this gap-flavored rewrite of the standard 28+(7/8)×90 identity. Proof unfolds g_star_D, substitutes the twice-gap identity for fermionic DOF, and closes by ring.
Claim. With spatial dimension $D=3$, the high-temperature effective relativistic DOF count satisfies $g_*(D)=N_b+w_{FD}(D)\cdot(2\,\Delta(D))$, where $N_b$ is the imported bosonic count (28), $w_{FD}(D)=(2^D-1)/2^D$ is the Fermi–Dirac thermal weight, and $\Delta(D)=D^2(D+2)$ is the dimension gap (so $\Delta(3)=45$).
background
This module records exact arithmetic identities linking imported Standard Model relativistic DOF counts to D=3 combinatorial quantities. Per the module status note, it does not derive the SM spectrum: gauge representations, Higgs content, neutrino convention (g_f=90), and the 7/8 Fermi–Dirac integral are imported physics; D=3, the eight-tick period 2^D, and generation count 3 are cited from upstream RS forcing (T8 and related).
The dimension gap is the polynomial $\Delta(D)=D^2(D+2)$, equal to 45 at D=3. Bosonic DOF is the standard high-T count 28 (gauge plus Higgs). The Fermi–Dirac weight at D is $(2^D-1)/2^D$, which is 7/8 when D=3. The sibling identity fermionic_dof = 2·Δ(D) rewrites the imported 90 as twice the gap.
The assembled target is the textbook high-T value g_*=106.75. This declaration is the gap-flavored packaging of that sum: bosons plus weight times twice the gap, rather than bosons plus weight times fermionic DOF.
proof idea
Term/tactic hybrid, four steps. Unfold the definition of g_star_D (which is bosonic plus weight times fermionic DOF). Invoke the sibling lemma that fermionic DOF equals twice the dimension gap. push_cast rewrites the natural-number identity into the real expression appearing in the goal. ring closes the remaining polynomial equality. No external analysis; pure substitution and arithmetic.
why it matters
Sits in the honest post-review layer of Unification.FermionDOFGapBridge: machine-checked re-expression of known DOF arithmetic in D-flavored notation, not an RS derivation of g_*=106.75. The doc-comment states the concrete form 28+(7/8)(2×45) and ties it to fermionic_dof_eq_twice_gap.
Framework landmarks in view are T8 (D=3 spatial dimensions) and the eight-tick octave 2^D=8, which make the weight (2^D−1)/2^D and the gap polynomial evaluate to the familiar 7/8 and 45. Downstream use count is presently zero; the lemma is a citation-ready alternate face of the assembled g_* identity for anyone preferring gap language over raw fermionic DOF.
The module header is explicit about the open gap: turning this into a true RS derivation would require deriving SM representations, Higgs, chiral neutrinos, and the thermal spin-statistics integral from RS premises. None of that is claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.