GluonChannel
plain-language theorem explainer
GluonChannel enumerates the five canonical color channels for gluon exchanges arising from SU(3) in the Recognition Science model. QCD modelers verifying combinatorial counts of 24 color states from eight gluons would cite this enumeration when checking the configDim D = 5 relation. The declaration is a direct inductive type definition whose deriving clauses automatically supply decidable equality and finite cardinality.
Claim. The set of gluon channels is the finite type consisting of three color-antiquark states and two diagonal states, with cardinality 5.
background
In the Recognition Science treatment of gluon self-interactions the eight gluons of SU(3) satisfy 8 = N² - 1 with N = D = 3. The module records that eight gluons times three colors produces 24 states, equal to half the order of the binary tetrahedral group B₃. This inductive type isolates the five distinct exchange channels that realize the configuration dimension in the RS framework.
proof idea
The declaration is a direct inductive definition introducing five constructors. No lemmas are applied; the deriving clauses for DecidableEq, Repr, BEq, and Fintype are supplied automatically by Lean.
why it matters
This definition supplies the type whose cardinality is certified as 5 in the downstream gluonChannelCount theorem and the GluonCert structure. It fills the combinatorial step in the RS account of SU(3) self-interactions, where the five channels align with configDim D = 5 and the relation 8 = 3² - 1. The parent results use it to confirm the 24 color states without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.