specific_heat
plain-language theorem explainer
Defines the RS specific heat at fixed charge as C_N(σ) = cosh(σ/N)/N. It is the second σ-derivative of equilibrium entropy and the σ-derivative of temperature. Thermodynamic stability proofs and the F-011 certificate cite it. The body is a direct closed-form assignment from differentiating sinh(σ/N).
Claim. For system size $N\in\mathbb{N}$ and charge parameter $\sigma\in\mathbb{R}$, the specific heat is $C_N(\sigma)=\cosh(\sigma/N)/N$. Equivalently $C=dS_{\mathrm{eq}}/dT=d^2 S_{\mathrm{eq}}/d\sigma^2$ at constant charge.
background
Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and finite observer resolution. Entropy is total defect $S(c)=\sum_i J(x_i)$; energy is log-charge $E(c)=\sum_i\log(x_i)$. Temperature is not a ledger property: an observer with resolution $K<N$ treats the unseen entries as a heat bath, and the Lagrange multiplier of that coarse-graining is $T$.
Equilibrium entropy as a function of total charge $\sigma$ takes the form involving $\sinh(\sigma/N)$. Differentiating once in $\sigma$ recovers temperature; differentiating again yields specific heat. The closed form $C_N(\sigma)=\cosh(\sigma/N)/N$ is the elementary consequence of $d(\sinh u)/du=\cosh u$ with $u=\sigma/N$.
Sibling definitions supply $S$, $E$, equilibrium entropy, and $T_N(\sigma)$. Positivity of $\cosh$ then gives thermodynamic stability for every $N>0$.
proof idea
Definitional, not a proof. The body sets specific_heat N σ equal to Real.cosh (σ / N) / N, matching the formal derivative of equilibrium entropy (or of temperature) under the equilibrium ansatz. Downstream lemmas unfold this definition and apply Real.cosh_pos, Real.cosh_zero, and the chain rule for deriv (fun x => Real.sinh (x / N)).
why it matters
Fills the heat-capacity slot in the F-011 thermodynamic dictionary so RS can state stability and response functions in standard language. Parents: specific_heat_positive (C>0 for N>0), specific_heat_is_second_deriv (C = dT/dσ = d²S_eq/dσ²), specific_heat_at_zero (C(0)=1/N), and the aggregate thermodynamics_certificate. Thermal-equilibrium comparison lemmas sit nearby in the same module.
In the broader chain this is bookkeeping after entropy-as-defect and energy-as-log-charge: once T exists from coarse-graining, C is forced by calculus. It does not invoke T5–T8 directly, but it is the response function that makes the ledger thermodynamics contact ordinary statistical mechanics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.