qcdCert
plain-language theorem explainer
qcdCert bundles the RS-derived QCD counts into the QCDCert structure. Researchers extending the forcing chain to the Standard Model would cite it to certify the color and gluon numbers. The construction applies the equality lemmas directly in a record literal.
Claim. Define the structure QCDCert by the requirements colorCount = 3, gluonCount = 8, colorCount × gluonCount = 24, and |QCDPhase| = 5. Then qcdCert denotes the term satisfying these via the Recognition Science equalities colorCount = D and gluonCount = 3² - 1.
background
Recognition Science derives QCD from the unified forcing chain, where spatial dimension D = 3 fixes the number of colors. The gluon count follows as the dimension of the adjoint representation of SU(3), which is 8. QCDPhase enumerates the five canonical phases (hadronic, quark-gluon plasma, color-superconductor, nuclear, vacuum) whose count equals the configuration dimension 5. The upstream theorems establish colorCount = 3 by reflexivity from D = 3, gluonCount = 8 by direct computation, their product 24 by decision procedure, and the phase cardinality by decision. These are all proved without axioms or sorrys in the module.
proof idea
The definition constructs the QCDCert record by assigning each field to the corresponding equality theorem: color_3 to colorCount_eq_D, gluon_8 to gluonCount_eq_8, product_24 to color_times_gluon, and five_phases to qcdPhaseCount. This is a direct record literal that bundles the verified relations.
why it matters
This definition provides the certified QCD sector for the Recognition Science derivation of the Standard Model. It connects to the T8 step fixing D = 3 and the self-similar structure yielding the SU(3) generators. The module notes that the gluon confinement scale is expressed in RS units as m_W × φ^(-15). It serves as the interface for downstream checks on asymptotic freedom and confinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.