equilibrium_entropy_zero_iff
plain-language theorem explainer
Equilibrium entropy of an N-entry ledger vanishes exactly when the conserved log-charge σ is zero. Anyone identifying the thermodynamic ground state (zero entropy, unity configuration) with vanishing charge cites this characterization. The argument unfolds S_eq = N · J_log(σ/N) and uses the known zero locus of J_log together with N > 0.
Claim. For every positive integer $N$ and every real $\sigma$, the equilibrium entropy $S_{\mathrm{eq}}(N,\sigma) := N \cdot J_{\log}(\sigma/N)$ satisfies $S_{\mathrm{eq}}(N,\sigma) = 0$ if and only if $\sigma = 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 total defect $\sum_i J(x_i)$ (InitialCondition); energy is the conserved log-charge $\sum_i \log x_i$ (VariationalDynamics). Equilibrium entropy is the value of that defect on the equal-share equilibrium entry: with charge $\sigma$ spread over $N$ slots one has $S_{\mathrm{eq}}(N,\sigma) = N \cdot J_{\log}(\sigma/N)$, where $J_{\log}(t) = \cosh t - 1$ is the unique cost forced by the Recognition Composition Law (T5).
Upstream, J_log_eq_zero_iff records that $J_{\log}(t) = 0$ precisely at $t = 0$ (via $\cosh t = 1$), and J_log_zero is the evaluation $J_{\log}(0) = 0$. The present lemma is the corresponding statement for the extensive equilibrium functional.
proof idea
Term-mode proof after unfolding the definition of equilibrium entropy (so the goal is $N \cdot J_{\log}(\sigma/N) = 0 \leftrightarrow \sigma = 0$). Forward direction: cast $N > 0$ to reals, apply mul_eq_zero, discard the $N = 0$ branch by linarith, then feed the remaining factor into J_log_eq_zero_iff and clear the denominator with div_eq_zero_iff (using $N \neq 0$). Reverse direction: substitute $\sigma = 0$, rewrite $0/N = 0$, apply J_log_zero and mul_zero.
why it matters
Closes the zero-locus step for equilibrium thermodynamics inside F-011. Downstream temperature is defined as $T = \partial S_{\mathrm{eq}}/\partial\sigma = \sinh(\sigma/N)$; knowing $S_{\mathrm{eq}} = 0$ only at $\sigma = 0$ pins the unique zero-temperature, zero-entropy state to vanishing charge, matching the unity configuration of the forcing chain. The identity rests on T5 J-uniqueness ($J(x) = \cosh(\log x) - 1$) and on entropy-as-defect from InitialCondition. No parent theorems currently depend on it in the graph, but the sibling temperature block and any canonical-ensemble uniqueness argument need exactly this characterization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.