Prove2Me

Eqs. (11)–(12): C=C0TαC=C_0T^\alpha is compatible with the third law iff α>0\alpha>0

Proved
ThirdLawThermo.powerLaw_heatCapacity_entropy_bounded_iff

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

mathematical-physicsstatistical-mechanicsthermodynamicsthird-law

Suppose that at low temperature the heat capacity of a sample follows a power law C(T)=C0TαC(T)=C_0T^{\alpha} with C0>0C_0>0 and α∈R\alpha\in\mathbb R, and fix a temperature T>0T>0. The entropy difference between temperatures T0∈(0,T)T_0\in(0,T) and TT is

S(T)−S(T0)=∫T0TC(T′)T′ dT′=∫T0TC0 T′αT′ dT′.S(T)-S(T_0)=\int_{T_0}^{T}\frac{C(T')}{T'}\,dT'=\int_{T_0}^{T}\frac{C_0\,T'^{\alpha}}{T'}\,dT' .

Theorem. This entropy difference stays bounded above as T0→0T_0\to0 if and only if the exponent is positive:

(∃M ∀T0∈(0,T): ∫T0TC0T′αT′ dT′≤M)  ⟺  α>0.\Big(\exists M\ \forall T_0\in(0,T):\ \int_{T_0}^{T}\frac{C_0T'^{\alpha}}{T'}\,dT'\le M\Big)\iff\alpha>0 .

Since the third law requires the entropy to approach a finite value as T→0T\to0, a power-law heat capacity is compatible with it only for α>0\alpha>0, in which case C(T)→0C(T)\to0 at absolute zero (Eq. (12)).

Formalization Note The power law is assumed to hold exactly on the whole interval (0,T](0,T]; the source's "asymptotically as T→0T\to0" version differs only by an integral over a compact subinterval of (0,∞)(0,\infty), which is finite. T′αT'^{\alpha} is the real power with positive base.

Preamble
import Definitions.Def_ThirdLawThermo_Defs
import Mathlib

open Filter Topology
Formal statement
namespace ThirdLawThermo

theorem powerLaw_heatCapacity_entropy_bounded_iff (C₀ α T : ℝ) (hC₀ : 0 < C₀) (hT : 0 < T) :
    (∃ M : ℝ, ∀ T₀ ∈ Set.Ioo 0 T, ∫ t in T₀..T, C₀ * t ^ α / t ≤ M) ↔ 0 < α := 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", Eq. (11) and Eq. (12) ("Suppose that the heat capacity of a sample in the low temperature region has the form of a power law C(T,X) = C0 T^α asymptotically as T → 0, and we wish to find which values of α are compatible with the third law. ... this integral must be bounded as T0 → 0, which is only possible if α > 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.

For all reals C0C_0, α\alpha, TT with C0>0C_0>0 and T>0T>0 (and α\alpha arbitrary), the statement asserts the equivalence of

  1. there exists a real MM such that for every T0T_0 with 0<T0<T0<T_0<T,
∫T0TC0 tαt dt≤M\int_{T_0}^{T}\frac{C_0\,t^{\alpha}}{t}\,dt\le M

(an ordinary integral over [T0,T][T_0,T] of a continuous function of t>0t>0; tαt^{\alpha} is the real power); 2. α>0\alpha>0.

Only an upper bound is asserted in (1); the integrand is positive, so the integrals are also positive.

View graph