equilibrium_entry
plain-language theorem explainer
At thermodynamic equilibrium with N ledger entries and conserved log-charge σ, every entry equals exp(σ/N). Thermodynamic constructions in the RS foundation cite this as the uniform configuration realizing fixed energy. It is a one-line definition: the exponential of mean energy per site.
Claim. For $N \in \mathbb{N}$ and conserved energy $\sigma \in \mathbb{R}$, the equilibrium ledger entry is $e^{\sigma/N}$.
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)$ (zero only at unity); energy is the conserved log-charge $E(c)=\sum_i \log(x_i)$ from variational dynamics.
Equilibrium under fixed total energy $\sigma$ is the uniform configuration: every entry carries the same share $\sigma/N$ of log-charge. Exponentiating that share recovers the entry value itself. Temperature later appears as the Lagrange multiplier for the unseen bath when an observer resolves only $K<N$ entries.
proof idea
Pure definition: Real.exp (σ / N). No lemmas or tactics; the body is the closed-form uniform entry under additive conservation of log-charge.
why it matters
Supplies the uniform equilibrium configuration used by equilibrium_entry_pos (strict positivity of the entry) and, through that, the equilibrium entropy $S_{\mathrm{eq}}(\sigma)=N,J(e^{\sigma/N})=N(\cosh(\sigma/N)-1)$. That formula is the bridge from ledger defect to thermodynamic $S(E)$, enabling temperature as $\partial E/\partial S$ in the coarse-grained observer picture. It sits downstream of energy-as-log-charge and upstream of the full canonical-ensemble story in F-011.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.