InThermalEquilibrium
plain-language theorem explainer
Two finite subsystems with entry counts N₁, N₂ and conserved log-charges σ₁, σ₂ are thermally equilibrated precisely when their RS temperatures agree. Temperature is sinh(σ/N), so equality of temperatures is the natural contact condition between coarse-grained observers. Anyone deriving zeroth-law style statements or canonical ensembles from the ledger cites this predicate. The body is a one-line equality of the temperature definition.
Claim. Subsystems with sizes $N_1,N_2\in\mathbb{N}$ and conserved charges $\sigma_1,\sigma_2\in\mathbb{R}$ are in thermal equilibrium when $T(N_1,\sigma_1)=T(N_2,\sigma_2)$, where the RS temperature is $T(N,\sigma)=\sinh(\sigma/N)$.
background
Module F-011 builds temperature and the canonical ensemble from the ledger's J-cost and finite observer resolution. Entropy is total defect $S=\sum_i J(x_i)$ (from InitialCondition); energy is the conserved log-charge $\sigma=\sum_i\log(x_i)$ (from VariationalDynamics). Temperature is not a ledger primitive: it arises when an observer with resolution $K<N$ treats the unseen entries as a heat bath, so the Lagrange multiplier of the constrained defect is $T$.
The RS temperature is defined by $T(N,\sigma)=\sinh(\sigma/N)$, the derivative of equilibrium entropy with respect to charge. At unity ($\sigma=0$) one has $T=0$. The classical contact rule "equal temperatures" is therefore equality of these sinh values for two subsystems.
proof idea
Pure definitional abbreviation: the predicate is the propositional equality rs_temperature N₁ σ₁ = rs_temperature N₂ σ₂. No tactics or lemmas are invoked; unfolding later yields sinh(σ₁/N₁)=sinh(σ₂/N₂).
why it matters
This is the zeroth-law contact condition inside the RS thermodynamic layer. Downstream, thermal_eq_iff_equal_ratio converts equal temperatures into equal per-entry charges $\sigma/N$ (for positive $N$), which is the form needed for heat-flow and ensemble arguments. It closes the gap named in the module doc: entropy, time, and variational dynamics existed, but without a temperature predicate the framework could not state thermal equilibrium or derive $T=\partial S/\partial E$-style relations. It sits under the broader forcing chain only indirectly (J-cost and defect structure from T5 onward), but is the local bridge from ledger cost to classical thermo language.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.