The stretch rescales the canonical commutator: $[\sqrt\lambda X,\sqrt\lambda P] = i\lambda\hbar$

Proved

HighEntropyLimit.stretched_commutator

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

mathematical-physicsquantum-mechanics

Let $\mathcal A$ be a $\mathbb C$ -algebra and $X,P\in\mathcal A$ with $[X,P] = XP - PX = i\hbar$ . For $\lambda>1$ ,

[\sqrt\lambda X, \sqrt\lambda P] = \lambda[X,P] = i\lambda\hbar.

So the stretched position and momentum obey canonical commutation relations with $\hbar$ replaced by $\lambda\hbar$ .

Preamble

import Mathlib

Formal statement

namespace HighEntropyLimit
theorem stretched_commutator {A : Type*} [Ring A] [Algebra ℂ A] (X P : A) (hbar lam : ℝ)
    (hlam : 1 < lam) (hccr : X * P - P * X = (Complex.I * hbar) • (1 : A)) :
    ((Real.sqrt lam : ℂ) • X) * ((Real.sqrt lam : ℂ) • P) -
        ((Real.sqrt lam : ℂ) • P) * ((Real.sqrt lam : ℂ) • X) =
      (Complex.I * (lam * hbar : ℝ)) • (1 : A) := 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. 10, Eqs. (35)-(38)

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

The stretch rescales the canonical commutator: [λX,λP]=iλℏ[\sqrt\lambda X,\sqrt\lambda P] = i\lambda\hbar[λ​X,λ​P]=iλℏ

The stretch rescales the canonical commutator: $[\sqrt\lambda X,\sqrt\lambda P] = i\lambda\hbar$