temperature_zero_at_unity
plain-language theorem explainer
When the conserved log-charge energy vanishes, RS temperature is identically zero: absolute zero at the unity (zero-defect) state. Cited by the third-law statement and the F-011 thermodynamics certificate. Proof is a one-line unfold of the sinh definition plus the classical identity sinh(0)=0.
Claim. For every positive integer $N$, the RS temperature at vanishing energy satisfies $T(N,0)=0$, where $T(N,\sigma)=\sinh(\sigma/N)$ is the derivative of equilibrium entropy with respect to the conserved log-charge $\sigma$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger's J-cost and the observer's finite resolution. Entropy is total defect, $S(c)=\sum_i J(x_i)$, already zero only at unity. Energy is the conserved log-charge $E(c)=\sum_i\log(x_i)$ from the variational dynamics; it is extensive and labels equilibrium.
Temperature is not a property of the ledger state itself. It is the Lagrange multiplier in the observer's coarse-grained description of unseen entries (the heat bath). The RS formula is $T(N,\sigma)=\sinh(\sigma/N)$, the derivative of equilibrium entropy in the charge $\sigma$. At the zero-defect initial state one has $\sigma=0$, so the ground-state temperature is the value of that formula at the origin.
proof idea
Term proof. Unfold the definition $T(N,\sigma)=\sinh(\sigma/N)$, set $\sigma=0$, and simplify by the standard identity $\sinh(0)=0$. No intermediate lemmas are required beyond that classical fact.
why it matters
Supplies the absolute-zero half of the third law in this module: as energy goes to zero, temperature and entropy both hit zero at the unique minimum-entropy configuration (all entries equal to 1). Downstream, third_law quotes it directly as the first conjunct, and the F-011 thermodynamics certificate lists "temperature is zero at ground state" as clause (1) of the certified dictionary between RS concepts and standard $S$, $E$, $T$.
Together with entropy-vanishing at unity, this closes the ground-state corner of the thermodynamic contact that F-011 was written to provide. It does not yet encode unattainability in finite time; that is stated narratively in the third-law doc-comment via the variational dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.