temperature_determines_equilibrium
plain-language theorem explainer
Equal RS temperatures at fixed system size force equal log-charges: if sinh(σ₁/N) = sinh(σ₂/N) for N > 0, then σ₁ = σ₂. Thermodynamic uniqueness arguments cite this to treat temperature as a complete label of the equilibrium macrostate. The proof is a short injectivity argument for sinh followed by clearing the positive denominator N.
Claim. For every natural number $N > 0$ and real log-charges $\sigma_1, \sigma_2$, if the RS temperatures agree, $\sinh(\sigma_1/N) = \sinh(\sigma_2/N)$, then $\sigma_1 = \sigma_2$. Equivalently, temperature uniquely determines the equilibrium energy parameter at fixed size.
background
Module F-011 builds temperature from the ledger J-cost and a finite-resolution observer. Entropy is total defect $S(c) = \sum_i J(x_i)$ (from InitialCondition), zero only at unity. Energy is the conserved log-charge $E(c) = \sum_i \log(x_i)$ from variational dynamics. Temperature is not a ledger primitive; it is the Lagrange multiplier for the observer's coarse-grained heat bath.
At equilibrium each entry is $\exp(\sigma/N)$, and equilibrium entropy is $S_{\mathrm{eq}}(\sigma) = N(\cosh(\sigma/N)-1)$. The RS temperature is defined as the derivative $T(\sigma,N) = dS_{\mathrm{eq}}/d\sigma = \sinh(\sigma/N)$, the direct analogue of $T = \partial S/\partial E$. Sibling facts record $T=0$ at zero charge (absolute zero) and nonnegativity of equilibrium entropy.
The present statement isolates the uniqueness half of that dictionary: because $\sinh$ is injective on $\mathbb{R}$, the map $\sigma \mapsto T(\sigma,N)$ is one-to-one for each fixed positive $N$.
proof idea
Term-mode proof. Unfold the definition $T = \sinh(\sigma/N)$ in the hypothesis. Cast $N > 0$ to a positive real so division by $N$ is legitimate. Apply Real.sinh_injective to obtain $\sigma_1/N = \sigma_2/N$. Multiply both sides by $N$ via congrArg, then field_simp with the nonzero cast of $N$ to conclude $\sigma_1 = \sigma_2$. No thermodynamic lemmas beyond the definition of RS temperature are required.
why it matters
In the RS thermodynamic package this is the uniqueness clause that lets temperature label equilibrium states: once $N$ is fixed, $T$ determines $\sigma$, hence the full equilibrium configuration $\exp(\sigma/N)$ on each entry. The module doc frames temperature as the missing contact point between ledger defect structure and classical thermo; without injectivity, equal temperatures could hide distinct energies and the canonical ensemble would be ambiguous.
Immediately downstream in the same file, the First Law identity $dS_{\mathrm{eq}} = T, dE$ with $S_{\mathrm{eq}} = N(\cosh(\sigma/N)-1)$ and $dS_{\mathrm{eq}}/d\sigma = \sinh(\sigma/N)$ relies on $\sigma$ being the correct energy coordinate recovered from $T$. No external used_by edges are recorded yet, so the lemma currently anchors the local Part 3–4 development (temperature and First Law) rather than a later forcing-chain step. It does not invoke T5–T8, RCL, or the phi ladder; it is pure real analysis inside the F-011 thermodynamic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.