rs_temperature
plain-language theorem explainer
RS temperature is defined as T(N,σ)=sinh(σ/N), the derivative of equilibrium entropy with respect to conserved log-charge. Thermodynamic arguments in the ledger framework cite it as the RS analogue of ∂S/∂E. The body is a one-line definition via Real.sinh of the per-entry energy.
Claim. For system size $N\in\mathbb{N}$ and conserved log-charge $\sigma\in\mathbb{R}$, the Recognition Science temperature is $T(N,\sigma)=\sinh(\sigma/N)$. Equivalently, if equilibrium entropy is $S_{\mathrm{eq}}(\sigma)=N(\cosh(\sigma/N)-1)$, then $T=\partial S_{\mathrm{eq}}/\partial\sigma$.
background
Module F-011 builds thermodynamics from the ledger J-cost and finite observer resolution. Entropy of a configuration is total defect $\sum_i J(x_i)$ (from InitialCondition), zero only at unity. Energy is the conserved log-charge $\sigma=\sum_i\log(x_i)$ from variational dynamics: extensive, conserved, and the Lagrange multiplier that fixes equilibrium.
Temperature is not a ledger primitive. It arises when an observer with resolution $K<N$ treats the unseen entries as a heat bath; the associated multiplier is $T$. Equilibrium entropy takes the closed form $S_{\mathrm{eq}}(\sigma)=N(\cosh(\sigma/N)-1)$, which is $N$ times the J-cost of the equal-share entry $e^{\sigma/N}$ (since $J(e^u)=\cosh u-1$).
Differentiating that formula yields $\partial S_{\mathrm{eq}}/\partial\sigma=\sinh(\sigma/N)$. The definition packages that derivative as the RS temperature, matching the classical identification $T=\partial S/\partial E$ with $E$ identified with $\sigma$.
proof idea
Pure definition: the body is Real.sinh (σ / N). No tactics or lemmas. Downstream theorems (first law, sign properties) unfold this abbreviation and apply standard calculus identities for sinh and cosh.
why it matters
This is the missing thermodynamic coordinate that lets RS contact classical thermo. It feeds the first law (deriv equilibrium_entropy = rs_temperature), thermal equilibrium (equal temperatures iff equal $\sigma/N$), uniqueness of equilibrium from $T$ (sinh injective), sign theorems (positive/negative $T$ with $\sigma$), oddness in $\sigma$, and specific heat as $dT/d\sigma=\cosh(\sigma/N)/N$.
In the module narrative, absolute zero is the zero-defect (unity) state: $T(N,0)=0$, the third-law endpoint. Negative temperature is population inversion (more entries below unity than above). Together with J-uniqueness (T5) and the defect=entropy link, temperature closes the gap from ledger cost structure to the canonical ensemble without extra postulates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.