partition_from_ledger_sum
plain-language theorem explainer
The partition function in Recognition Science is the sum over ledger states of exp(-J_cost(s) / k_B T). Researchers connecting statistical mechanics to the RS ledger structure would cite this link when deriving free energy and entropy. The proof is a one-line term that applies trivial to assert the relation.
Claim. $Z = sum_{s} exp(-J(s) / k_B T)$, where the sum runs over ledger states $s$ and $J$ is the canonical cost function $J(x) = (x + x^{-1})/2 - 1$.
background
The module THERMO-002 derives the partition function from RS ledger structure. Z encodes free energy via $F = -k_B T ln Z$, average energy via the beta derivative, and entropy via $S = k_B (ln Z + beta
proof idea
The proof is a one-line term that applies trivial.
why it matters
This result supplies the ledger-to-partition bridge inside the thermodynamics module and aligns with the J-cost definition from CondensedMatter.JCostPhaseTransition. It supports later siblings such as freeEnergy and entropy while remaining consistent with the forcing chain steps that fix J-uniqueness and the phi ladder. No downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.