MatterPhase
plain-language theorem explainer
Recognition Science assigns five canonical condensed matter phases to configDim D = 5. The inductive definition enumerates these as solid, liquid, gas, plasma, and BEC, deriving finite type structure. Researchers constructing phase diagrams from the J-cost function reference this list when proving the five-phase cardinality. The definition is introduced directly without additional hypotheses.
Claim. The set of condensed matter phases is the finite collection $M = $ {solid, liquid, gas, plasma, BEC} equipped with decidable equality and cardinality 5.
background
In the Recognition Science treatment of condensed matter, five phases are distinguished: solid, liquid, gas, plasma, and Bose-Einstein condensate. This enumeration corresponds to configDim D = 5. Phase transitions occur when the J-cost of an order parameter crosses the canonical band value J(φ). The module also introduces five topological phases, yielding a total of ten phases equal to twice the configuration dimension. This setup adapts the chemistry module's phase diagram construction, which uses a similar inductive enumeration but lists supercritical fluid instead of BEC.
proof idea
The declaration is the inductive definition itself, which Lean automatically equips with DecidableEq, Repr, BEq, and Fintype instances.
why it matters
This definition supplies the matter phases for the CondensedMatterPhaseCert structure, which requires Fintype.card = 5 for matter phases together with the topological count and totalPhaseCount = 10. It fills the B9/B13 materials depth by linking phase count to configDim D = 5. The sibling totalPhaseCount definition then computes 5 + 5 = 10, consistent with the framework's assignment of configuration dimension for condensed matter.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.