bosonic_traces_to_Q3
plain-language theorem explainer
Packages three equalities that pin the high-T bosonic SM count to the Q₃ color layer: gluon helicities equal twice the SU(3) adjoint dimension, that adjoint dimension is 8, and the total bosonic DOF is 28. Anyone assembling g_★ = 106.75 from RS-sourced gauge data cites this. The proof is a three-component term that applies reflexivity, the SU(3) adjoint lemma, and the already-proved bosonic total.
Claim. Gluon degrees of freedom equal twice the adjoint dimension of the color layer's fundamental representation dimension; that adjoint dimension is $8$; and the total bosonic relativistic DOF above the electroweak scale is $28$.
background
This module performs textbook high-temperature SM bookkeeping for $g_\star = g_b + (7/8)g_f = 28 + (7/8)\cdot 90 = 106.75$, valid only for $T \gtrsim T_{\mathrm{EW}}$. RS supplies the gauge group $\mathrm{SU}(3)\times\mathrm{SU}(2)\times\mathrm{U}(1)$ from $Q_3$ automorphisms (GaugeFromCube) and the generation count $3$ from $D=3$; matter representations and the $7/8$ thermal weight are imported standard physics.
The color layer is the SU(3) gauge layer extracted from the cube group $B_3$, with fundamental representation dimension $3$. The adjoint dimension of $\mathrm{SU}(n)$ is $n^2-1$, so the color adjoint is $8$. Local bosonic DOF is the sum of gluon, symmetric-phase weak-boson, and Higgs contributions; the companion equality already states that total is $28$. Cosmology.GStarDerivation carries the parallel global definition (gauge plus Higgs) with the same total.
proof idea
Term-mode triple constructor. The first conjunct is definitional equality (rfl): gluon DOF is written as adjoint dimension of the color fundamental times two polarizations. The second is the sibling lemma su3_adjoint, which evaluates $\mathrm{adjoint_dim}(3)=8$. The third reuses the already-proved local bosonic_dof_eq (native decision after unfolding gluons, weak bosons, and Higgs). No new arithmetic is performed here; the theorem only bundles the three facts under the Q₃-tracing claim.
why it matters
Closes the bosonic half of the module's "each DOF traces to $Q_3$ structure" narrative: color comes from the cube gauge layer (T8 / GaugeFromCube), adjoint dimension is forced by $n=3$, and the total $g_b=28$ is the standard high-T input to $g_\star=106.75$. Downstream assembly of $g_\star$ (and the cosmology GStar path) needs this certified link between RS-sourced SU(3) and the textbook bosonic count. No used_by edges are recorded yet; the companion fermionic-trace statement sits immediately below. Status remains bookkeeping over adopted SM content, not a novel mass or coupling prediction. Framework landmarks touched: gauge-from-cube and $D=3$ forcing of the color layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.