gluon_dof
plain-language theorem explainer
Gluon degrees of freedom are written as twice the SU(D) adjoint dimension at the forced spatial dimension D = 3, i.e. 2(D² − 1) = 16. Anyone assembling the high-T bosonic count for g_* or certifying the SM DOF ledger cites this. It is a one-line definition that re-expresses the imported 8×2 gluon count in D-flavored notation.
Claim. Define the gluon degree-of-freedom count by $2(D^2-1)$, where $D=3$ is the forced spatial dimension. At $D=3$ this equals $2(9-1)=16$, matching eight SU(3) adjoint generators times two massless polarizations.
background
This module records exact arithmetic identities that rewrite imported Standard Model degree-of-freedom counts in D-flavored notation. After external review it explicitly does not claim to derive the SM spectrum: gauge representations, Higgs content, and thermal weights remain imported physics; only the equalities among the resulting integers are kernel-checked here.
The local constant $D$ is the spatial dimension forced by T8 (DimensionForcing), fixed at $3$. The eight-tick period $2^D=8$ and the generation count $3$ are likewise upstream RS results cited, not re-proved. Sibling definitions package fermionic and bosonic totals from the same $D$.
Upstream, StandardModel.RelativisticDOF already defines the gluon count as $\mathrm{adjoint_dim}(3)\times 2$. The present definition is the parallel bridge form $2(D^2-1)$, which is the adjoint dimension of SU(D) times two polarizations evaluated at that forced $D$.
proof idea
One-line definition: the natural number is set equal to $2(D^2-1)$ with $D:=3$ in-module. No tactics or lemmas; evaluation is immediate arithmetic once $D$ is substituted. Equality to $16$ is discharged downstream by native_decide (or rfl) in the companion gluon_dof_eq theorems.
why it matters
This is the gluon term in the high-T bosonic ledger. Downstream, local and SM-side bosonic_dof sum it with electroweak and Higgs pieces to the standard $28$; gluon_dof_eq pins the value at $16$; bosonic_traces_to_Q3 packages the adjoint and total as Q₃ structure facts; and GStarCert requires gluons : gluon_dof = 16 as one certificate field for the $g_*=106.75$ assembly.
In the Recognition framework it sits under the honest split of the module: T8 forces $D=3$, so the SU(D) adjoint formula collapses to the familiar eight generators, but the choice of color SU(3) and the representation assignments remain imported SM content. The identities proved here (including $28+(7/8)\times 90=106.75$) are exact re-expressions, not a first-principles derivation of the gauge group or of $g_*$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.