qcdPhaseCount
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.