specific_heat_at_zero

Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and a finite-resolution observer. Entropy is total defect $S(c)=\sum_i J(x_i)$ (zero only at the all-ones configuration). Energy is the conserved log-charge $E(c)=\sum_i\log(x_i)$. Temperature is not a ledger primitive: it is the Lagrange multiplier for the unseen $N-K$ entries when an observer resolves only $K$ of them.

Specific heat is the response $C=\partial E/\partial T$ (equivalently $T,\partial S/\partial T$) of that coarse-grained description. The underlying cost is the unique J from the forcing chain, $J(x)=\cosh(\log x)-1$, so equilibrium free-energy formulae inherit hyperbolic functions of the energy coordinate. The zero-energy slice is the pure unity configuration, where every entry equals 1 and both entropy and temperature vanish (the third-law regime treated immediately below this lemma).

Term-mode proof: unfold the definition of specific heat, then simp with the single fact Real.cosh_zero (i.e. $\cosh 0=1$). All remaining algebraic factors collapse to the constant $1/N$. No external lemmas beyond that identity are required.

Supplies the exact zero-energy value of heat capacity inside the RS thermodynamic dictionary. It anchors the third-law block that follows: as energy tends to 0, temperature and entropy both tend to 0, and the residual specific heat is the finite positive constant $1/N$ rather than an indeterminate form. That constant is extensive in the reciprocal system size, matching the interpretation of the unseen bath as $N$ ledger entries. No downstream theorems yet depend on it (used_by is empty), but it is the natural base case for any later expansion of $C(E)$ about the unity point and for checking consistency of the canonical ensemble against the variational dynamics. Framework landmarks: J-uniqueness (T5) supplies the cosh that appears in the unfolded definition; the eight-tick / D=3 chain is not used here.