auto-task(CanonicalEnsemble): add API-map.yaml tracking the canonical ensemble API

[doxtor6]

Summary

Adds Physlib/StatisticalMechanics/CanonicalEnsemble/API-map.yaml, the in-repo tracker for the
Canonical ensemble API (Physlib/StatisticalMechanics/CanonicalEnsemble/). The map is
generated from the directory's four Lean files (Basic.lean, Lemmas.lean, Finite.lean,
TwoState.lean), with GitHub issue
#892 "API: Canonical Ensemble"
used only as a reference for intended scope. No Lean source is touched; lake build stays green
(a YAML-only change).

This redoes PR #1266, which was
approved ("Looks good!") and then closed at the maintainer's request specifically so it could
be resubmitted with this improved tick-box description. The directory has no API-map.yaml on
master, and no open PR adds or edits one (checked gh pr list and the changed files of the
likely candidates).

Links below pin commit 2e21835a so line numbers are stable.

A note on the issue vs. the code

Issue #892 is a stub carrying the requirements-needed label — it has no requirement
checklist — so every requirement below was generated from what the directory's Lean files
actually contain, and each done flag was decided by reading the code. The two done: false
items are not invented: they come from the directory's own informal_lemma placeholders in
TwoState.lean. The issue's only concrete datum, "Parent APIs: #861" (Temperature), matches the
code's imports and is used for ParentAPIs.

---

Field-by-field justification (reviewer tick-box)

Title / Overview

Title: Canonical ensemble

Overview: |
    The key data structure `CanonicalEnsemble` describes a system in thermal
    equilibrium with a heat bath at fixed temperature `T`, given by a measurable type
    of microstates, an energy function, and the semi-classical data (degrees of
    freedom and phase-space unit) needed to form dimensionless thermodynamic
    quantities. The API gives a measure-theoretic formalization (uniform over discrete
    and continuous models) of the partition function, Boltzmann/probability measures,
    mean energy, entropies, and Helmholtz free energy, together with the fundamental
    identities `F = U - T S` and `U = -∂_β log Z`, the fluctuation-dissipation theorem,
    and the composition of ensembles.

Grounded in the Basic.lean module docstring
(Basic.lean#L10-L27):

A canonical ensemble describes a system in thermal equilibrium with a heat bath at fixed
temperature T. This file gives a measure–theoretic, semi–classical formalization intended to
work uniformly for discrete (counting measure) and continuous (Lebesgue–type) models.

and its "Roadmap" section
(Basic.lean#L95-L100):

Subsequent files (Lemmas.lean) prove: … Fundamental identity F = U - T S.
Derivative (response) formulas: U = -∂_β log Z.

ParentAPIs

ParentAPIs:
  - Temperature (Physlib/Thermodynamics/Temperature)

Determined from the only Physlib API import in the directory
(Basic.lean#L9):

public import Physlib.Thermodynamics.Temperature.Basic

which is used throughout via Temperature, T.β, and kB (e.g.
Basic.lean#L319-L320).
Issue #892 agrees: its "Parent APIs" section lists exactly
#861 "API: Temperature".

References

References:
  - L. D. Landau & E. M. Lifshitz, Statistical Physics, Part 1 (§31).
  - D. Tong, Lectures on Statistical Physics (Cambridge), https://www.damtp.cam.ac.uk/user/tong/statphys/one.pdf and https://www.damtp.cam.ac.uk/user/tong/statphys/two.pdf

Taken verbatim from the module docstrings — nothing invented. Basic.lean §8 References
(Basic.lean#L88-L93):

## 8. References

* L. D. Landau & E. M. Lifshitz, *Statistical Physics, Part 1*.
* D. Tong, Cambridge Lecture Notes (sections on canonical ensemble).
  - https://www.damtp.cam.ac.uk/user/tong/statphys/one.pdf
  - https://www.damtp.cam.ac.uk/user/tong/statphys/two.pdf

The §31 pin comes from Finite.lean
(Finite.lean#L42-L45).

---

Requirements

✅ 1. Key data structure and composition operations

- description: >
    The key data structure of the canonical ensemble (microstates type, energy
    function, degrees of freedom, phase-space unit, and a σ-finite measure) is
    defined, together with composition operations: addition of independent
    ensembles, `n` non-interacting copies, and transport along measurable
    equivalences.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (CanonicalEnsemble, HAdd instance, nsmul, congr)

Basic.lean#L108-L128:

/-- A Canonical ensemble is described by a type `ι`, corresponding to the type of microstates,
and a map `ι → ℝ` which associates which each microstate an energy
and physical constants needed to define dimensionless thermodynamic quantities. -/
structure CanonicalEnsemble (ι : Type) [MeasurableSpace ι] : Type where
  energy : ι → ℝ
  dof : ℕ
  phaseSpaceunit : ℝ := 1
  ...
  μ : MeasureTheory.Measure ι := by volume_tac
  [μ_sigmaFinite : SigmaFinite μ]

Composition: HAdd instance
Basic.lean#L147-L159,
congr
Basic.lean#L168-L180,
nsmul
Basic.lean#L188-L196:

/-- Scalar multiplication of `CanonicalEnsemble`, defined such that
`nsmul n 𝓒` represents `n` non-interacting, distinguishable copies of the ensemble `𝓒`. -/
noncomputable def nsmul (n : ℕ) (𝓒 : CanonicalEnsemble ι) : CanonicalEnsemble (Fin n → ι) where

✅ 2. Boltzmann measure, probability measure, and densities

- description: >
    The API defines the (unnormalized) Boltzmann measure and the normalized
    probability measure, and the pointwise mathematical and physical (dimensionless)
    probability densities.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (μBolt, μProd, probability, physicalProbability)

μBolt
Basic.lean#L318-L320:

/-- The Boltzmann measure on the space of microstates. -/
noncomputable def μBolt (T : Temperature) : MeasureTheory.Measure ι :=
  𝓒.μ.withDensity (fun i => ENNReal.ofReal (exp (- T.β * 𝓒.energy i)))

μProd
Basic.lean#L514-L517,
probability
Basic.lean#L480-L486,
physicalProbability
Basic.lean#L908-L912.

✅ 3. Mathematical and physical partition functions

- description: >
    The API defines the mathematical partition function `∫ exp(-β E) dμ` and the
    physical dimensionless partition function `Z = Z_math / h^dof`, with positivity
    lemmas.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (mathematicalPartitionFunction, partitionFunction)

Basic.lean#L401-L404
and
Basic.lean#L756-L758:

noncomputable def mathematicalPartitionFunction (T : Temperature) : ℝ := (𝓒.μBolt T).real Set.univ
...
/-- The dimensionless thermodynamic partition function, `Z = Z_math / h^dof`. -/
noncomputable def partitionFunction (T : Temperature) : ℝ :=
  𝓒.mathematicalPartitionFunction T / (𝓒.phaseSpaceunit ^ 𝓒.dof)

Positivity: mathematicalPartitionFunction_pos
Basic.lean#L469-L474,
partitionFunction_pos
Basic.lean#L765-L771.

✅ 4. Mean energy, mean-square energy, variance

- description: >
    The API defines the mean energy, mean-square energy, and energy variance, and
    proves `Var(E) = <E²> - <E>²`.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (meanEnergy, meanSquareEnergy, energyVariance); Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean (energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq)

Basic.lean#L630-L639:

/-- The mean energy of the canonical ensemble at temperature `T`. -/
noncomputable def meanEnergy (T : Temperature) : ℝ := ∫ i, 𝓒.energy i ∂𝓒.μProd T

Variance identity
Lemmas.lean#L656-L661:

/-- The identity Var(E) = ⟨E²⟩ - ⟨E⟩². -/
theorem energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq

✅ 5. Helmholtz free energy

- description: The API defines the Helmholtz free energy `F = -kB T log Z`.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (helmholtzFreeEnergy)

Basic.lean#L837-L840:

/-- The Helmholtz free energy, `F = -k_B T log(Z)`. This is the central
quantity from which other thermodynamic properties are derived. -/
noncomputable def helmholtzFreeEnergy (T : Temperature) : ℝ :=
  - kB * T.val * Real.log (𝓒.partitionFunction T)

✅ 6. Differential, thermodynamic, and Shannon entropies

- description: >
    The API defines the differential entropy and the absolute thermodynamic entropy,
    and (in the finite case) proves the thermodynamic entropy equals the Shannon
    entropy `-kB ∑ p log p`.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Basic.lean (differentialEntropy, thermodynamicEntropy); Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean (shannonEntropy, thermodynamicEntropy_eq_shannonEntropy)

differentialEntropy
Basic.lean#L693-L697,
thermodynamicEntropy
Basic.lean#L1023-L1027:

/-- The absolute thermodynamic entropy, defined from its statistical mechanical foundation as
the Gibbs-Shannon entropy of the dimensionless physical probability distribution. ... -/
noncomputable def thermodynamicEntropy (T : Temperature) : ℝ :=
  -kB * ∫ i, Real.log (𝓒.physicalProbability T i) ∂(𝓒.μProd T)

shannonEntropy
Finite.lean#L160-L165,
equality theorem
Finite.lean#L281-L286:

theorem thermodynamicEntropy_eq_shannonEntropy [MeasurableSingletonClass ι] [IsFinite 𝓒]
    (T : Temperature) :
    𝓒.thermodynamicEntropy T = 𝓒.shannonEntropy T := by

✅ 7. Fundamental identity F = U - T S

- description: The API proves the fundamental thermodynamic identity `F = U - T S`.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean (helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy)

Lemmas.lean#L241-L250:

theorem helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy
    (T : Temperature) (hT : 0 < T.val)
    [IsFiniteMeasure (𝓒.μBolt T)] [NeZero 𝓒.μ]
    (hE : Integrable 𝓒.energy (𝓒.μProd T)) :
    𝓒.helmholtzFreeEnergy T
      = 𝓒.meanEnergy T - T.val * 𝓒.thermodynamicEntropy T := by

✅ 8. Response formula U = -∂_β log Z

- description: The API proves the mean energy is `U = -∂_β log Z`.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean (meanEnergy_eq_neg_deriv_log_Z_of_beta)

Lemmas.lean#L628-L642:

theorem meanEnergy_eq_neg_deriv_log_Z_of_beta
    ...
    𝓒.meanEnergy T =
      - (derivWithin
          (fun β : ℝ => Real.log (𝓒.partitionFunction (ofβ (Real.toNNReal β))))
          (Set.Ioi 0) (T.β : ℝ)) := by

(The mathematical-partition-function version meanEnergy_eq_neg_deriv_log_mathZ_of_beta is at
Lemmas.lean#L453-L464.)

✅ 9. Heat capacity and fluctuation-dissipation theorem

- description: >
    The API defines the heat capacity and proves the fluctuation-dissipation theorem
    `C_V = Var(E) / (kB T²)` for finite ensembles.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean (heatCapacity, fluctuation_dissipation_energy_parametric); Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean (fluctuation_dissipation_theorem_finite)

heatCapacity
Lemmas.lean#L702-L704,
parametric FDT
Lemmas.lean#L731-L738,
and the finite case
Finite.lean#L473-L476:

/-- FDT for finite canonical ensembles: C_V = Var(E) / (k_B T²). -/
theorem fluctuation_dissipation_theorem_finite
    [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) (hT_pos : 0 < T.val) :
    𝓒.heatCapacity T = 𝓒.energyVariance T / (kB * (T.val : ℝ)^2) := by

✅ 10. Finite (discrete) specialization

- description: >
    The API specializes the framework to systems with finitely many discrete
    microstates via the `IsFinite` class, reducing the integral definitions to finite
    sums (e.g. `Z = ∑ᵢ exp(-β Eᵢ)`).
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/Finite.lean (IsFinite, partitionFunction_of_fintype, meanEnergy_of_fintype)

Finite.lean#L62-L69:

class IsFinite (𝓒 : CanonicalEnsemble ι) [Fintype ι] : Prop where
  μ_eq_count : 𝓒.μ = Measure.count
  dof_eq_zero : 𝓒.dof = 0
  phase_space_unit_eq_one : 𝓒.phaseSpaceunit = 1

Sum reductions
Finite.lean#L174-L177
and
Finite.lean#L201-L202:

lemma partitionFunction_of_fintype [IsFinite 𝓒] (T : Temperature) :
    𝓒.partitionFunction T = ∑ i, exp (- T.β * 𝓒.energy i) := by

✅ 11. Two-state ensemble with closed forms

- description: >
    The API constructs the concrete two-state ensemble and proves closed forms for
    its partition function, state probabilities, and mean energy.
  done: true
  location: Physlib/StatisticalMechanics/CanonicalEnsemble/TwoState.lean (twoState, twoState_partitionFunction_apply, twoState_probability_fst, twoState_probability_snd, twoState_meanEnergy_eq)

TwoState.lean#L27-L33:

/-- The canonical ensemble corresponding to state system, with one state of energy
  `E₀` and the other state of energy `E₁`. -/
noncomputable def twoState (E₀ E₁ : ℝ) : CanonicalEnsemble (Fin 2) where

Closed forms:
TwoState.lean#L39-L42
(partition function),
TwoState.lean#L60-L62
/
TwoState.lean#L77-L79
(probabilities),
TwoState.lean#L94-L96
(mean energy).

❌ 12. Two-state entropy simplification (not yet done)

- description: >
    The API shall prove a closed-form simplification of the thermodynamic entropy of
    the two-state ensemble.
  done: false
  location: N/A

Taken from the directory's own placeholder — an informal_lemma, i.e. a stated-but-unproven
TODO
(TwoState.lean#L101-L104):

/-- A simplification of the `entropy` of the two-state canonical ensemble. -/
informal_lemma twoState_entropy_eq where
  tag := "EVJJI"
  deps := [``twoState, ``thermodynamicEntropy]

❌ 13. Two-state Helmholtz free energy simplification (not yet done)

- description: >
    The API shall prove a closed-form simplification of the Helmholtz free energy of
    the two-state ensemble.
  done: false
  location: N/A

Likewise from the directory's informal_lemma placeholder
(TwoState.lean#L106-L109):

/-- A simplification of the `helmholtzFreeEnergy` of the two-state canonical ensemble. -/
informal_lemma twoState_helmholtzFreeEnergy_eq where
  tag := "EVMPR"
  deps := [``twoState]

---

Verification

• YAML parses (python -c "import yaml; yaml.safe_load(...)") and follows the v0.1 schema
  exactly (only the six prescribed top-level fields; every done: true has a real location,
  every done: false has location: N/A).
• Every declaration named in a location was confirmed present in the current sources by
  reading the files and by grep.
• lake build passes — no Lean file is touched by this PR.

🤖 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]

Looks good - approved