phaseCount
plain-language theorem explainer
The theorem fixes the number of canonical matter phases at five in the Recognition Science chemistry model. A condensed-matter theorist or chemist working on J-cost phase diagrams would cite the cardinality when certifying triple-point equilibria or enumerating states in the configDim D = 5 setting. The proof is a one-line decision procedure that exhausts the finite inductive type.
Claim. The finite type of matter phases has cardinality five: there are exactly five phases (solid, liquid, gas, plasma, supercritical).
background
The module treats the triple point as the unique recognition equilibrium where J-cost reaches its global minimum simultaneously for solid, liquid and gas phases, so that J(r) = 0 for each. MatterPhase is the inductive type whose five constructors enumerate the canonical states and derive Fintype, DecidableEq and Repr. The local setting therefore equates five phases with configDim D = 5, restricting the triple-point analysis to the first three of them.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. The tactic succeeds because the inductive definition of MatterPhase derives a Fintype instance, allowing exhaustive enumeration of the five constructors.
why it matters
The cardinality supplies the five_phases field of the downstream phaseDiagramCert definition, which certifies the overall phase-diagram structure. It directly encodes the framework claim that five phases realize configDim D = 5, consistent with the eight-tick octave (T7) and the forcing chain to D = 3 spatial dimensions. The module records zero sorrys, closing the enumeration step for triple-point work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.