statMechEnsembleCount
plain-language theorem explainer
The declaration proves that the inductive type of statistical ensembles in the Recognition Science framework has finite cardinality exactly five. Researchers deriving thermodynamics from the J-cost functional equation would cite this when fixing the configuration dimension for the partition function at equilibrium. The proof is a one-line decision procedure that enumerates the five constructors via the derived Fintype instance.
Claim. Let StatMechEnsemble be the inductive type generated by the constructors microcanonical, canonical, grandCanonical, NPT, and NVE. Then its Fintype cardinality satisfies $Fintype.card(StatMechEnsemble) = 5$.
background
The module Statistical Mechanics from RS derives macroscopic behavior from microscopic states using the partition function $Z = sum exp(-J(state)/kT)$. At equilibrium the $J=0$ state dominates, so $Z=1$. The module introduces five canonical ensembles (microcanonical, canonical, grand canonical, NPT, NVE) that realize the configuration dimension $D=5$ in the RS-native setting.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This tactic evaluates the cardinality directly from the Fintype instance automatically derived for the inductive type StatMechEnsemble together with its DecidableEq instance.
why it matters
The result populates the five_ensembles field of the StatMechCert structure, which also records equilibrium_zero and off_equil_positive. It supplies the concrete count required by the module's claim that five ensembles arise from the RS partition function at $J=0$, closing the finite-type foundation for statistical mechanics without additional axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.