gluon_dof_eq
plain-language theorem explainer
Gluon degrees of freedom equal 16 under the module's imported SM bookkeeping. Anyone assembling the high-T effective count g_* cites this equality. The proof is a one-line native_decide check that the closed arithmetic definition evaluates to 16.
Claim. The gluon degree-of-freedom count equals $16$ (eight $SU(3)$ generators times two transverse polarizations, as imported Standard Model content).
background
This module records exact arithmetic identities that rewrite imported Standard Model relativistic degree-of-freedom counts in $D$-flavored notation. Per the module status note, it does not derive the SM spectrum: gauge representations, polarizations, and the high-$T$ scope of $g_*$ are imported physics; only the numerical identities are kernel-checked here.
Upstream RS facts used as ambient constants include spatial dimension $D = 3$ (T8 / DimensionForcing) and the eight-tick period $2^D = 8$. Those fix the combinatorial scaffolding elsewhere in the file (generation count, dimension gap, fermionic tally). The gluon count itself is the standard QCD entry: eight massless vector bosons, each with two helicities, totaling 16.
Sibling identities in the same bridge (fermionic DOF, Fermi–Dirac weight $7/8$, assembled $g_* = 106.75$) follow the same pattern: re-expression after the target number is known, not a first-principles derivation of that number.
proof idea
One-line tactic proof: native_decide. The definition of the gluon DOF quantity is a closed natural-number expression; the kernel evaluates it and confirms equality with 16. No lemmas are invoked.
why it matters
Feeds the Standard Model relativistic DOF layer: the twin gluon_dof_eq there and the certificate gStarCert, which packages bosonic, fermionic, generation, color, and gluon equalities into one $g_*$ witness. In the Recognition framework this sits on the honest side of the derived-vs-imported split after the 2026-06-25 rescope: $D = 3$ and the eight-tick octave are RS-forced (T7–T8), but the gluon representation content is not. The identity is still required so downstream cosmology and unification tallies can cite a proved numeral rather than an opaque constant. It does not close the open gap of deriving $SU(3)$ gauge structure from RS premises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.