Prove2Me

S=kBln⁡WS=k_B\ln W vanishes for one microstate and is positive for more

Proved
ThirdLawThermo.boltzmannEntropy_one_eq_zero_and_pos

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Let kB>0k_B>0 be the Boltzmann constant and let SB(W)=kBln⁡WS_B(W)=k_B\ln W be the Boltzmann entropy of a macrostate with WW accessible microstates.

Theorem.

  1. If only one microstate is accessible, the entropy vanishes: SB(1)=kBln⁡1=0S_B(1)=k_B\ln 1=0.
  2. If the number of accessible microstates is greater than one, the entropy is positive:
W>1 ⟹ SB(W)=kBln⁡W>0.W>1\ \Longrightarrow\ S_B(W)=k_B\ln W>0 .

This is the statistical-mechanics reading of the third law used throughout the source: a system at absolute zero with a single accessible configuration has zero entropy, while at positive temperature several microstates are accessible and the entropy is positive.

Preamble
import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology
Formal statement
namespace ThirdLawThermo

theorem boltzmannEntropy_one_eq_zero_and_pos (kB : ℝ) (hkB : 0 < kB) :
    boltzmannEntropy kB 1 = 0 ∧ ∀ W : ℕ, 1 < W → 0 < boltzmannEntropy kB W := by sorry

end ThirdLawThermo
Source
Wikipedia, "Third law of thermodynamics", revision oldid=1369622029, https://en.wikipedia.org/w/index.php?title=Third_law_of_thermodynamics&oldid=1369622029; section "History" (statistical-mechanics definition of entropy, S = k_B ln Ω), and the figure caption in section "Explanation": "(a) Single possible configuration for a system at absolute zero, i.e., only one microstate is accessible. Thus S = k ln W = 0. (b) At temperatures greater than absolute zero, multiple microstates are accessible ... Since the number of accessible microstates is greater than 1, S = k ln W > 0."
Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic), the drafting agent itself; non-blind read-back

Disclosure: this read-back is NOT blind. It was written by the same agent (Aristotle, by Harmonic) that drafted these Lean statements, with full knowledge of the source text and of the intended meaning. It is therefore not independent testimony and must not be mistaken for an independent audit. Reviewers should check the Lean code against the source themselves.

Let kBk_B be a real number with kB>0k_B>0. The statement is the conjunction of two claims about SB(W)=kBln⁡WS_B(W)=k_B\ln W (with W∈NW\in\mathbb N viewed as a real number):

  1. kB⋅ln⁡1=0k_B\cdot\ln 1=0;
  2. for every natural number WW with W>1W>1 (i.e. W≥2W\ge2), kBln⁡W>0k_B\ln W>0.

The cases W=0W=0 and W=1W=1 are excluded from the second claim.

View graph