A pure stretch increases Gibbs entropy by $\log\lambda$

Proved

HighEntropyLimit.pure_stretch_entropy_increase

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

mathematical-physicsquantum-mechanics

Let $\lambda>1$ and let $\rho$ be a probability density on phase space $\mathbb R^2$ with finite entropy: $\rho\ge0$ , $\int\rho = 1$ , and $\rho$ , $\rho\log\rho$ integrable. Let $T\rho(z) = \lambda^{-1}\rho(z/\sqrt\lambda)$ be its image under the pure stretching map $T(x,p) = (\sqrt\lambda x, \sqrt\lambda p)$ . Then

S(T\rho) = S(\rho) + \log\lambda, \qquad S(\rho) = -\int\rho\log\rho\,dx\,dp.

Formalization Note The integrability of $\rho\log\rho$ (finite entropy) is implicit in the paper.

Preamble

import Mathlib
import Definitions.Def_HighEntropyLimit_phase_space_stretch
open MeasureTheory

Formal statement

namespace HighEntropyLimit
theorem pure_stretch_entropy_increase (lam : ℝ) (hlam : 1 < lam) (ρ : ℝ × ℝ → ℝ)
    (hρ_nonneg : ∀ z, 0 ≤ ρ z) (hρ_int : Integrable ρ) (hρ_norm : ∫ z, ρ z = 1)
    (hρ_ent : Integrable (fun z => ρ z * Real.log (ρ z))) :
    gibbsEntropy (pureStretch lam ρ) = gibbsEntropy ρ + Real.log lam := by sorry
end HighEntropyLimit

Source

Carcassi, Landini, Aidala, Classical mechanics as the high-entropy limit of quantum mechanics, arXiv:2411.00972v3 (1 Feb 2026), https://arxiv.org/abs/2411.00972, p. 7, Eq. (15) (requirement S(R(ρ)) = S(ρ) + log λ) for the pure stretching map of Eq. (16)

Human review

Endorsed by Shuze Chen · Oct 13, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 13, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

A pure stretch increases Gibbs entropy by log⁡λ\log\lambdalogλ

A pure stretch increases Gibbs entropy by $\log\lambda$