QCDCert
plain-language theorem explainer
QCDCert packages the Recognition Science counts of three colors, eight gluons, their product of twenty-four, and five QCD phases into one record structure. A physicist checking Standard Model group embeddings against the spatial dimension D would cite this when confirming the SU(3) adjoint and phase enumeration. The definition is a direct record constructor that assembles four equalities already fixed by sibling constant definitions and the Fintype instance on the phase inductive type.
Claim. The QCD certificate is the record type whose fields assert that the number of colors equals 3, the number of gluons equals 8, their product equals 24, and the cardinality of the set of five canonical QCD phases equals 5.
background
In the Quantum Chromodynamics from RS module, the number of colors is fixed at the constant 3 and identified with the spatial dimension D from the forcing chain. The number of gluons is fixed at that number squared minus one, reproducing the dimension of the adjoint representation of SU(3). QCDPhase is the inductive type with five constructors (hadronic, quark-gluon plasma, color superconductor, nuclear, vacuum) equipped with a Fintype instance whose cardinality is therefore 5. The module states that these relations hold by decide and that five phases equal configDim D = 5.
proof idea
The structure is introduced by declaring its four fields directly. No tactics or lemmas are applied inside the definition itself; the fields simply name the equalities and cardinality already established by the constant definitions for the number of colors and gluons together with the Fintype derivation on the phase inductive type.
why it matters
This structure supplies the bundled certificate consumed by the downstream qcdCert definition that assembles the QCD properties. It fills the Recognition Science derivation of the Standard Model by packaging the color count equal to D, the gluon count equal to 3 squared minus 1, and the five phases equal to configDim D. The placement aligns with the eight-tick octave and the forcing-chain step that sets D = 3, confirming the group structure without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.