temperature_positive
plain-language theorem explainer
For positive system size N and positive conserved log-charge σ, the RS temperature sinh(σ/N) is strictly positive. Anyone matching ledger energy above the ground state to a thermodynamic T > 0 cites this. The argument unfolds the definition and applies the standard positivity criterion for sinh on a positive quotient.
Claim. For every natural number $N > 0$ and every real energy parameter $\sigma > 0$, the Recognition Science temperature $T(N,\sigma) := \sinh(\sigma/N)$ satisfies $0 < T(N,\sigma)$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and an observer's finite resolution. Entropy is the 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)$, written $\sigma$ in the equilibrium slice; it is extensive and fixed by the variational dynamics.
Temperature is not a property of the full ledger state. It is the Lagrange multiplier in the observer's coarse-grained description of the unseen entries (the heat bath). The RS temperature is defined by differentiating equilibrium entropy in the charge: $T(N,\sigma) = dS_{\mathrm{eq}}/d\sigma = \sinh(\sigma/N)$. The sibling zero-temperature statement records that $\sigma = 0$ forces $T = 0$.
The present claim is the positive-energy half of that dictionary: energy above the ground state yields strictly positive temperature.
proof idea
Term-mode proof. Unfold the definition $T(N,\sigma) = \sinh(\sigma/N)$. Promote the hypothesis $0 < N$ to a real inequality via Nat.cast_pos. The quotient $\sigma/N$ is then positive by div_pos. Conclude with the Mathlib equivalence Real.sinh_pos_iff, which states that $\sinh x > 0$ if and only if $x > 0$.
why it matters
Without a positive-temperature theorem the ledger cannot contact classical thermodynamics ($T = \partial E/\partial S$ and the canonical ensemble). This result closes that half of F-011 for $\sigma > 0$, pairing with the zero-temperature and negative-temperature siblings in the same module.
It sits on the entropy-as-defect and energy-as-log-charge infrastructure from InitialCondition and VariationalDynamics, and on the observer/heat-bath reading from MeasurementMechanism. No downstream theorems currently depend on it, so it is a leaf that future equilibrium and ensemble statements can cite directly.
Framework-wise it is pure thermodynamics of the J-cost ledger; it does not invoke the forcing chain T5–T8, the RCL, or the mass ladder, but it supplies the missing thermodynamic coordinate those structures need once dynamics and measurement are in place.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.