StatMechCert
plain-language theorem explainer
StatMechCert bundles three properties certifying the RS derivation of statistical mechanics: exactly five ensembles, vanishing J-cost at unit ratio, and strict positivity of J-cost off equilibrium. A researcher building thermodynamics from the Recognition Science functional equation would cite it to confirm ensemble count equals configuration dimension D=5 and equilibrium dominance by the J=0 state. The definition is a direct structure whose fields are assigned from upstream cardinality and J-cost lemmas.
Claim. A certificate structure asserts that the set of statistical ensembles has cardinality 5, that the J-cost function satisfies $J(1)=0$, and that $J(r)>0$ for every $r>0$ with $r≠1$.
background
Recognition Science obtains statistical mechanics by treating the J-cost function as the effective energy in the partition function $Z=∑exp(-J(state)/kT)$. Equilibrium occurs when the J=0 state dominates, forcing $Z=1$. The module defines five canonical ensembles (microcanonical, canonical, grand canonical, NPT, NVE) whose count is identified with configuration dimension D=5.
proof idea
This is a structure definition. Its three fields are populated directly by the ensemble cardinality lemma, the equilibrium partition result, and the off-equilibrium positivity lemma.
why it matters
StatMechCert supplies the certified properties consumed by the downstream statMechCert definition. It anchors the statistical mechanics layer to the J-cost theorems from EntropyArrowFromJCost and the five-ensemble enumeration, confirming alignment with the RS configuration dimension and the equilibrium condition J=0. This step closes the foundation for macroscopic thermodynamics without extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.