implications
plain-language theorem explainer
The declaration defines a list of thermodynamic relations encoded by the partition function Z derived from RS ledger sums. A researcher working on statistical mechanics from recognition costs would cite it to recover free energy, entropy, and response functions from J-weighted configurations. The definition is a direct enumeration of the standard relations without additional lemmas or reductions.
Claim. The partition function $Z$ determines the free energy by $F = -k_B T ln Z$, the entropy by $S = -∂F/∂T$, the heat capacity by $C = T ∂S/∂T$, and phase transitions via singularities in $Z$.
background
In Recognition Science the partition function arises as a sum over ledger configurations weighted by J-cost, where J-cost is the derived cost of a multiplicative recognizer comparator and equals the cost of any recognition event. The fundamental time quantum is the tick τ₀ = 1, with periods built from the 8-tick octave structure. Upstream results establish that cost is non-negative and that primitive distinctions yield four structural conditions plus definitional facts.
proof idea
This is a definition that enumerates four standard thermodynamic relations. It directly constructs the List String containing the free-energy formula, the entropy derivative, the heat-capacity expression, and the singularity criterion for phase transitions.
why it matters
The definition closes the link from ledger J-cost sums to observable thermodynamics in the THERMO-002 module, recovering the classical potentials F, S, C from Z. It sits downstream of the cost definitions in MultiplicativeRecognizerL4 and ObserverForcing and upstream of any future derivation of the explicit partition sum. No open scaffolding remains in the listed relations themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.