TH4: Landauer's principle (the thermodynamic cost of erasure)

Category: conceptually 1-Mathlib (CSD-free general quantum statistical mechanics) with a CSD reading; kept in the CSD.Thermo tree alongside TH1–TH3.

Glossary: https://glossary.constraintsurfacedynamics.com/landauer-principle/ Plain-language, CSD-role and formal statements of Landauer's principle, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh. On upstreaming: this is a Category 1 file. Strip this Glossary block before any Mathlib or Physlib PR; a personal project link has no place in a canonical header.

Landauer's principle: erasing information has an unavoidable thermodynamic cost. In the information-theoretic (Reeb–Wolf) form, a system S coupled unitarily to a bath B initially in the Gibbs state τ_B = exp(-βH_B)/Z at inverse temperature β obeys

`β · ΔQ ≥ S(ρ_S) − S(ρ_S')`,

where ΔQ = ⟨H_B⟩_{ρ_B'} − ⟨H_B⟩_{τ_B} is the heat dumped into the bath and ρ_S, ρ_S' are the system's initial and final reduced states. The right side is the entropy REMOVED from the system; the left is β times the dissipated heat. Resetting a maximally-mixed bit (S(ρ_S) = log 2) to a definite value (S(ρ_S') = 0) therefore costs ΔQ ≥ T log 2 = kT ln 2 — Landauer's bound.

The derivation (all from earlier tranches)

1. Entropy conservation (unitary + product): S(ρ_SB') = S(ρ_S ⊗ τ_B) = S(ρ_S) + S(τ_B), via vonNeumannEntropy_conj_unitary (K1) and vonNeumannEntropy_kronecker.
2. Subadditivity: S(ρ_SB') ≤ S(ρ_S') + S(ρ_B') (vonNeumannEntropy_subadditive). With (1): S(ρ_S) − S(ρ_S') ≤ S(ρ_B') − S(τ_B).
3. Bath Clausius inequality: S(ρ_B') − S(τ_B) ≤ β·ΔQ, i.e. β·ΔQ − (S(ρ_B') − S(τ_B)) = D(ρ_B' ‖ τ_B) ≥ 0 (relEntropy_nonneg), using the Gibbs log identity log τ_B = −βH_B − (log Z)·1 (TH3, re_trace_mul_log_gibbs).

Chaining (2) and (3) gives Landauer.

Honest scope

The final marginals ρ_S', ρ_B' are required positive-definite (full rank) — the support hypothesis Klein/subadditivity need; physically the generic case. The initial system state is taken positive-definite (so ρ_S ⊗ τ_B is; a maximally-mixed bit qualifies). This is the standard finite-dimensional Reeb–Wolf setting: a genuine bound, not the asymptotic/reversible idealisation. As across the thermo track it is a QM-stat-mech theorem with a CSD reading; the deterministic-microdynamics interpretation rests on the shared SO-1/D1 residue.

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no sorry, no new axioms. Reuses K1 (vonNeumannEntropy, subadditivity), the Klein / relative-entropy layer, and TH3 (gibbsState, re_trace_mul_log_gibbs); nothing is re-proved.

theorem CSD.Thermo.re_trace_self_eq_neg_entropy {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : RCLike.re (ρ * hρ.cfc Real.log).trace = -QuantumInfo.vonNeumannEntropy hρ

Re Tr(ρ · log ρ) = −S(ρ) for a density (self term of the relative entropy).

theorem CSD.Thermo.bath_clausius {m : Type u_2} [Fintype m] [DecidableEq m] [Nonempty m] (HB : Matrix m m ℂ) (hHB : HB.IsHermitian) (β : ℝ) {ρB : Matrix m m ℂ} (hpdB : ρB.PosDef) (htrB : ρB.trace = 1) : QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯ ≤ β * (energy HB ρB - energy HB (gibbsState HB hHB β))

The bath Clausius inequality. For any bath density ρ_B' and the Gibbs state τ_B = exp(-βH_B)/Z, the entropy gained by the bath is at most β times the heat it absorbs: S(ρ_B') − S(τ_B) ≤ β·(⟨H_B⟩_{ρ_B'} − ⟨H_B⟩_{τ_B}). This is D(ρ_B' ‖ τ_B) ≥ 0 rewritten through the Gibbs log identity — the thermodynamic face of relative-entropy non-negativity, and the engine of Landauer.

The Landauer bound

theorem CSD.Thermo.landauer_bound {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] [DecidableEq m] [Nonempty m] (HB : Matrix m m ℂ) (hHB : HB.IsHermitian) {β : ℝ} {ρS : Matrix n n ℂ} (hpdS : ρS.PosDef) (htrS : ρS.trace = 1) {U : Matrix (n × m) (n × m) ℂ} (hU : star U * U = 1) (hpdS' : (QuantumInfo.partialTraceRight (U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρS (gibbsState HB hHB β) * star U)).PosDef) (hpdB' : (QuantumInfo.partialTraceLeft (U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρS (gibbsState HB hHB β) * star U)).PosDef) : QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯ ≤ β * (energy HB (QuantumInfo.partialTraceLeft (U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρS (gibbsState HB hHB β) * star U)) - energy HB (gibbsState HB hHB β))

TH4 — Landauer's principle (Reeb–Wolf bound). A system S (initial state ρ_S, positive-definite) coupled by a global unitary U to a bath B initially in the Gibbs state τ_B = exp(-βH_B)/Z at inverse temperature β > 0, with full-rank final marginals, obeys

`S(ρ_S) − S(ρ_S') ≤ β · (⟨H_B⟩_{ρ_B'} − ⟨H_B⟩_{τ_B})`.

The left side is the entropy REMOVED from the system by the process; the right is β times the heat ΔQ dumped into the bath. Erasing information (decreasing S(ρ_S) towards a definite state) therefore forces a proportional heat cost — Landauer's principle. Proof: entropy conservation (unitary + product)

• subadditivity give S(ρ_S) − S(ρ_S') ≤ S(ρ_B') − S(τ_B); the bath Clausius inequality bounds the latter by β·ΔQ.

The one-bit corollary: ΔQ ≥ T log 2

theorem CSD.Thermo.landauer_one_bit {m : Type u_2} [Fintype m] [DecidableEq m] [Nonempty m] (HB : Matrix m m ℂ) (hHB : HB.IsHermitian) {β : ℝ} {ρS : Matrix (Fin 2) (Fin 2) ℂ} (hpdS : ρS.PosDef) (htrS : ρS.trace = 1) {U : Matrix (Fin 2 × m) (Fin 2 × m) ℂ} (hU : star U * U = 1) (hpdS' : (QuantumInfo.partialTraceRight (U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρS (gibbsState HB hHB β) * star U)).PosDef) (hpdB' : (QuantumInfo.partialTraceLeft (U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρS (gibbsState HB hHB β) * star U)).PosDef) (hSinit : QuantumInfo.vonNeumannEntropy ⋯ = Real.log 2) (hSfinal : QuantumInfo.vonNeumannEntropy ⋯ = 0) : Real.log 2 ≤ β * (energy HB (QuantumInfo.partialTraceLeft (U * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ρS (gibbsState HB hHB β) * star U)) - energy HB (gibbsState HB hHB β))

Landauer's kT ln 2 bound for erasing one bit. If the system is a single qubit initially maximally mixed (S(ρ_S) = log 2) and the erasure resets it to a definite (pure) state (S(ρ_S') = 0), the heat dumped into the bath satisfies

`log 2 ≤ β · ΔQ`,   equivalently   `ΔQ ≥ T · log 2 = kT ln 2`.

Stated as a consequence of landauer_bound given the two entropy end-points: the entropy removed is exactly log 2, so the dissipated heat is at least T log 2.