Foundation Thermodynamics Thermal Eq Iff Equal Ratio

Thermal equilibrium

In classical thermodynamics, two bodies in thermal contact settle into a shared temperature. The Recognition Science framework reaches the same conclusion from a different starting point. It defines a system's energy as the sum of the logarithms of its entries, and its temperature as the derivative of entropy with respect to that energy. The framework's library of machine-checked theorems then proves a compact equivalence: two systems are in thermal equilibrium if and only if their energy per entry is equal.

The statement, named thermal_eq_iff_equal_ratio, is a theorem in the framework's formal library. It says that for two systems with entry counts N₁ and N₂ and total energies σ₁ and σ₂, the condition σ₁/N₁ = σ₂/N₂ holds exactly when their temperatures match. The proof relies on the fact that the framework's temperature function is the hyperbolic sine of the energy per entry, and the sine function is injective on the real line. This makes the equality of temperatures and the equality of ratios logically interchangeable.

The result is a structural consequence of how the framework defines its thermodynamic quantities. It does not claim that this is the only way to define temperature, nor does it assert that the framework's temperature matches the Kelvin scale in any direct numerical sense. The theorem is about the internal consistency of the framework's definitions, not about calibrating them to laboratory measurements.

What the theorem does establish is that the framework's concept of thermal equilibrium is well-formed. It gives a precise, checkable condition for when two systems can be said to share a temperature. This is a necessary step for the framework to make contact with the rest of thermodynamics, and it is a step the framework has taken with a machine-checked proof.

/-- Thermal equilibrium means equal sinh(σ/N), hence equal σ/N. -/
theorem thermal_eq_iff_equal_ratio (N₁ N₂ : ℕ) (hN₁ : 0 < N₁) (hN₂ : 0 < N₂)
    (σ₁ σ₂ : ℝ) :
    InThermalEquilibrium N₁ N₂ σ₁ σ₂ ↔ σ₁ / N₁ = σ₂ / N₂ := by
  unfold InThermalEquilibrium rs_temperature
  constructor
  · intro h
    exact Real.sinh_injective h
  · intro h
    exact congrArg Real.sinh h

/-- **RS Temperature**: The derivative of equilibrium entropy with respect
    to energy (the conserved charge σ).

    T(σ, N) = dS_eq/dσ = sinh(σ/N)

    This is the RS analogue of T = ∂S/∂E in classical thermodynamics.

    Derivation:
      S_eq(σ) = N · (cosh(σ/N) - 1)
      dS_eq/dσ = N · sinh(σ/N) · (1/N) = sinh(σ/N) -/
noncomputable def rs_temperature (N : ℕ) (σ : ℝ) : ℝ :=
  Real.sinh (σ / N)

/-- **RS Energy**: The total log-ratio (conserved charge).
    E(c) = ∑ᵢ log(xᵢ), conserved under dynamics. -/
noncomputable def rs_energy {N : ℕ} (c : Configuration N) : ℝ :=
  log_charge c

What this page does not claim

This theorem does not prove the second law of thermodynamics. This theorem does not claim the framework's temperature is numerically equal to the Kelvin temperature. This theorem does not establish that the framework's definitions correspond to any real physical system.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/Thermodynamics.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: