Crystal absorbing a photon: $\Delta S = k_B\ln N$

Proved

ThirdLawThermo.photon_absorption_entropy_change

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Consider a crystal lattice of $N$ identical atoms at $T=0$ which absorbs a single photon. Before absorption only one microstate is accessible; after absorption exactly one atom is excited and any of the $N$ atoms may be the excited one, so $N$ microstates are accessible. With the Boltzmann entropy $S_B(W)=k_B\ln W$ :

Theorem. The entropy change caused by the absorption is

\Delta S=S_B(N)-S_B(1)=k_B\ln N .

This is the worked example of the source showing that the entropy of a crystal at absolute zero rises from $0$ when energy is absorbed.

Formalization Note The identity is stated for every natural number $N$ and every real $k_B$ ; for $N=0$ both sides are $0$ by the convention $\ln 0=0$ .

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem photon_absorption_entropy_change (kB : ℝ) (N : ℕ) :
    boltzmannEntropy kB N - boltzmannEntropy kB 1 = kB * Real.log N := 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 "Example: Entropy change of a crystal lattice heated by an incoming photon" ("Initially, there is only one accessible microstate"; "after absorption, there are N possible microstates accessible by the system"; "The entropy change is [formula]"; the displayed formulas appear as images in the supplied PDF and are transcribed as ΔS = k_B ln N − k_B ln 1 from the surrounding text).

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.

For every real number $k_B$ (no sign condition) and every natural number $N$ (including $N=0$ ), the statement asserts

k_B\ln N-k_B\ln 1=k_B\ln N,

where $N$ is viewed as a real number and $\ln 0=0$ . No physical hypotheses appear; the photon, the lattice and the temperature are not represented.

View graph

Crystal absorbing a photon: ΔS=kBln⁡N\Delta S = k_B\ln NΔS=kB​lnN

Crystal absorbing a photon: $\Delta S = k_B\ln N$