TH2: the second law as coarse-grained entropy monotonicity

Category: conceptually 1-Mathlib (CSD-free general quantum statistical mechanics) with a CSD reading; kept in the CSD.Thermo tree alongside TH1 because its physical content is the CSD H-theorem.

The CSD thermodynamic picture (specs/thermo-plan.md): the fine-grained de-isolation flow is unitary, hence entropy-conserving (Liouville / reversibility); irreversibility enters through coarse-graining — passing to the pointer-basis diagonal (dephasing). This module proves the H-theorem form of the second law for that coarse-graining:

`S(ρ) ≤ S(pinch ρ)`,

pinching (dephasing to the pointer-basis diagonal) never decreases the von Neumann entropy. The fine-grained step conserves entropy (vonNeumannEntropy_conj_unitary, K1); the coarse-graining step increases it. Together: reversible microdynamics, entropy increase from coarse-graining — the Boltzmann/Gibbs picture, native to the CSD substrate.

Main results

• pinch : the pointer-basis dephasing / coarse-graining map ρ ↦ diagonal (fun i => (ρ i i).re). Hermitian; trace-preserving on densities; positive-definite when the pointer weights are all positive.
• vonNeumannEntropy_le_pinching (TH2, the H-theorem): for a density ρ with strictly positive pointer weights, S(ρ) ≤ S(pinch ρ). Via Klein's inequality D(ρ ‖ pinch ρ) ≥ 0 and the diagonal identity Tr(ρ · log(pinch ρ)) = Tr(pinch ρ · log(pinch ρ)) = −S(pinch ρ).
• entropy_reversible_then_coarsegrain (the second-law statement): a fine-grained unitary step conserves entropy and the following coarse-graining does not decrease it, so S(ρ) ≤ S(pinch (U ρ Uᴴ)).
• entropy_production_nonneg (the sign of the second law): the entropy gained by pinching, S(pinch ρ) − S(ρ) ≥ 0. Its pure-state instance (S(ρ)=0, Born weights on the diagonal) is the entropy-production witness of the decoherence tier (LF6-B.3, decohere_vonNeumann_entropy_nonneg), recovered here as an instance of the general monotonicity.

Honest scope

The strict-positivity hypothesis on the pointer weights (pinch ρ positive-definite) is Klein's support condition; without it the finite negMulLog-junk expression can misbehave (the same discipline as relEntropy_nonneg). For a pure state with a vanishing Born weight the inequality still holds by continuity, but the clean Klein route needs full support; the pure-state corollary is stated under it. This is the H-theorem for a SPECIFIC coarse-graining (the pointer-basis pinch), not a universal second law, and it is a statement about the coarse-graining map, not a proof that a given state thermalises dynamically (that needs mixing / ETH; the CSD-microdynamics reading rests on the shared SO-1/D1 residue, as across the thermo track).

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no sorry, no new axioms. Reuses K1 (vonNeumannEntropy, vonNeumannEntropy_diagonal, vonNeumannEntropy_conj_unitary) and the Klein / relative-entropy layer (klein_inequality, cfc_eq_conj_diagonal, re_trace_self_log); nothing is re-proved.

The pointer-basis pinching (dephasing) map

noncomputable def CSD.Thermo.pinch {n : Type u_1} [DecidableEq n] (ρ : Matrix n n ℂ) : Matrix n n ℂ

The pointer-basis pinching (dephasing) map: replace ρ by the diagonal matrix of its (real) diagonal entries. This is the coarse-graining that discards the off-diagonal coherences in the pointer basis — the irreversible step of a de-isolation measurement.

Equations

• CSD.Thermo.pinch ρ = Matrix.diagonal fun (i : n) => ↑(ρ i i).re

@[simp]

theorem CSD.Thermo.pinch_apply {n : Type u_1} [DecidableEq n] (ρ : Matrix n n ℂ) (i j : n) : pinch ρ i j = if i = j then ↑(ρ i i).re else 0

theorem CSD.Thermo.pinch_isHermitian {n : Type u_1} [DecidableEq n] (ρ : Matrix n n ℂ) : (pinch ρ).IsHermitian

pinch ρ is Hermitian (a real-diagonal matrix).

theorem CSD.Thermo.diag_ofReal_re_of_isHermitian {n : Type u_1} {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (i : n) : ↑(ρ i i).re = ρ i i

On a Hermitian ρ, the pinched diagonal entry IS the original diagonal entry: ρ i i = (ρ i i).re, since Hermitian forces real diagonal.

theorem CSD.Thermo.pinch_trace_of_isHermitian {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) : (pinch ρ).trace = ρ.trace

Pinching preserves the trace of a Hermitian matrix (real diagonal): the diagonal is untouched.

theorem CSD.Thermo.pinch_trace_one {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hρ : ρ.IsHermitian) (htr : ρ.trace = 1) : (pinch ρ).trace = 1

Pinching a trace-one density gives a trace-one density.

theorem CSD.Thermo.pinch_posDef {n : Type u_1} [DecidableEq n] {ρ : Matrix n n ℂ} (hpos : ∀ (i : n), 0 < (ρ i i).re) : (pinch ρ).PosDef

When all pointer weights (ρ i i).re are strictly positive, pinch ρ is positive-definite (Klein's support condition).

The cfc log of a pinched (diagonal) state

theorem CSD.Thermo.pinch_cfc {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : Matrix n n ℂ) (f : ℝ → ℝ) : ⋯.cfc f = Matrix.diagonal fun (i : n) => ↑(f (ρ i i).re)

The continuous functional calculus of a real function on the pinched (diagonal) state is diagonal: cfc f (pinch ρ) = diagonal (f ∘ pointer-weights). Instance of cfc_eq_conj_diagonal at the trivial diagonalisation U = 1.

The cross term Tr(ρ · log(pinch ρ))

theorem CSD.Thermo.re_trace_mul_pinch_cfc_log {n : Type u_1} [Fintype n] [DecidableEq n] (ρ : Matrix n n ℂ) : RCLike.re (ρ * ⋯.cfc Real.log).trace = ∑ i : n, (ρ i i).re * Real.log (ρ i i).re

The diagonal cross-term identity. Re Tr(ρ · cfc log (pinch ρ)) sees only the diagonal of ρ, so it collapses to the pointer-weight sum ∑ᵢ (ρ i i).re · log((ρ i i).re) = −S(pinch ρ). This is the crux of the H-theorem: the relative-entropy cross term is the pinched self-entropy.

The H-theorem

theorem CSD.Thermo.vonNeumannEntropy_le_pinching {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) (hpos : ∀ (i : n), 0 < (ρ i i).re) : QuantumInfo.vonNeumannEntropy ⋯ ≤ QuantumInfo.vonNeumannEntropy ⋯

TH2 — the second law (H-theorem for pointer-basis coarse-graining). For a density ρ with strictly positive pointer weights, pinching does not decrease the von Neumann entropy:

`S(ρ) ≤ S(pinch ρ)`.

Proof: Klein's inequality gives Tr(ρ log ρ) ≥ Tr(ρ log(pinch ρ)); the RHS is −S(pinch ρ) by the diagonal cross-term identity, the LHS is −S(ρ) by re_trace_self_log.

The second-law statement: reversible step + coarse-graining

theorem CSD.Thermo.entropy_reversible_then_coarsegrain {n : Type u_1} [Fintype n] [DecidableEq n] {ρ U : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (_htr : ρ.trace = 1) (hU : star U * U = 1) (hUρU : (U * ρ * star U).IsHermitian) (hpsdU : (U * ρ * star U).PosSemidef) (htrU : (U * ρ * star U).trace = 1) (hpos : ∀ (i : n), 0 < ((U * ρ * star U) i i).re) : QuantumInfo.vonNeumannEntropy ⋯ ≤ QuantumInfo.vonNeumannEntropy ⋯

The second-law statement. A fine-grained unitary step (the reversible de-isolation microdynamics) conserves entropy, and the subsequent coarse-graining (pinching to the pointer basis) does not decrease it:

`S(ρ) = S(U ρ Uᴴ) ≤ S(pinch (U ρ Uᴴ))`.

The entropy of the isolated (unitarily-evolved) system is unchanged; all entropy production is in the coarse-graining.

theorem CSD.Thermo.entropy_production_nonneg {n : Type u_1} [Fintype n] [DecidableEq n] {ρ : Matrix n n ℂ} (hpsd : ρ.PosSemidef) (htr : ρ.trace = 1) (hpos : ∀ (i : n), 0 < (ρ i i).re) : 0 ≤ QuantumInfo.vonNeumannEntropy ⋯ - QuantumInfo.vonNeumannEntropy ⋯

Entropy production is non-negative (restatement of TH2): the entropy gained by pinching, S(pinch ρ) − S(ρ), is ≥ 0. This is the sign of the second law — coarse-graining produces entropy, never destroys it. The pure-state instance (S(ρ) = 0, so S(pinch ρ) ≥ 0 with the Born weights on the diagonal) is the entropy-production witness already recorded at LF6-B.3 (decohere_vonNeumann_entropy_nonneg); here it is the general monotonicity.