equilibrium_entropy
plain-language theorem explainer
Defines equilibrium entropy of an N-entry ledger at conserved energy σ as S_eq(σ) = N · J_log(σ/N) = N(cosh(σ/N) − 1). Thermodynamic derivations in the Foundation module cite this as the closed-form S(E) curve at the variational minimizer. The body is a one-line composition of the log-coordinate J-cost with the intensive energy density σ/N.
Claim. For $N \in \mathbb{N}$ and conserved energy $\sigma \in \mathbb{R}$, the equilibrium entropy is $S_{\mathrm{eq}}(N,\sigma) := N \, J_{\log}(\sigma/N)$, where $J_{\log}(t) = \cosh t - 1$. Equivalently $S_{\mathrm{eq}}(N,\sigma) = N(\cosh(\sigma/N) - 1)$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and finite observer resolution. Entropy of a configuration is the total defect $\sum_i J(x_i)$ (InitialCondition); energy is the conserved log-charge $\sum_i \log x_i$ (VariationalDynamics). Temperature is not a ledger property: it is the Lagrange multiplier for an observer who sees only $K < N$ entries and treats the rest as a heat bath.
$J_{\log}$ is the cost in log coordinates: $J_{\log}(t) = \cosh t - 1$, a convex bowl minimized at $t = 0$ (DiscretenessForcing; ContinuumBridge). At recognition equilibrium the forced dynamics conserve $\sigma$ and strictly decrease level variance until consensus (RecognitionEquilibrium). The equilibrium configuration is therefore fixed by $\sigma$ alone, so entropy collapses to a function of $(N,\sigma)$ only.
Sibling quantities include the general RS entropy/energy maps and the equilibrium entry value; this definition specializes entropy to that equilibrium slice.
proof idea
Definitional one-liner: unfold to $N \cdot J_{\log}(\sigma/N)$. No tactics. The identity $S_{\mathrm{eq}} = N(\cosh(\sigma/N)-1)$ is immediate from $J_{\log}(t) = \cosh t - 1$ and is recorded separately as equilibrium_entropy_eq.
why it matters
This is the closed-form $S(E)$ that makes RS thermodynamics calculable. Downstream, equilibrium_entropy_eq rewrites it in cosh form; equilibrium_entropy_nonneg and equilibrium_entropy_zero_iff give $S \ge 0$ with equality iff $\sigma = 0$ (third-law ground state). Differentiating yields the first law: $dS_{\mathrm{eq}}/d\sigma = \sinh(\sigma/N) = T$ (first_law_derivative, first_law). The Boltzmann weight at equilibrium is $\exp(-S_{\mathrm{eq}})$ (boltzmann_at_equilibrium), and the module certificate packages these facts.
In the broader framework the definition sits on T5 J-uniqueness ($J(x) = (x+x^{-1})/2-1 = \cosh(\log x)-1$) and the variational dynamics that force a unique equilibrium at fixed $\sigma$. It closes the gap named in the module doc: without $S_{\mathrm{eq}}(\sigma)$ there is no $T = \partial E/\partial S$ contact with classical thermodynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.