A heat capacity bounded below by a positive constant makes the entropy diverge

Proved

ThirdLawThermo.entropy_integral_tendsto_atTop_of_heatCapacity_ge

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Let $C(T)$ be the heat capacity of a sample, let $T>0$ , and suppose that $C$ is bounded below by a positive constant at low temperature: $C(t)\ge c>0$ for all $t\in(0,T]$ . Assume that $C(t)/t$ is integrable on $[T_0,T]$ for each $T_0\in(0,T)$ , so that the entropy difference

S(T)-S(T_0)=\int_{T_0}^{T}\frac{C(t)}{t}\,dt

is defined.

Theorem. The entropy difference diverges as $T_0\to0$ :

\int_{T_0}^{T}\frac{C(t)}{t}\,dt\longrightarrow+\infty\qquad(T_0\to0^+).

Consequently a heat capacity bounded below by a positive constant near absolute zero violates the third law, with or without a power-law assumption.

Preamble

import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology

Formal statement

namespace ThirdLawThermo

theorem entropy_integral_tendsto_atTop_of_heatCapacity_ge (C : ℝ → ℝ) (c T : ℝ)
    (hc : 0 < c) (hT : 0 < T) (hC : ∀ t ∈ Set.Ioc 0 T, c ≤ C t)
    (hint : ∀ T₀ ∈ Set.Ioo 0 T,
      IntervalIntegrable (fun t => C t / t) MeasureTheory.volume T₀ T) :
    Tendsto (fun T₀ => ∫ t in T₀..T, C t / t) (𝓝[>] 0) atTop := 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 "Consequences", subsection "Specific heat", sentence after Eq. (12): "The same argument shows that it cannot be bounded below by a positive constant, even if we drop the power-law assumption."

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 $C:\mathbb R\to\mathbb R$ be any function and $c,T$ reals with $c>0$ and $T>0$ . Assume

$c\le C(t)$ for every $t$ with $0<t\le T$ ;
for every $T_0$ with $0<T_0<T$ , the function $t\mapsto C(t)/t$ is Lebesgue integrable on the interval between $T_0$ and $T$ .

Then

\int_{T_0}^{T}\frac{C(t)}{t}\,dt\to+\infty\quad\text{as }T_0\to0\text{ with }T_0>0,

i.e. for every $B$ there is $\delta>0$ with the integral exceeding $B$ whenever $0<T_0<\delta$ . No continuity of $C$ and no values of $C$ outside $(0,T]$ are assumed.

View graph