diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean
index 71341f2fe..eb983af50 100644
--- a/PhyslibAlpha.lean
+++ b/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
diff --git a/PhyslibAlpha/QuantumThermodynamics/API-map.yaml b/PhyslibAlpha/QuantumThermodynamics/API-map.yaml
new file mode 100644
index 000000000..71edeca5e
--- /dev/null
+++ b/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
diff --git a/PhyslibAlpha/QuantumThermodynamics/Landauer.lean b/PhyslibAlpha/QuantumThermodynamics/Landauer.lean
new file mode 100644
index 000000000..663485395
--- /dev/null
+++ b/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
diff --git a/PhyslibAlpha/QuantumThermodynamics/ThermalState.lean b/PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
new file mode 100644
index 000000000..8f9da59ab
--- /dev/null
+++ b/PhyslibAlpha/QuantumThermodynamics/ThermalState.lean
@@ -0,0 +1,162 @@
+/-
+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 Physlib.Thermodynamics.Temperature.Basic
+public import QuantumInfo.Entropy.Relative
+
+/-!
+# Quantum thermal states
+
+This file defines the finite-dimensional quantum thermal (Gibbs) state associated with a
+Hamiltonian. It provides both a real inverse-temperature parametrization and the physical
+`Temperature` parametrization used by Physlib.
+
+The main result is the Gibbs relative-entropy balance. It identifies an energy change from a
+thermal state with the corresponding entropy change and quantum relative entropy.
+
+## A. The partition function
+
+## B. The thermal state
+
+## C. The Gibbs relative-entropy balance
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open scoped ComplexOrder InnerProductSpace RealInnerProductSpace HermitianMat
+
+variable {d : Type*} [Fintype d] [DecidableEq d] [Nonempty d]
+
+/-!
+## A. The partition function
+-/
+
+namespace HermitianMat
+
+/-- The quantum partition function `Z(β) = tr(exp(-βH))` at real inverse temperature `β`. -/
+noncomputable def partitionFunctionBetaReal (H : HermitianMat d ℂ) (β : ℝ) : ℝ :=
+  ((-β) • H).exp.trace
+
+/-- The finite-dimensional quantum partition function is strictly positive. -/
+lemma partitionFunctionBetaReal_pos (H : HermitianMat d ℂ) (β : ℝ) :
+    0 < H.partitionFunctionBetaReal β := by
+  exact HermitianMat.trace_pos (((-β) • H).exp_pos)
+
+end HermitianMat
+
+/-!
+## B. The thermal state
+-/
+
+namespace MState
+
+/-- The thermal (Gibbs) state `exp(-βH) / Z(β)` at real inverse temperature `β`.
+
+Unlike the classical `CanonicalEnsemble`, which is `Temperature`-primary, the
+quantum side takes a real `β` as the primitive: the functional-calculus lemma
+kit is stated most cleanly over `ℝ`, and real `β` keeps negative temperatures
+reachable. `MState.thermal` is the `Temperature`-facing entry point matching
+the classical idiom. -/
+noncomputable def thermalBetaReal (H : HermitianMat d ℂ) (β : ℝ) : MState d where
+  M := (H.partitionFunctionBetaReal β)⁻¹ • ((-β) • H).exp
+  nonneg := smul_nonneg (inv_nonneg.mpr (H.partitionFunctionBetaReal_pos β).le)
+    ((-β) • H).exp_nonneg
+  tr := by
+    rw [HermitianMat.trace_smul]
+    change (H.partitionFunctionBetaReal β)⁻¹ * H.partitionFunctionBetaReal β = 1
+    exact inv_mul_cancel₀ (H.partitionFunctionBetaReal_pos β).ne'
+
+/-- The thermal state associated with a Hamiltonian at a physical `Temperature`. -/
+noncomputable def thermal (H : HermitianMat d ℂ) (T : Temperature) : MState d :=
+  thermalBetaReal H (T.β : ℝ)
+
+/-- The matrix of a real-inverse-temperature thermal state is its normalized exponential. -/
+lemma thermalBetaReal_M (H : HermitianMat d ℂ) (β : ℝ) :
+    (thermalBetaReal H β).M =
+      (H.partitionFunctionBetaReal β)⁻¹ • ((-β) • H).exp := rfl
+
+/-- A real-inverse-temperature thermal state has trace one. -/
+lemma thermalBetaReal_trace (H : HermitianMat d ℂ) (β : ℝ) :
+    (thermalBetaReal H β).M.trace = 1 :=
+  (thermalBetaReal H β).tr
+
+/-- A finite-dimensional thermal state has full rank. -/
+lemma thermalBetaReal_nonSingular (H : HermitianMat d ℂ) (β : ℝ) :
+    (thermalBetaReal H β).M.NonSingular := by
+  rw [thermalBetaReal_M]
+  exact HermitianMat.nonSingular_smul
+    (isUnit_iff_ne_zero.mpr
+      (inv_ne_zero (H.partitionFunctionBetaReal_pos β).ne'))
+
+/-- The density matrix of a finite-dimensional thermal state is positive definite. -/
+lemma thermalBetaReal_posDef (H : HermitianMat d ℂ) (β : ℝ) :
+    (thermalBetaReal H β).M.mat.PosDef := by
+  exact (HermitianMat.nonSingular_iff_posDef_of_PSD (thermalBetaReal H β).nonneg).mp
+    (thermalBetaReal_nonSingular H β)
+
+/-- The physical-temperature thermal state is the real-`β` state at `Temperature.β`. -/
+@[simp]
+lemma thermal_eq_thermalBetaReal (H : HermitianMat d ℂ) (T : Temperature) :
+    thermal H T = thermalBetaReal H (T.β : ℝ) := rfl
+
+/-- The logarithm of a thermal state is `-βH - log Z(β)`. -/
+lemma thermalBetaReal_log (H : HermitianMat d ℂ) (β : ℝ) :
+    (thermalBetaReal H β).M.log =
+      Real.log (H.partitionFunctionBetaReal β)⁻¹ • (1 : HermitianMat d ℂ) +
+        (-β) • H := by
+  rw [thermalBetaReal_M]
+  rw [HermitianMat.log_smul
+    (inv_ne_zero (H.partitionFunctionBetaReal_pos β).ne')]
+  simp [HermitianMat.exp, HermitianMat.log, ← HermitianMat.cfc_comp]
+
+/-!
+## C. The Gibbs relative-entropy balance
+-/
+
+/-- For a thermal reference state, the energy change times `β` is the entropy change plus the
+quantum relative entropy from the final state to the thermal state. -/
+lemma gibbsRelativeEntropyBalanceBetaReal (ρ : MState d) (H : HermitianMat d ℂ) (β : ℝ) :
+    β * (ρ.exp_val H - (thermalBetaReal H β).exp_val H) =
+      Sᵥₙ ρ - Sᵥₙ (thermalBetaReal H β) +
+        (qRelativeEnt ρ (thermalBetaReal H β)).toReal := by
+  let γ := thermalBetaReal H β
+  haveI : γ.M.NonSingular := thermalBetaReal_nonSingular H β
+  have hLogExpVal (σ : MState d) :
+      ⟪σ.M, γ.M.log⟫ =
+        Real.log (H.partitionFunctionBetaReal β)⁻¹ + (-β) * σ.exp_val H := by
+    rw [show γ.M.log =
+      Real.log (H.partitionFunctionBetaReal β)⁻¹ • (1 : HermitianMat d ℂ) +
+        (-β) • H by exact thermalBetaReal_log H β]
+    simp [MState.exp_val, inner_add_right, HermitianMat.inner_smul_right,
+      HermitianMat.inner_one, σ.tr, mul_comm]
+  have hRelativeEntropyExpand :
+      (qRelativeEnt ρ γ).toReal = -Sᵥₙ ρ - ⟪ρ.M, γ.M.log⟫ := by
+    have h := congrArg EReal.toReal (qRelativeEnt_eq_neg_Sᵥₙ_add ρ γ)
+    simp only [HermitianMat.nonSingular_ker_bot, bot_le, if_true] at h
+    rw [EReal.toReal_add (by simp) (by simp) (by simp) (by simp)] at h
+    simpa [sub_eq_add_neg, EReal.toReal_coe_ennreal] using h
+  have hThermalEntropy :
+      Sᵥₙ γ =
+        -(Real.log (H.partitionFunctionBetaReal β)⁻¹ +
+          (-β) * γ.exp_val H) := by
+    rw [Sᵥₙ_eq_neg_trace_log]
+    rw [real_inner_comm]
+    rw [hLogExpVal γ]
+  change β * (ρ.exp_val H - γ.exp_val H) =
+    Sᵥₙ ρ - Sᵥₙ γ + (qRelativeEnt ρ γ).toReal
+  rw [hRelativeEntropyExpand, hThermalEntropy, hLogExpVal ρ]
+  ring
+
+/-- Temperature-parametrized form of the Gibbs relative-entropy balance. -/
+lemma gibbsRelativeEntropyBalance (ρ : MState d) (H : HermitianMat d ℂ) (T : Temperature) :
+    (T.β : ℝ) * (ρ.exp_val H - (thermal H T).exp_val H) =
+      Sᵥₙ ρ - Sᵥₙ (thermal H T) + (qRelativeEnt ρ (thermal H T)).toReal := by
+  exact gibbsRelativeEntropyBalanceBetaReal ρ H (T.β : ℝ)
+
+end MState