Foundation Thermodynamics Equilibrium Entropy Nonneg

The nonnegative entropy theorem

In classical thermodynamics, entropy measures the number of microscopic arrangements a system can have while looking the same from the outside. That number is never negative, because a system cannot have fewer than zero ways to be arranged. The Recognition Science framework builds a discrete model of physical states and asks whether this basic property survives translation into its own terms.

The framework's answer is the theorem equilibrium_entropy_nonneg, which states that for any system size N and any value of the conserved charge σ, the equilibrium entropy is greater than or equal to zero. The proof is short and direct. The framework defines equilibrium entropy as N times a cost function J applied to the ratio σ/N, where J(x) = (x + 1/x)/2 − 1. Since J is always nonnegative for positive x, and N is positive, the product is nonnegative. The machine-checked library of formal theorems records this argument in full.

The theorem is one of several structural results in the framework's thermodynamics module. Its companion results show that entropy is zero exactly when the system sits in its ground state with σ = 0, and that temperature, defined as the derivative of entropy with respect to energy, is also zero at that point. Together these establish that the framework's equilibrium thermodynamics has a sensible absolute zero: no disorder, no temperature, no entropy.

In Recognition Science, the declaration does not claim that entropy always increases. The framework's only directional theorem about the total defect, which it identifies with entropy, proves the opposite sign: the defect is non-increasing along variational trajectories. The framework's own documentation flags this as an open problem, noting that a second-law statement would require an observer-side rescue that is not yet proved.

What the theorem does give is a consistency check. Any framework that hopes to describe thermodynamics must reproduce the fact that equilibrium entropy is nonnegative. This result confirms that the framework's cost-based definition behaves correctly at equilibrium, and it clears the way for the more ambitious claims about temperature and the canonical ensemble that the module goes on to make.

/-- The equilibrium entropy as a function of the conserved energy σ.
    S_eq(σ) = N · J(exp(σ/N)) = N · (cosh(σ/N) - 1). -/
noncomputable def equilibrium_entropy (N : ℕ) (σ : ℝ) : ℝ :=
  N * J_log (σ / N)

/-- Equilibrium entropy is non-negative. -/
theorem equilibrium_entropy_nonneg (N : ℕ) (σ : ℝ) :
    0 ≤ equilibrium_entropy N σ := by
  unfold equilibrium_entropy
  apply mul_nonneg
  · positivity
  · exact J_log_nonneg (σ / N)

/-- Total defect is non-increasing for the full ledger. -/
theorem full_defect_monotone {N : ℕ}
    (traj : Trajectory N)
    (h : IsVariationalTrajectory traj) :
    ∀ t, total_defect (traj (t + 1)) ≤ total_defect (traj t) :=
  trajectory_defect_monotone traj h

What this page does not claim

This theorem does not prove a second law of thermodynamics. This theorem does not claim that entropy is nonnegative for non-equilibrium configurations. This theorem does not establish the physical existence of the framework's equilibrium states.

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: