feat(PhyslibAlpha): QuantumThermodynamics — thermal state, Landauer bound, area API-map

PhyslibAlpha.lean

@@ -29,6 +29,8 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere
 public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell
 public import PhyslibAlpha.QuantumMechanics.QuantumHarmonicOscillator
 public import PhyslibAlpha.QuantumMechanics.StinespringDilation
+public import PhyslibAlpha.QuantumThermodynamics.Landauer
+public import PhyslibAlpha.QuantumThermodynamics.ThermalState
 public import PhyslibAlpha.Mathematics.PartialDerivativeTest
 public import PhyslibAlpha.ClassicalMechanics.CoupledSpringPotential
 public import PhyslibAlpha.Particles.BeyondTheStandardModel.TwoHDM.ChargeBalance

PhyslibAlpha/QuantumThermodynamics/API-map.yaml

@@ -0,0 +1,135 @@
+version: v0.1
+
+Title: Quantum thermodynamics
+
+Overview: |
+    The quantum-thermodynamics API begins with the finite-dimensional thermal
+    (Gibbs) state of a Hamiltonian, `MState.thermalBetaReal H β = exp(-βH) / Z(β)`,
+    and its physical-temperature form `MState.thermal H T`. The thermal state is
+    proved to have trace one and a positive-definite, full-rank density matrix.
+    Its logarithm gives a general Gibbs relative-entropy balance relating energy,
+    von Neumann entropy, and quantum relative entropy.
+
+    A `QuantumThermodynamics.LandauerProcess` starts a system and thermal reservoir
+    in a product state and evolves them by a joint unitary. The API defines the final
+    marginals, entropy changes, heat, and reservoir relative entropy, then proves the
+    exact Landauer identity and the Landauer bound. The open requirements identify
+    the shared infrastructure for the entropy-production and quantum-resource-theory
+    campaigns: total correlation, thermal operations, thermo-majorization, and
+    nonequilibrium quantum free energy.
+
+ParentAPIs:
+  - Mixed quantum states (QuantumInfo/States/Mixed/MState)
+  - Quantum entropy and relative entropy (QuantumInfo/Entropy)
+  - Temperature (Physlib/Thermodynamics/Temperature)
+  - Canonical ensemble (Physlib/StatisticalMechanics/CanonicalEnsemble)
+
+References:
+  - Reeb and Wolf, An improved Landauer principle with finite-size corrections.
+  - Esposito, Lindenberg, and Van den Broeck, New Journal of Physics 12, 013013 (2010).
+  - Horodecki and Oppenheim, Nature Communications 4, 2059 (2013).
+  - Brandão, Horodecki, Ng, Oppenheim, and Wehner, PNAS 112, 3275 (2015).
+
+Requirements:
+
+  - description: >
+      The API defines the finite-dimensional quantum partition function at a real
+      inverse temperature and proves that it is strictly positive.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
+      (HermitianMat.partitionFunctionBetaReal, HermitianMat.partitionFunctionBetaReal_pos)
+
+  - description: >
+      The API constructs the thermal state both from a real inverse temperature and
+      from Physlib's physical `Temperature` type.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
+      (MState.thermalBetaReal, MState.thermal)
+
+  - description: >
+      The thermal-state API proves trace-one normalization, full rank, and positive
+      definiteness of the density matrix.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
+      (MState.thermalBetaReal_trace, MState.thermalBetaReal_nonSingular,
+      MState.thermalBetaReal_posDef)
+
+  - description: >
+      The real-inverse-temperature and physical-temperature parametrizations are
+      connected by an explicit bridge lemma.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
+      (MState.thermal_eq_thermalBetaReal)
+
+  - description: >
+      The API proves the general Gibbs relative-entropy balance for both the real
+      inverse-temperature and physical-temperature parametrizations.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
+      (MState.gibbsRelativeEntropyBalanceBetaReal,
+      MState.gibbsRelativeEntropyBalance)
+
+  - description: >
+      A minimal finite-dimensional Landauer process is defined by an initial system
+      state, reservoir Hamiltonian and temperature, and joint unitary evolution.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/Landauer.lean
+      (QuantumThermodynamics.LandauerProcess)
+
+  - description: >
+      The Landauer-process API defines its initial and final joint states, final
+      marginals, entropy changes, reservoir heat, and reservoir relative entropy.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/Landauer.lean
+      (LandauerProcess.initialReservoir, LandauerProcess.initialJoint,
+      LandauerProcess.finalJoint, LandauerProcess.finalSystem,
+      LandauerProcess.finalReservoir, LandauerProcess.systemEntropyDecrease,
+      LandauerProcess.reservoirEntropyIncrease, LandauerProcess.reservoirHeat,
+      LandauerProcess.reservoirRelativeEntropy)
+
+  - description: >
+      The API proves that the reservoir entropy increase equals the system entropy
+      decrease plus the final system-reservoir mutual information.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/Landauer.lean
+      (LandauerProcess.entropyBalance)
+
+  - description: >
+      The API proves the exact Landauer identity and derives the Landauer bound from
+      nonnegativity of mutual information and quantum relative entropy.
+    done: true
+    location: >
+      PhyslibAlpha/QuantumThermodynamics/Landauer.lean
+      (LandauerProcess.landauerIdentity, LandauerProcess.landauerBound)
+
+  - description: >
+      The API shall define an n-ary total-correlation functional and prove its
+      nonnegativity, supporting multi-reservoir entropy-production identities.
+    done: false
+    location: N/A
+
+  - description: >
+      The API shall define thermal operations and Gibbs-preserving quantum channels,
+      including their preservation laws for thermal states.
+    done: false
+    location: N/A
+
+  - description: >
+      The API shall define the thermo-majorization order on energy-incoherent states
+      and connect it to conversion by thermal operations.
+    done: false
+    location: N/A
+
+  - description: >
+      The API shall define nonequilibrium quantum free energy for mixed states and
+      relate it to quantum relative entropy from the thermal state.
+    done: false
+    location: N/A

PhyslibAlpha/QuantumThermodynamics/Landauer.lean

@@ -0,0 +1,155 @@
+/-
+Copyright (c) 2026 Huanhai Zhou. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Huanhai Zhou
+-/
+module
+
+public import PhyslibAlpha.QuantumThermodynamics.ThermalState
+
+/-!
+# Landauer processes
+
+This file models a finite-dimensional Landauer process. A system and a thermal reservoir begin in
+a product state and evolve jointly by a unitary. The resulting entropy bookkeeping gives the exact
+Landauer identity and its usual lower bound.
+
+## A. Landauer process data
+
+## B. Initial and final states
+
+## C. Thermodynamic changes
+
+## D. The Landauer identity and bound
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open scoped MState
+
+namespace QuantumThermodynamics
+
+/-!
+## A. Landauer process data
+-/
+
+/-- A finite-dimensional Landauer process consisting of a system state, a thermal reservoir, and
+a joint unitary evolution. -/
+structure LandauerProcess (S R : Type*) [Fintype S] [DecidableEq S]
+    [Fintype R] [DecidableEq R] [Nonempty R] where
+  /-- The initial state of the system. -/
+  initialSystem : MState S
+  /-- The Hamiltonian of the reservoir. -/
+  reservoirHamiltonian : HermitianMat R ℂ
+  /-- The temperature of the reservoir. -/
+  reservoirTemperature : Temperature
+  /-- The joint unitary evolution of the system and reservoir. -/
+  evolution : Matrix.unitaryGroup (S × R) ℂ
+
+variable {S R : Type*} [Fintype S] [DecidableEq S]
+  [Fintype R] [DecidableEq R] [Nonempty R]
+
+namespace LandauerProcess
+
+/-!
+## B. Initial and final states
+-/
+
+/-- The initial thermal state of the reservoir. -/
+def initialReservoir (P : LandauerProcess S R) : MState R :=
+  MState.thermal P.reservoirHamiltonian P.reservoirTemperature
+
+/-- The initial product state of the system and reservoir. -/
+def initialJoint (P : LandauerProcess S R) : MState (S × R) :=
+  P.initialSystem ⊗ᴹ P.initialReservoir
+
+/-- The joint state after the unitary evolution. -/
+def finalJoint (P : LandauerProcess S R) : MState (S × R) :=
+  P.initialJoint.U_conj P.evolution
+
+/-- The final system marginal obtained by tracing out the reservoir. -/
+def finalSystem (P : LandauerProcess S R) : MState S :=
+  P.finalJoint.traceRight
+
+/-- The final reservoir marginal obtained by tracing out the system. -/
+def finalReservoir (P : LandauerProcess S R) : MState R :=
+  P.finalJoint.traceLeft
+
+/-!
+## C. Thermodynamic changes
+-/
+
+/-- The decrease in the system's von Neumann entropy. -/
+def systemEntropyDecrease (P : LandauerProcess S R) : ℝ :=
+  Sᵥₙ P.initialSystem - Sᵥₙ P.finalSystem
+
+/-- The increase in the reservoir's von Neumann entropy. -/
+def reservoirEntropyIncrease (P : LandauerProcess S R) : ℝ :=
+  Sᵥₙ P.finalReservoir - Sᵥₙ P.initialReservoir
+
+/-- The heat transferred to the reservoir, defined as its increase in expected energy. -/
+def reservoirHeat (P : LandauerProcess S R) : ℝ :=
+  P.finalReservoir.exp_val P.reservoirHamiltonian -
+    P.initialReservoir.exp_val P.reservoirHamiltonian
+
+/-- The relative entropy of the final reservoir state from its initial thermal state. -/
+def reservoirRelativeEntropy (P : LandauerProcess S R) : ℝ :=
+  (qRelativeEnt P.finalReservoir P.initialReservoir).toReal
+
+/-!
+## D. The Landauer identity and bound
+-/
+
+/-- The reservoir entropy increase is the system entropy decrease plus the final mutual
+information between system and reservoir. -/
+lemma entropyBalance (P : LandauerProcess S R) :
+    P.reservoirEntropyIncrease =
+      P.systemEntropyDecrease + qMutualInfo P.finalJoint := by
+  have hFinalEntropy : Sᵥₙ P.finalJoint = Sᵥₙ P.initialJoint := by
+    simp [finalJoint, Sᵥₙ]
+  have hInitialMutualInfo : qMutualInfo P.initialJoint = 0 := by
+    have h := qMutualInfo_as_qRelativeEnt P.initialJoint
+    simpa [initialJoint] using h
+  have hInitialEntropy :
+      Sᵥₙ P.initialJoint = Sᵥₙ P.initialSystem + Sᵥₙ P.initialReservoir := by
+    rw [qMutualInfo] at hInitialMutualInfo
+    simpa [initialJoint, add_comm] using (eq_add_of_sub_eq hInitialMutualInfo).symm
+  rw [reservoirEntropyIncrease, systemEntropyDecrease, qMutualInfo,
+    finalSystem, finalReservoir]
+  rw [hFinalEntropy, hInitialEntropy]
+  ring
+
+/-- The exact Landauer identity: the scaled reservoir heat is the system entropy decrease plus
+the final mutual information and reservoir relative entropy. -/
+lemma landauerIdentity (P : LandauerProcess S R) :
+    (P.reservoirTemperature.β : ℝ) * P.reservoirHeat =
+      P.systemEntropyDecrease + qMutualInfo P.finalJoint +
+        P.reservoirRelativeEntropy := by
+  rw [← P.entropyBalance]
+  exact MState.gibbsRelativeEntropyBalance P.finalReservoir P.reservoirHamiltonian
+    P.reservoirTemperature
+
+/-- Landauer's bound: the system entropy decrease does not exceed the reservoir heat multiplied
+by the inverse temperature. -/
+lemma landauerBound (P : LandauerProcess S R) :
+    P.systemEntropyDecrease ≤
+      (P.reservoirTemperature.β : ℝ) * P.reservoirHeat := by
+  rw [P.landauerIdentity]
+  have hMutualInfo : 0 ≤ qMutualInfo P.finalJoint := by
+    have h := congrArg EReal.toReal (qMutualInfo_as_qRelativeEnt P.finalJoint)
+    have hToReal :
+        qMutualInfo P.finalJoint =
+          (qRelativeEnt P.finalJoint
+            (P.finalJoint.traceRight ⊗ᴹ P.finalJoint.traceLeft)).toReal := by
+      simpa [EReal.toReal_coe_ennreal] using h
+    rw [hToReal]
+    exact ENNReal.toReal_nonneg
+  have hRelativeEntropy : 0 ≤ P.reservoirRelativeEntropy :=
+    ENNReal.toReal_nonneg
+  linarith
+
+end LandauerProcess
+
+end QuantumThermodynamics