pith. machine review for the scientific record. sign in
def definition def or abbrev high

gluonCount

show as:
view Lean formalization →

gluonCount computes the gluon multiplicity for the SU(3) color sector as rank cubed minus one, yielding eight. Researchers deriving QCD from the Recognition Science forcing chain cite this when counting the eight adjoint bosons of the color group. The definition is a direct arithmetic substitution of the constant rank value three.

claimThe gluon multiplicity equals $3^2 - 1 = 8$, where the rank of SU(3) is fixed at three.

background

The Standard Model Group Structure module decomposes the gauge group into SU(3) for color, SU(2) for weak isospin, and U(1) for hypercharge, with ranks adding to six. rankSU3 is defined as the constant three, matching the spatial dimension D from the forcing chain. Upstream, the gluonCount definition in QuantumChromodynamicsFromRS uses the same formula with colorCount set to three.

proof idea

One-line definition that substitutes the upstream rankSU3 constant into the adjoint-dimension formula N squared minus one.

why it matters in Recognition Science

This supplies the gluon count of eight that enters QCDCert, gluon_count, color_times_gluon, and totalCarriers. It completes the SU(3) factor in the rank decomposition of the SM gauge group, consistent with T8 (D=3) and the eight-tick octave. Downstream results use it to certify the product colorCount times gluonCount equals twenty-four.

scope and limits

formal statement (Lean)

  37def gluonCount : ℕ := rankSU3 ^ 2 - 1

used by (8)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.