su2_adjoint
plain-language theorem explainer
The adjoint representation of SU(2) has dimension 3, i.e. 2²−1=3. Anyone assembling weak-boson or g★ bookkeeping in the high-T SM count cites this. The proof is a one-line native evaluation of the adjoint-dimension formula.
Claim. The adjoint dimension of $SU(2)$ equals $3$: if $\mathrm{adj}(n)=n^2-1$, then $\mathrm{adj}(2)=3$.
background
This module performs exact rational bookkeeping for the high-temperature Standard Model relativistic degree-of-freedom 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.
RS supplies the gauge factor $SU(3)\times SU(2)\times U(1)$ from cube automorphisms and the generation count 3 from $D=3$. The adjoint-dimension helper is the elementary formula $\mathrm{adj}(n)=n^2-1$. Matter representations, the $7/8$ thermal weight, and the high-$T$ scope are imported standard physics.
Upstream, the same formula is used for gluons ($8\times 2$ DOF above $T_{\mathrm{QCD}}$) and for the SU(3) adjoint count; the present fact is the SU(2) twin.
proof idea
One-line tactic proof: native_decide evaluates the closed formula $\mathrm{adj}(2)=2^2-1$ in the natural numbers and checks equality with 3. No lemmas beyond the definition of adjoint dimension are required.
why it matters
Closes the SU(2) side of the gauge-boson dimension table needed for bosonic $g_b$ in the $g_\star=106.75$ assembly. Sibling facts cover SU(3) adjoint dimension 8 and the polarization-weighted weak-boson and gluon DOF. In the RS chain the group $SU(2)$ itself is forced by Q₃ automorphisms (GaugeFromCube); this lemma only converts that group label into the integer dimension used by thermal counting. No downstream theorems currently depend on it in the graph, but the module’s weak-boson and total bosonic DOF identities are the natural consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.