su3_adjoint
plain-language theorem explainer
The adjoint representation of SU(3) has dimension 8. Anyone assembling the high-temperature SM bosonic degree-of-freedom count (gluons, then g_b and g_star) cites this equality. The proof is a one-line native decision of the arithmetic 3² − 1 = 8.
Claim. The adjoint dimension of $SU(3)$ equals $8$: if the adjoint dimension of $SU(n)$ is defined by $n^2-1$, then $3^2-1=8$.
background
This module performs exact rational bookkeeping for the high-temperature Standard Model relativistic degree count $g_\star=g_b+(7/8)g_f=106.75$, valid only for $T\gtrsim T_{\mathrm{EW}}$. Status is bookkeeping over adopted SM content, not a novel RS prediction.
The adjoint dimension of $SU(n)$ is the elementary formula $n^2-1$. For color, $n=3$, so the gluon multiplet sits in an 8-dimensional adjoint. Upstream, RS supplies the gauge factor $SU(3)$ from $Q_3$ automorphisms (GaugeFromCube) and three generations from $D=3$; the matter representation content itself is imported SM data.
Sibling definitions package gluon DOF as twice the adjoint dimension (two helicities) and fold that into the total bosonic count $g_b=28$.
proof idea
One-line wrapper: native_decide evaluates the closed arithmetic $3^2-1=8$ on the definition of adjoint dimension. No lemmas beyond that definition are required.
why it matters
Feeds bosonic_traces_to_Q3, which packages the claim that each bosonic DOF traces to $Q_3$ structure: gluon DOF equals adjoint dimension of the color fundamental times two, that adjoint dimension is 8, and total bosonic DOF is 28. Without fixing adjoint dimension at 8, the gluon contribution (16) and the textbook $g_b=28$ do not close in Lean.
In the RS forcing chain this sits downstream of gauge-from-cube ($SU(3)\times SU(2)\times U(1)$) and the $D=3$ generation count; it does not itself re-derive those landmarks. It is the arithmetic hinge between the color layer and the assembled high-$T$ $g_\star$ ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.