StatMechEnsemble
plain-language theorem explainer
Physicists reconstructing thermodynamics from the J-cost functional cite this enumeration to fix the configuration dimension at five. Recognition Science models equilibrium via the partition function Z = sum exp(-J/kT) with the J = 0 state dominating. The declaration introduces the five ensembles by direct inductive construction and derives Fintype to enable the subsequent cardinality theorem.
Claim. The statistical ensembles consist of the microcanonical ensemble, the canonical ensemble, the grand canonical ensemble, the NPT ensemble, and the NVE ensemble.
background
The module Statistical Mechanics from RS posits that macroscopic behavior follows from microscopic states through the partition function Z = Σ exp(-J(state)/kT). At equilibrium the minimum-cost state with J = 0 dominates, yielding Z = 1. Five ensembles are introduced to realize configDim D = 5.
proof idea
The declaration is a direct inductive definition with five constructors that automatically derives DecidableEq, Repr, BEq and Fintype instances.
why it matters
StatMechCert requires this enumeration to assert Fintype.card = 5 together with the equilibrium condition Jcost 1 = 0. The definition supplies the finite set needed for the partition-function identity Z = exp(0) = 1 and aligns the ensemble count with the five-dimensional configuration space of the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.