feat(Thermodynamics): add foundational API by nateabr · Pull Request #1365 · leanprover-community/physlib

nateabr · 2026-07-04T09:31:57Z

Summary

This PR is larger than the usual Physlib standard, but I am still opening it as one PR
because I believe it is easier to review as one connected piece.

The goal is to make thermodynamics usable in Physlib and, hopefully, to enable parallel
development in two directions at once.

First, it adds an abstract accessibility-and-entropy interface following Lieb and Yngvason —
closely adapted from an existing Lean formalization (see Acknowledgements): thermodynamic
states are ordered by adiabatic accessibility, and entropy is represented as an
order-preserving, additive, extensive quantity.

Second, it adds the standard macroscopic coordinate presentation used in thermodynamics
courses. The reference used here is Callen's classic thermodynamics textbook.

The bridge between these layers is ThermoModel: a smooth coordinate entropy can be charted
into an abstract thermodynamic system, and the entropy principle for charted states is
derived from the entropy representation and the comparison hypothesis.

The ideal gas is included as a first concrete example. Its entropy is packaged as a
FundamentalRelation; the equations of state PV = NRT and U = cNRT are derived; and a
characterization theorem shows that those equations of state, plus one reference value,
determine the entropy.

Why This Is One PR

I recognize that this is a large PR. The reason I kept it together is that the components
justify each other:

the accessibility interface gives the second-law / order-theoretic foundation;
the coordinate layer gives the familiar macroscopic thermodynamics interface;
the bridge explains how the two views relate;
the ideal gas shows that the coordinate interface is inhabited by a standard physical
example.

Splitting this into several PRs would make each piece harder to evaluate in isolation. The
bridge needs both sides, and the example is useful precisely because it exercises the
definitions that come before it.

More broadly, I think this is a useful direction for Physlib. It lets newer pure-physics
contributors work with thermodynamics in the familiar macroscopic style, while also leaving
room for the formalization of the Lieb-Yngvason second law — a substantial
mathematical-physics result that would be a great addition to the library's API if we can
formalize it.

Foundation/Accessibility.lean
Defines thermodynamic systems, state spaces, composition, scaling, adiabatic
accessibility, Lieb-Yngvason-style world axioms, comparability, strict accessibility, and
basic preorder API.
Foundation/Entropy.lean
Defines entropy representations over all states, with monotonicity on comparable states,
additivity, extensivity, and affine uniqueness as a statement.
FundamentalRelation/Basic.lean
Defines positive extensive states, the positive orthant, and FundamentalRelation.
FundamentalRelation/Intensive.lean
Defines entropy partials, temperature, pressure, chemical potential, coordinate-derivative
lemmas, the total differential, and uniqueness from the entropy partials plus one
reference value.
FundamentalRelation/Euler.lean
Proves Euler's homogeneous-function identity and the thermodynamic Euler relation
U = T*S - P*V + μ*N.
FundamentalRelation/Model.lean
Defines ThermoModel, the bridge from a smooth fundamental relation to the abstract
entropy/accessibility interface.
IdealGas/Basic.lean
Extends the existing ideal-gas entropy formalization with idealGasFR, derivative
formulas, equations of state, and a characterization theorem.

Scope

The foundation files define interfaces and assumptions; they do not construct entropy from
accessibility.

The smooth coordinate layer assumes regularity, extensivity, and a positive energy
derivative.

The comparison hypothesis is carried explicitly where needed. It is not assumed globally by
the accessibility interface.

Limitations and Follow-Up

ThermoModel is a bridge interface, but this PR does not yet instantiate it for the ideal
gas. The ideal gas is packaged as a FundamentalRelation and its equations of state are
proved, but connecting that coordinate model to an abstract accessibility/entropy world will
require more API around charts, state spaces, and model construction.

The Callen-style coordinate layer is still small and needs significant development.

The existing Thermodynamics.Temperature files are not integrated here. I am still working
out how that material should relate to the entropy-representation development. One possible
direction is to use it later as part of a bridge between statistical thermodynamics and
macroscopic thermodynamics, but that design is not settled in this PR.

Thermodynamics.Basic remains a stub / register file for now. If this PR is accepted, I plan
to follow up with a cleanup pass that organizes the public thermodynamics API more
deliberately.

The immediate aim is to land enough structure that future work has clear places to attach:
more Callen-style identities, concrete ThermoModel instances, better public module
organization, and eventually connections to statistical thermodynamics.

Request for Comments

The main goal of this PR is to gather constructive feedback. I would welcome suggestions and
questions — they would help me think through details I may not have considered yet, so we can
iteratively refine the PR and work toward getting it merged.

Acknowledgements

The Lieb-Yngvason portion of this PR would not have been possible without the excellent work
in the repository linked below. Much of the accessibility-and-entropy material is adapted
very closely from it; my changes there are largely refactoring to fit Physlib's conventions,
together with the ThermoModel bridge — the new piece that aims to connect standard
macroscopic thermodynamics to the Lieb-Yngvason construction of entropy. That project has
made remarkable progress, and it puts a full formalization of the Lieb-Yngvason second law
within reach for Physlib, which would be a great milestone for the project.

https://github.com/or4nge19/ThermodynamicsLean

Introduce the abstract thermodynamics interface: - Accessibility.lean: thermodynamic systems, state spaces, composition, scaling, the primitive accessibility relation, Lieb-Yngvason-style worlds, comparability, strict accessibility, and preorder API. - Entropy.lean: entropy representations with monotonicity on comparable states, additivity, extensivity, basic order consequences, and affine uniqueness as a statement. The fields are assumptions of the interface; no entropy is constructed here.

Add the entropy-representation coordinate layer for simple systems: - Basic.lean: positive extensive states, the positive orthant, FundamentalRelation, and strict monotonicity in energy. - Intensive.lean: entropy partials, intensive parameters, positive temperature, coordinate derivatives, the total differential, and uniqueness from entropy partials. - Euler.lean: Euler's homogeneous-function identity and U = T*S - P*V + mu*N.

Connect a smooth fundamental relation to the abstract accessibility and entropy interface. ThermoModel bundles a thermodynamic core, a chart from positive extensive states, an entropy representation, entropy agreement, and the Comparison Hypothesis; the entropy principle is derived from these assumptions.

Extend the ideal-gas entropy formalization with its FundamentalRelation instance, entropy derivatives, equations of state PV = NRT and U = cNRT, and the characterization theorem showing that those equations of state plus one reference value determine the entropy.

github-actions · 2026-07-04T09:32:26Z

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.

nateabr · 2026-07-04T09:33:03Z

RFC
t-thermodynamics

jstoobysmith · 2026-07-04T12:08:34Z

Not a full review right now, but one thing I think would help is reorganizing this a bit better around the key data structures. E.g. ExtensiveState should be in its own file if not directory.

It would also be nice if the justification for why given data structures have the fields they do is clear. For example, are the fields in ExtensiveState enough to uniquely define such a state, are any redundant etc?

nateabr · 2026-07-04T14:08:19Z

Thank you for the comments - this was very constructive. After thinking it through and working through some code, you're right that there are redundancies in some of the data structures I need to sort out. For example, ExtensiveState doesn't need to carry its positivity the way it currently does, the hU/hV/hN fields duplicate the posOrthant domain the relation is defined on, so that can be consolidated into a single source; and I noticed similar redundancies in a few of my other structures.

I'll address these along with a heavier refactor of the file structure, so that things hopefully become a bit easier to review. I'll add the awaiting-author label and remove it once I've addressed your comment - but if you find more comments please do add them here, or Zulip works too (I've also messaged on the thread there if that's easier).

awaiting-author

nateabr · 2026-07-09T08:46:14Z

Once again thanks for the feedback @jstoobysmith . I've reorganized around the key data structures.

On justifying the fields. I've leaned on the referenced literature and aimed to make the docstrings and documentation carry that justification. I recognize that a full justification of the Lieb–Yngvason side would need further API development and actual proofs rather than prose, but I think the prose is a reasonable start?

I think the PR is in a better state for review now, happy to address further comments whenever you have time.

nateabr · 2026-07-09T08:46:26Z

-awaiting-author

jstoobysmith

Some comments:

I've only looked at the FundamentlRelation part, (not including Model.lean).
Maybe we should make a PR just on these parts for now.
Can you show you get a unique equation for U (or have you already done this)?
If you can do 3, I think we should change the definition of temperature, pressure etc. to match those in Callen.

Otherwise this is very good, and nice.

jstoobysmith · 2026-07-09T09:10:08Z

+(`ℝ → ℝ → ℝ → ℝ`), with positivity carried by the field hypotheses and by `ExtensiveState`,
+and regularity is asserted only on the positive orthant (`posOrthant`).
+Strict monotonicity in `U` is derived via `dS_dU_pos` which is the pointwise primitive
+`∂S/∂U > 0` from which `strictMonoOn_U` follows.


Though maybe would be nice to give some examples from physical systems?

I was think of adding the standard Callen examples here, such as radiation or van der Waals systems, but I was slightly worried that formalizing those examples would bloat this file?

However, I did formalize the simple ideal gas in IdealGas.idealGasFR line 214 as a physical example, should this be moved into this file? or stay in their own model files?

Sorry - just meant in the doc string, not in the actual lean code.

jstoobysmith · 2026-07-09T09:14:19Z

+/-- A positive **extensive state** `(U, V, N)` of a simple system, the internal energy,
+volume, and particle number, all strictly positive. This is the physical domain over which a
+`FundamentalRelation` is smooth, homogeneous, and monotone. -/
+def ExtensiveState := {p : ℝ × ℝ × ℝ // p ∈ posOrthant}


I would have thought having ExtensiveState as a structure with the conditions that all its entries are positive makes more sense.

You are definitely right - I thought I did something super slick with this change, but upon a second read its quite clear I have made it unnecessarily convoluted.

Will revert to what it was before

jstoobysmith · 2026-07-09T09:17:54Z

+/-- The energy partial derivative `∂S/∂U` at a positive extensive state.
+
+In the entropy differential, this is the coefficient `1 / T` of `dU`. -/
+def FundamentalRelation.dS_dU (Φ : FundamentalRelation) (e : ExtensiveState) : ℝ :=


I think more explicit names would be better e.g. entropy_deriv_internalEnergy etc.

jstoobysmith · 2026-07-09T09:21:08Z

+
+## iv. References
+
+- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley


Page number, or link would be good here?

Agreed, I can give both.

jstoobysmith · 2026-07-09T09:31:50Z

+derives positivity from the subtype property. -/
+
+/-- The internal energy of an extensive state. -/
+def U (e : ExtensiveState) : ℝ := e.1.1


Would give more explicit names.

Agreed - will make the changes

jstoobysmith · 2026-07-09T09:32:02Z

+lemma hV (e : ExtensiveState) : 0 < e.V := e.2.2.1
+
+/-- Positivity of the particle number, from the subtype property. -/
+lemma hN (e : ExtensiveState) : 0 < e.N := e.2.2.2


likewise here

(can define notation though)

nateabr · 2026-07-09T17:05:47Z

Thank you for your careful comments @jstoobysmith, will begin working on them shortly

I agree that the best next step is probably to make this PR focus on the FundamentalRelation / coordinate part first, and leave the Lieb-Yngvason part out.

A side question on that, do you think the Lieb-Yngvason material is something we would eventually want in Physlib, or is it better treated as a separate/solo project? I’m asking mainly to gauge whether it is worth bringing back later as a follow-up PR.

On points 3 and 4, So when you ask whether we can “get a unique equation for U,” The word unique points me towards a uniqueness theorem, so something like for fixed S,V,N, there is at most one positive U satisfying Φ.S U V N = S; this should follow from dS/dU > 0 / strictMonoOn_U, I could package that as a theorem. But point 4 makes me believe you are suggesting an actual energetic representation U = U(S,V,N), with existence/range hypotheses, so that temperature, pressure, and chemical potential can be defined directly in Callen’s style from derivatives of U.

Some clarification before I start would be great :)

nateabr · 2026-07-09T17:06:25Z

-awaiting-author

(please add it back after you've answered the comment :))

jstoobysmith · 2026-07-10T04:08:36Z

Regarding the Lieb-Yngvason material. I absolutely think we should have it. I'm only suggesting splitting the PR up to make it easier to get it merged. We can get the FundamentalRelation stuff as good as we can before moving onto the Foundation stuff.

Callen seems to suggest that you can get a function U = U(S, V, N) if we can explicitly construct that (even through choice), I think it would be nice. Then at least we can show that the definition of temperature, pressure etc. matches those of Callen.

jstoobysmith · 2026-07-10T04:08:45Z

awaiting-author

nateabr · 2026-07-10T05:58:27Z

Okk great thanks for the clarification on Lieb-Ygnvason and I completely agree, in fact I should've split it up from the start.

I think what you're saying is possible with regards to U and this is probably the better design choice for further downstream development. I'll get on it :))

nateabr added 6 commits July 4, 2026 11:56

chore(Thermodynamics): register thermodynamics modules

f93e481

chore(Thermodynamics): fix linter findings

7a25636

github-actions Bot added RFC Request for comment t-thermodynamics Thermodynamics labels Jul 4, 2026

refactor(Thermodynamics): rename ThermoModel.coords to stateOf

6527289

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 4, 2026

refactor(Thermodynamics): address comments

85a71af

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 9, 2026

jstoobysmith reviewed Jul 9, 2026

View reviewed changes

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 9, 2026

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Jul 9, 2026

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Jul 10, 2026


		## iv. References

		- H.B. Callen, Thermodynamics and an Introduction to Thermostatistics, 2nd ed., Wiley

Uh oh!

Conversation

nateabr commented Jul 4, 2026

Summary

Why This Is One PR

Contents

Scope

Limitations and Follow-Up

Request for Comments

Acknowledgements

Uh oh!

github-actions Bot commented Jul 4, 2026

Uh oh!

nateabr commented Jul 4, 2026

Uh oh!

jstoobysmith commented Jul 4, 2026

Uh oh!

nateabr commented Jul 4, 2026

Uh oh!

nateabr commented Jul 9, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

nateabr commented Jul 9, 2026

Uh oh!

jstoobysmith left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

nateabr commented Jul 9, 2026

Uh oh!

nateabr commented Jul 9, 2026

Uh oh!

jstoobysmith commented Jul 10, 2026

Uh oh!

jstoobysmith commented Jul 10, 2026

Uh oh!

nateabr commented Jul 10, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

nateabr commented Jul 9, 2026 •

edited

Loading

nateabr commented Jul 10, 2026 •

edited

Loading