bosonic_dof_eq
plain-language theorem explainer
The total bosonic relativistic degree-of-freedom count equals 28. Cosmology and Standard-Model g_* certificates cite this equality when assembling g_* = 106.75 from bosonic plus Fermi-weighted fermionic pieces. The proof is a one-line native decision on the closed arithmetic definition (equivalently the D-polynomial 4D²−2D−2 at D=3).
Claim. The bosonic degree-of-freedom count equals $28$. Equivalently, at spatial dimension $D=3$, the D-flavored polynomial identity $4D^2-2D-2=28$ holds. The count packages the usual high-temperature Standard Model bosonic tally (gauge polarizations plus Higgs) and is not claimed as an RS derivation of that spectrum.
background
Module FermionDOFGapBridge records kernel-checked arithmetic identities that relate imported Standard Model degree-of-freedom counts to D=3 combinatorial quantities. After external review it explicitly does not claim to derive the SM spectrum: gauge representations, the Higgs doublet, and thermal weights are imported physics; RS contributes D=3 (T8 / DimensionForcing), the eight-tick period 2^D=8, and the generation count 3.
Upstream, Cosmology.GStarDerivation defines the bosonic tally as gauge DOF plus Higgs DOF and already records the standard value 28. Sibling constants in this module include D:=3, eightTick:=8, and dimensionGap, used to re-express fermionic and weight identities in D-flavored form. The local bosonic statement is the matching closed count (or the polynomial 4D²−2D−2 evaluated at D=3).
The honest split in the module doc: proved here are exact equalities such as 28+(7/8)×90=106.75; not proved are the representation content or the Fermi–Dirac integral that supplies the 7/8 weight.
proof idea
One-line tactic proof: native_decide evaluates the closed natural-number definition of the bosonic count (or the polynomial 4D²−2D−2 at the concrete D=3) and confirms equality with 28. No lemmas are unfolded in this wrapper; the parallel Cosmology proof instead unfolds gauge_dof, gauge_generators, gauge_polarisations, and higgs_dof before decide. Here the kernel simply decides the arithmetic.
why it matters
This equality is a leaf in every g_* certificate that assembles the high-temperature relativistic DOF total. Downstream it is referenced by Cosmology.GStarDerivation.gStarDerivationCert (field bosonic), by StandardModel.RelativisticDOF.gStarCert, g_star_derived_eq (rewrite to reach 106.75), g_star_dirac_eq, and bosonic_traces_to_Q3 (which packages gluon adjoint data with bosonic_dof=28). Inside this module it feeds g_star_D3_eq.
Framework role is narrow but load-bearing for the unification/cosmology bridge: T8 forces D=3, and the eight-tick octave is 2^D; the bosonic 28 is the imported partner to the D-flavored fermionic and weight identities (90=2×dimensionGap(3), 7/8=(2^D−1)/2^D). The module doc is explicit that packaging 28 as 4D²−2D−2 does not derive SM boson content from RS premises—an open task remains deriving gauge reps, Higgs, and the thermal integral from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.