feat(Thermodynamics): add foundational API

[nateabr]

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.

Contents

• 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

[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.

[nateabr]

RFC
t-thermodynamics

[jstoobysmith]

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]

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