QCDPhase
QCDPhase enumerates the five canonical QCD phases in the RS setting as hadronic, quark-gluon plasma, color-superconductor, nuclear, and vacuum. Researchers deriving strong-interaction properties from the forcing chain cite this enumeration to fix phase cardinality at five, matching configDim D. The inductive declaration installs Fintype automatically, so the sibling cardinality result follows by decision procedure.
claimThe type of QCD phases is the inductive type whose constructors are the states hadronic, quark-gluon plasma, color superconductor, nuclear, and vacuum, equipped with decidable equality, representation, boolean equality, and finite-type structure.
background
In the Quantum Chromodynamics from RS module, three colors equal spatial dimension D and eight gluons equal three squared minus one. The upstream vacuum definition from Yang-Mills mass gap is the gauge bond configuration with all bonds at rung zero. This inductive type lists the five phases whose cardinality is asserted to equal configDim D.
proof idea
Direct inductive definition of the five phases. The deriving clause installs DecidableEq, Repr, BEq, and Fintype instances with no additional tactics or lemmas. The resulting Fintype structure supports the one-line cardinality theorem proved by decide in the sibling declaration.
why it matters in Recognition Science
QCDPhase supplies the phase set for the QCDCert structure that certifies color count three, gluon count eight, product twenty-four, and phase count five. It realizes the module claim that five phases equal configDim D, completing the enumeration step in the RS-derived QCD model. The construction is consistent with the framework's eight-tick octave and D equals three spatial dimensions.
scope and limits
- Does not derive transition temperatures or critical points between phases.
- Does not assign J-cost or defect distances to individual phases.
- Does not prove dynamical stability from the Recognition Composition Law.
- Does not connect phases to mass rungs on the phi-ladder.
formal statement (Lean)
33inductive QCDPhase where
34 | hadronic | quarkGluonPlasma | colorSuperconductor | nuclear | vacuum
35 deriving DecidableEq, Repr, BEq, Fintype
36