gluonChannelCount
plain-language theorem explainer
The theorem establishes that the inductive type of gluon channels has cardinality five, matching the five canonical color exchange channels in the RS model of SU(3) self-interactions. QCD theorists deriving vertex structures from D = 3 would cite this count when building the gluonCert certificate. The proof is a one-line wrapper that invokes the decide tactic on the Fintype instance of the five-constructor inductive type.
Claim. The finite type of gluon channels has cardinality five: $|$GluonChannel$| = 5$, where GluonChannel is the inductive type whose constructors are the three color-antiquark channels and two diagonal channels.
background
The module on Gluon Self-Interaction from RS derives the eight gluons of SU(3) as $N^2 - 1$ with $N = D = 3$. The referenced GluonChannel inductive type enumerates five cases (colorAntiquark1, colorAntiquark2, colorAntiquark3, diagonal1, diagonal2), each deriving DecidableEq, Repr, BEq, and Fintype. Module documentation states that this yields five canonical gluon exchange channels equal to configDim D = 5, with the upstream inductive definition supplying the Fintype instance used for the cardinality claim.
proof idea
The proof is a one-line wrapper that applies the decide tactic to compute Fintype.card directly from the five constructors of the inductive GluonChannel type.
why it matters
This result supplies the five_channels field inside the gluonCert definition, which assembles the gluon count of eight, the 24 color product, the B3 half, and the five channels. It closes the combinatorial step linking gluon self-interactions to the forcing chain at T8 (D = 3) and the eight-tick octave. Module documentation ties the count to |B3|/2 = 24 for color combinations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.