equilibrium_entry_pos
plain-language theorem explainer
Every equilibrium ledger entry exp(σ/N) is strictly positive for any natural N and real conserved energy σ. Thermodynamic constructions that take logs, form J-costs, or build the canonical ensemble cite this positivity. The proof is a one-line appeal to positivity of the real exponential.
Claim. For every $N \in \mathbb{N}$ and every $\sigma \in \mathbb{R}$, the equilibrium entry $e^{\sigma/N}$ satisfies $e^{\sigma/N} > 0$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and finite observer resolution. Entropy is total defect $S(c)=\sum_i J(x_i)$; energy is the conserved log-charge $E(c)=\sum_i \log(x_i)$, written $\sigma$ when fixed.
At equilibrium the configuration is uniform: each of the $N$ entries equals $\exp(\sigma/N)$. That value is the definition of the equilibrium entry. Downstream equilibrium entropy is $S_{\mathrm{eq}}(\sigma)=N,J(\exp(\sigma/N))=N(\cosh(\sigma/N)-1)$, which needs the argument of $J$ to lie in $\mathbb{R}_{>0}$.
$J$ is the unique cost from the forcing chain (T5): $J(x)=(x+x^{-1})/2-1$. Positivity of each entry is the elementary gate before those identities apply.
proof idea
Term-mode one-liner. Unfold the equilibrium entry to $\mathrm{Real.exp}(\sigma/N)$ and apply Real.exp_pos, which states $\exp(t)>0$ for every real $t$. No case split on $N$ or $\sigma$ is required.
why it matters
Closes the positivity obligation for the equilibrium sector of F-011. Sibling results (equilibrium entropy, its nonnegativity, and the zero-iff-unity characterization) all evaluate $J$ at the equilibrium entry; without $x>0$ those statements are ill-typed in the RS cost calculus.
In the broader framework this sits under the variational dynamics that conserve $\sigma$ and under the entropy-as-defect reading from InitialCondition. It is the elementary analytic fact that lets the canonical ensemble (observer resolution $K<N$, unseen entries as heat bath) stay inside the domain where T5 J-uniqueness and the Recognition Composition Law apply. No downstream theorems currently list it as a direct edge, but the sibling equilibrium entropy block is the intended consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.