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

[fliingelephant]

Seeds a PhyslibAlpha/QuantumThermodynamics/ area: the quantum thermal (Gibbs) state as an MState constructor-family member, the Gibbs relative-entropy balance, a minimal Landauer erasure setup with the Landauer bound, and the area's API-map.yaml (exemplar format) recording done seeds and the open requirements (total correlation, thermal operations, thermo-majorization, quantum free energy).

Draft on purpose: opened early for direction feedback on the area layout and the MState.thermal naming before polishing toward ready-for-review.

Added declarations

PhyslibAlpha/QuantumThermodynamics/ThermalState.lean

• HermitianMat.partitionFunctionBetaReal, partitionFunctionBetaReal_pos — Z(β) = Tr exp(-βH) and its positivity.
• MState.thermalBetaReal, MState.thermal — the Gibbs state exp(-βH)/Z(β); real-β primitive (functional-calculus-friendly, negative temperatures reachable) with the Temperature-facing entry matching the classical CanonicalEnsemble idiom.
• Lemma kit: thermalBetaReal_M, thermalBetaReal_trace, thermalBetaReal_nonSingular, thermalBetaReal_posDef, thermal_eq_thermalBetaReal (simp normal form), thermalBetaReal_log.
• gibbsRelativeEntropyBalanceBetaReal, gibbsRelativeEntropyBalance — β(⟨H⟩_ρ − ⟨H⟩_γ) = S(γ) − S(ρ) + D(ρ‖γ) in both parametrizations.

PhyslibAlpha/QuantumThermodynamics/Landauer.lean

• LandauerProcess — system + finite reservoir at Temperature, coupled by a global unitary.
• State/bookkeeping defs: initialReservoir, initialJoint, finalJoint, finalSystem, finalReservoir, systemEntropyDecrease, reservoirEntropyIncrease, reservoirHeat, reservoirRelativeEntropy.
• entropyBalance — entropy production as mutual information plus reservoir relative entropy.
• landauerIdentity, landauerBound — the exact finite-β Landauer identity (Reeb–Wolf style) and the bound β·Q ≥ ΔS.

PhyslibAlpha/QuantumThermodynamics/API-map.yaml — area map: overview, ParentAPIs (QuantumInfo entropies/CFC, classical CanonicalEnsemble, Temperature), references, done + open requirements.

PhyslibAlpha.lean — registration of the two new modules.

Reviewer map

1. ThermalState.lean top-to-bottom (partition function → state → kit → balance).
2. Landauer.lean (structure → bookkeeping defs → the three lemmas).
3. API-map.yaml, then the registration line.

Notes for reviewers

• No existing declaration in QuantumInfo/ or Physlib/ covers a quantum Gibbs state, quantum partition function, or these results (searched by meaning; closest neighbor is a private normalized exponential inside the Stein's-lemma proof).
• All heavy facts are consumed from upstream (qRelativeEnt expansion, entropy lemmas, HermitianMat CFC positivity/log API) — nothing is re-proved.
• Builds green; runPhyslibAlphaLinters, alphaFileImports.py, noAlphaImports.py, and the style linters all pass; no sorryAx in the new modules.
• AI-assisted per AI-POLICY.md/AGENTS.md: commits carry the model co-author trailer; the human author will independently verify the bibliographic references and certifies the statements before this leaves draft.

🤖 Generated with Claude Code

[github-actions]

Thank you for this PR, which will now be reviewed. If submitting to ./Physlib or ./QuantumInfo, please see our review guidelines if you are not familiar with the process. You should expect a back and forth with a reviewer before your PR is merged. See also that link for how to add appropriate labels to your PR. The PR will also go through a number of automated checks. You can learn more about these here, including how to run them locally.

If you are submitting to ./PhyslibAlpha there will be a lighter review process, though your PR must still pass the automated checks.

If you want to bring attention to this PR, please write a message on this thread of the Lean Zulip.

Important: If a reviewer adds an awaiting-author label to your PR, once you have addressed the review comments, please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.

[jstoobysmith]

Hey, I've put some comments here. Normally for ./PhyslibAlpha we don't do a detailed review, but have done so since you asked for comments.

[jstoobysmith]

This generally looks quite good. Although it is not my area so I can't speak about specific details.

One thing that I think would improve this PR is a better description in the documentation about what the Landauer process is, and why you need this input data for it.

[jstoobysmith]

Have these references been checked or AI generated?

[jstoobysmith]

How does e.g. this relate to other partition functions we have in Physlib?

[jstoobysmith]

That said, I've someone who has more experience in this area then me might be able to say something more useful.