first_law
plain-language theorem explainer
At equilibrium, the derivative of RS entropy with respect to the energy parameter equals the RS temperature. Thermodynamic and black-hole workers cite this as the ledger form of the first law. The proof is a one-line pointwise specialization of a prior functional derivative identity.
Claim. For every positive integer $N$ and every real parameter $\sigma$, the ordinary derivative of equilibrium entropy satisfies $\frac{d}{d\sigma}\,S_{\mathrm{eq}}(N)(\sigma)=T_{\mathrm{RS}}(N,\sigma)$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger J-cost and an observer's finite resolution. Entropy of a configuration is its total defect $\sum_i J(x_i)$ (zero only at unity); energy is the conserved log-charge $\sum_i \log x_i$. Temperature is not a property of the full ledger: when an observer resolves only $K<N$ entries, the unseen remainder acts as a heat bath, and the Lagrange multiplier of that coarse-grained description is temperature.
Equilibrium entropy $S_{\mathrm{eq}}(N)$ is the entropy of the equilibrium configuration parameterized by a real energy-like coordinate $\sigma$. RS temperature $T_{\mathrm{RS}}(N,\sigma)$ is the corresponding thermodynamic conjugate. Upstream, defect is identified with the J-cost, and configuration entropy is total defect (InitialCondition).
proof idea
One-line wrapper. Invoke the already-proved functional identity first_law_derivative N hN, which asserts equality of the two functions of $\sigma$. Apply congrFun to evaluate both sides at the given real $\sigma$, yielding the pointwise first-law equality.
why it matters
Closes the classical first-law contact inside F-011: once entropy and temperature exist as ledger quantities, $dS_{\mathrm{eq}}/d\sigma=T$ is the RS statement of the first law. Downstream it is consumed by Quantum.BekensteinHawking.first_law, whose doc-comment targets the black-hole identity $dM=T,dS$ (currently a trivial stub awaiting the geometric identification of mass and horizon entropy). In the broader chain this is the thermodynamic reading of defect and log-charge after T5 J-uniqueness and the variational dynamics, not a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.