matterPhaseCount
plain-language theorem explainer
The declaration fixes the cardinality of the canonical condensed matter phases at five, matching the configuration dimension D = 5 in the Recognition Science model. Researchers constructing phase diagrams from the J-cost function cite this count when enumerating solid, liquid, gas, plasma, and BEC states. The proof is a one-line decision tactic that exhausts the constructors of the inductive phase type.
Claim. The set of canonical condensed matter phases consisting of solid, liquid, gas, plasma, and Bose-Einstein condensate has cardinality five: $|M| = 5$ where $M$ denotes that set.
background
The Condensed Matter Phases from RS module defines an inductive type MatterPhase with exactly the constructors solid, liquid, gas, plasma, and BEC. This enumeration is stated to equal the configuration dimension D = 5. Phase transitions arise when the J-cost of an order parameter crosses the canonical band J(φ). The upstream inductive definition in Chemistry.PhaseDiagramTripleFromJCost lists a parallel but distinct set that substitutes supercritical fluid for BEC.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the Fintype.card equality for the inductive MatterPhase type.
why it matters
This result supplies the five_matter component inside the condensedMatterPhaseCert definition, which assembles the matter and topological counts to certify a total of ten phases. It implements the module claim that five matter phases plus five topological phases equal 2 times configDim D. The cardinality anchors the phase enumeration derived from the J-cost function within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.