statMechCert
plain-language theorem explainer
statMechCert assembles the five-ensemble cardinality with the J-cost zero at unity and strict positivity off unity into the StatMechCert structure. Researchers extracting thermodynamics from the Recognition Science J-functional equation would cite it to certify the partition function equals 1 at equilibrium. The definition is a direct record construction that reuses the decide tactic for the ensemble count and prior Jcost lemmas for the cost axioms.
Claim. Let StatMechCert be the structure asserting that the set of statistical mechanics ensembles has cardinality 5, that the J-cost of the unit state satisfies $J(1)=0$, and that $J(r)>0$ for every real $r>0$ with $r≠1$. Then statMechCert is the instance of this structure obtained by supplying the ensemble count, the equilibrium zero, and the off-equilibrium positivity.
background
Statistical mechanics in Recognition Science derives macroscopic behavior from the partition function $Z=∑exp(-J(state)/kT)$, where J is the cost function obeying the Recognition Composition Law. At equilibrium the J=0 state dominates, forcing Z=1. The module treats the five canonical ensembles (microcanonical, canonical, grand canonical, NPT, NVE) as a direct consequence of configDim D=5.
proof idea
The definition builds the StatMechCert record by assigning the five_ensembles field to statMechEnsembleCount, the equilibrium_zero field to equilibrium_partition, and the off_equil_positive field to off_equilibrium_cost. Each field is supplied by an upstream theorem; no additional tactics are applied beyond the record constructor.
why it matters
This definition certifies the statistical-mechanics layer of the RS framework by packaging the ensemble count with the J-cost equilibrium properties. It directly supports the module claim that Z=exp(0)=1 at equilibrium and that off-equilibrium states carry positive cost. The construction aligns with the five-ensemble requirement tied to the forcing-chain dimension count, though no downstream theorems yet consume the certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.