qcdPhaseCount
The theorem asserts that the finite type QCDPhase has cardinality exactly 5. Researchers deriving QCD phase structure from Recognition Science would cite it to confirm that the five phases arise as the configuration dimension D. The proof is a one-line decision procedure that exhausts the constructors of the inductive type.
claimThe cardinality of the finite type QCDPhase equals 5, where QCDPhase is the inductive type whose constructors are the phases hadronic, quark-gluon plasma, color-superconductor, nuclear, and vacuum.
background
The module derives QCD properties directly from Recognition Science, with 3 colors fixed to the spatial dimension D and 8 gluons fixed to 3²-1. The inductive type QCDPhase enumerates the five canonical phases hadronic, quark-gluon plasma, color-superconductor, nuclear, and vacuum, whose count is identified with configDim D = 5. The upstream inductive definition supplies the DecidableEq, Repr, BEq, and Fintype instances used by the cardinality computation.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic uses the derived Fintype instance on QCDPhase to enumerate the five constructors and return the cardinality 5.
why it matters in Recognition Science
The result supplies the five_phases field inside the QCDCert definition, which aggregates the RS-derived QCD invariants (color count, gluon count, and phase count). It closes the enumeration step that matches the phase count to configDim D = 5, consistent with the forcing chain step T8 that sets D = 3. No open scaffolding or unresolved questions are indicated for this declaration.
scope and limits
- Does not derive dynamical phase transitions or critical temperatures.
- Does not compute the gluon confinement scale or coupling running.
- Does not connect the phases to the phi-ladder mass formula.
- Does not address confinement or asymptotic freedom beyond the phase list.
Lean usage
def qcdCert : QCDCert where color_3 := colorCount_eq_D gluon_8 := gluonCount_eq_8 product_24 := color_times_gluon five_phases := qcdPhaseCountformal statement (Lean)
37theorem qcdPhaseCount : Fintype.card QCDPhase = 5 := by decide
proof body
38