equilibrium_entropy_nonneg
plain-language theorem explainer
Equilibrium entropy S_eq(N,σ) = N·J_log(σ/N) is nonnegative for every particle count N and conserved energy σ. Thermodynamic and ledger arguments that treat S_eq as a Lyapunov or free-energy ingredient cite this bound. The proof unfolds the definition and multiplies nonnegativity of N by J_log_nonneg.
Claim. For every natural number $N$ and real conserved energy $\sigma$, the equilibrium entropy $S_{\mathrm{eq}}(N,\sigma) := N\, J_{\log}(\sigma/N)$ satisfies $S_{\mathrm{eq}}(N,\sigma)\ge 0$. Equivalently, $N(\cosh(\sigma/N)-1)\ge 0$.
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$. Equilibrium entropy packages the equal-share ground state: with $N$ entries and total energy $\sigma$, each entry carries $\sigma/N$, so $S_{\mathrm{eq}}(N,\sigma)=N,J_{\log}(\sigma/N)=N(\cosh(\sigma/N)-1)$.
$J_{\log}$ is the additive form of the Recognition cost $J(x)=\cosh(\log x)-1$. Upstream J_log_nonneg states $J_{\log}(t)\ge 0$ for all real $t$, with equality only at $t=0$. Recognition equilibrium (Cosmology) identifies the zero-cost ground state with consensus; nonnegativity of $S_{\mathrm{eq}}$ is the scalar shadow of that fact on the conserved-energy slice.
proof idea
Term-mode proof. Unfold equilibrium_entropy to $N\cdot J_{\log}(\sigma/N)$. Apply mul_nonneg: the first factor is nonnegative by positivity on $N:\mathbb{N}$; the second is J_log_nonneg (σ/N) from DiscretenessForcing. No further case splits.
why it matters
Closes the elementary positivity half of the F-011 entropy package: $S_{\mathrm{eq}}\ge 0$ with the companion zero-iff statement on the next line. In the RS forcing chain this is the thermodynamic reading of T5 J-uniqueness (cost vanishes only at unity). It underwrites temperature as a Lagrange multiplier for the observer's coarse-grained heat bath and keeps free-energy comparisons well-signed. No downstream dependents are recorded yet; siblings equilibrium_entropy_zero_iff and rs_entropy_nonneg form the local cluster.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.