equilibrium_partition
plain-language theorem explainer
Equilibrium in the Recognition Science framework sets the J-cost of the unit state to zero, so the partition function equals one. Researchers deriving statistical mechanics from the Recognition functional equation cite this when establishing the equilibrium Boltzmann distribution. The proof is a direct one-line application of the Jcost unit lemma.
Claim. The Recognition Science cost function satisfies $J(1) = 0$, where $J(x) = (x-1)^2/(2x)$, implying the equilibrium partition function $Z = e^0 = 1$.
background
The Statistical Mechanics from RS module defines the partition function as $Z = sum exp(-J(state)/kT)$, with the equilibrium state (J=0) dominating the Boltzmann distribution. J-cost is the squared-ratio function $J(x) = (x-1)^2/(2x)$ from the Cost module. The upstream equilibrium theorem in NonlinearDynamicsFromRS records the same identity Jcost 1 = 0.
proof idea
The proof is a one-line wrapper that applies the Jcost_unit0 lemma, which reduces Jcost 1 to zero by direct simplification of the Jcost definition.
why it matters
This theorem supplies the equilibrium_zero field inside the statMechCert definition that certifies the five-ensemble structure. It closes the A1 foundation step where Z=1 at J=0, connecting to the Recognition Composition Law and the phi-ladder. No open questions are flagged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.