feat(Thermodynamics): add foundational API

Physlib.lean

@@ -464,6 +464,15 @@ public import Physlib.StringTheory.FTheory.SU5.Quanta.FiveQuanta
 public import Physlib.StringTheory.FTheory.SU5.Quanta.IsViable
 public import Physlib.StringTheory.FTheory.SU5.Quanta.TenQuanta
 public import Physlib.Thermodynamics.Basic
+public import Physlib.Thermodynamics.Foundation.Comparability
+public import Physlib.Thermodynamics.Foundation.Core
+public import Physlib.Thermodynamics.Foundation.Entropy
+public import Physlib.Thermodynamics.Foundation.World
+public import Physlib.Thermodynamics.FundamentalRelation.Basic
+public import Physlib.Thermodynamics.FundamentalRelation.Euler
+public import Physlib.Thermodynamics.FundamentalRelation.ExtensiveState
+public import Physlib.Thermodynamics.FundamentalRelation.Intensive
+public import Physlib.Thermodynamics.FundamentalRelation.Model
 public import Physlib.Thermodynamics.IdealGas.Basic
 public import Physlib.Thermodynamics.Temperature.Basic
 public import Physlib.Thermodynamics.Temperature.TemperatureUnits

Physlib/Thermodynamics/Foundation/Comparability.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaneal Sajan
+-/
+module
+
+public import Physlib.Thermodynamics.Foundation.Core
+
+/-!
+# Comparability of thermodynamic states
+
+## i. Overview
+
+Two states are *comparable* when at least one is adiabatically accessible from the other.
+They are *adiabatically equivalent* when accessibility holds in both directions. When it
+holds in only one direction, one state *strictly precedes* the other - this is what makes
+a process irreversible.
+
+Lieb-Yngvason's **comparison hypothesis** (CH) asserts that any two states of one state
+space are comparable. Crucially, CH is a *hypothesis*, and one of the aims of the paper is
+to *derive* it for simple systems from the thermal axioms, so we keep it as a named `Prop`
+that later entropy constructions carry as a separate assumption.
+
+The hypothesis comes in a strictly ordered hierarchy of scopes: `ComparisonHypothesis Γ`,
+comparing only the states of one system, is strictly weaker than CH restricted to all
+two-fold scaled products `(1−λ)Γ × λΓ`, which in turn is strictly weaker than
+`GlobalComparisonHypothesis`, comparing states across every pair of systems.
+
+## ii. Key results
+
+- `Comparable` — either state is accessible from the other.
+- `ComparisonHypothesis` — CH for a single system, the weakest tier of the scope
+  hierarchy above.
+- `GlobalComparisonHypothesis` — any two states of any two systems are comparable.
+- `StrictlyPrecedes` (`≺≺`) — irreversible accessibility.
+- `Comparable.symm` — comparability is symmetric.
+
+## iii. Table of contents
+
+- A. Comparability
+
+## iv. References
+
+- E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of
+  Thermodynamics*, Physics Reports **310** (1999) 1-96.
+-/
+
+@[expose] public section
+
+namespace Thermodynamics
+
+universe u
+
+/-! ## A. Comparability
+
+The comparability vocabulary over a bare operational core. -/
+
+section Core
+
+variable {System : Type u} [T : ThermoSystemCore System]
+
+/-- Two states are comparable if either is adiabatically accessible from the other,
+`X ≺ Y ∨ Y ≺ X`. -/
+def Comparable {Γ₁ Γ₂ : System} (X : T.State Γ₁) (Y : T.State Γ₂) : Prop :=
+  T.le X Y ∨ T.le Y X
+
+/-- The comparison hypothesis for a single system: any two of its states are comparable.
+This is the weakest tier of the scope hierarchy described in the module overview. -/
+def ComparisonHypothesis (Γ : System) : Prop :=
+  ∀ X Y : T.State Γ, Comparable (T := T) X Y
+
+/-- The global comparison hypothesis: any two states, possibly of different systems, are
+comparable. The strongest tier of the scope hierarchy described in the module
+overview. -/
+def GlobalComparisonHypothesis (System : Type u) [T : ThermoSystemCore System] : Prop :=
+  ∀ {Γ₁ Γ₂ : System} (X : T.State Γ₁) (Y : T.State Γ₂), Comparable (T := T) X Y
+
+/-- Strict adiabatic accessibility `X ≺≺ Y`: `X ≺ Y` but not `Y ≺ X`. These are the
+irreversible processes, the ones with strictly increasing entropy. -/
+def StrictlyPrecedes {Γ₁ Γ₂ : System} (X : T.State Γ₁) (Y : T.State Γ₂) : Prop :=
+  T.le X Y ∧ ¬ T.le Y X
+
+namespace Comparable
+
+/-- Comparability is symmetric. -/
+lemma symm {Γ₁ Γ₂ : System} {X : T.State Γ₁} {Y : T.State Γ₂}
+    (h : Comparable (T := T) X Y) : Comparable (T := T) Y X :=
+  Or.symm h
+
+end Comparable
+
+end Core
+
+end Thermodynamics

Physlib/Thermodynamics/Foundation/Core.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaneal Sajan
+-/
+module
+
+public import Mathlib.Data.Real.Basic
+public import Mathlib.Logic.Equiv.Defs
+
+/-!
+# The operational core of thermodynamics
+
+## i. Overview
+
+This module fixes the operational vocabulary of the abstract Lieb-Yngvason accessibility
+foundation, with no axioms attached.
+
+The primitive is a relation `≺` of **adiabatic accessibility** between equilibrium
+states: `X ≺ Y` means `Y` can be reached from `X` by an interaction with a device and a
+weight, the device returning to its initial state while the weight may change height. The
+eventual goal is an entropy `S` with `X ≺ Y ↔ S(X) ≤ S(Y)` on comparable states, additive
+and extensive, unique up to affine rescaling `S ↦ aS + B` (`a > 0`).
+
+A `ThermoSystemCore` records, for each *system*, its space of equilibrium *states*. Two
+operations build new systems from old ones: composition `⊗`, which places two systems
+side by side, and scaling `•`, which takes a `t`-sized copy of one. The zero system and
+the primitive relation `≺` complete the vocabulary.
+
+## ii. Key results
+
+- `ThermoSystemCore` — the operational vocabulary: systems, states, composition, scaling,
+  the zero system, and `≺`.
+- `comp_state`, `scale_state` — the states of composed and scaled systems associated to
+  component states.
+- `instInhabitedZState` — the zero-system state space is inhabited.
+
+## iii. Table of contents
+
+- A. Operational core (`ThermoSystemCore`)
+- B. Core API
+
+## iv. References
+
+- E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of
+  Thermodynamics*, Physics Reports **310** (1999).
+- E.H. Lieb and J. Yngvason, *The Mathematical Structure of the Second Law of
+  Thermodynamics*, Current Developments in Mathematics **2001** (2002).
+-/
+
+@[expose] public section
+
+namespace Thermodynamics
+
+universe u v
+
+/-! ## A. Operational core
+
+The operational vocabulary of thermodynamics, with no axioms attached. The
+`AccessibilityAxioms` class states the order axioms directly on this signature, and
+`ThermoWorld` bundles them with the system-algebra and cast-coherence layers. The fields
+are the primitive relation `≺`, the two system constructors `Γ₁ ⊗ Γ₂` and `t • Γ` with the
+identification of their state spaces, and the zero system.
+
+`comp` and `scale` build compound and scaled systems; `state_of_comp_equiv` and
+`state_of_scale_equiv` identify their state spaces, and axioms A3-A5 need these
+identifications to quantify over composed pairs `(X, Y)` and scaled states `tX`.
+
+`ZSystem` must be given directly rather than built from `scale`: `state_of_scale_equiv`
+only identifies state spaces for `t ≠ 0`, so nothing here pins down `scale 0 Γ`. The
+`SystemAlgebra` layer later characterizes `ZSystem` as exactly `scale 0 Γ` for every `Γ`
+(`scale_zero_is_ZSystem`); its unique state gives `instInhabitedZState`, the only
+state-space inhabitation this core guarantees. -/
+
+/-- The operational core of a thermodynamic accessibility structure: a state space for each
+system, composition `comp`, scaling `scale`, a zero system `ZSystem`, and the primitive
+adiabatic-accessibility relation `le` (`≺`). -/
+class ThermoSystemCore (System : Type u) where
+  /-- The state space associated to a thermodynamic system. -/
+  State : System → Type v
+  /-- Composition of thermodynamic systems. -/
+  comp : System → System → System
+  /-- Extensive scaling of thermodynamic systems by a real parameter. -/
+  scale : ℝ → System → System
+  /-- Primitive adiabatic accessibility `X ≺ Y`. -/
+  le {Γ₁ Γ₂ : System} : State Γ₁ → State Γ₂ → Prop
+  /-- The zero system. -/
+  ZSystem : System
+  /-- The zero system has a unique state. -/
+  State_ZSystem_is_Unit : Unique (State ZSystem)
+  /-- A state of a composed system is represented by a pair of states of the components. -/
+  state_of_comp_equiv {Γ₁ Γ₂ : System} : State (comp Γ₁ Γ₂) ≃ (State Γ₁ × State Γ₂)
+  /-- A state of a nonzero-scaled system is represented by a state of the original system. -/
+  state_of_scale_equiv {t : ℝ} (ht : t ≠ 0) {Γ : System} : State (scale t Γ) ≃ State Γ
+
+/-! ## B. Core API
+
+Small constructions built directly from the `ThermoSystemCore` fields.
+`comp_state` and `scale_state` name the reverse direction of `state_of_comp_equiv` and
+`state_of_scale_equiv`: building a composite or scaled state out of its components, which
+is the direction most call sites need. `instInhabitedZState` turns the zero system's
+unique state into an `Inhabited` instance for typeclass search. -/
+
+section Core
+
+variable {System : Type u} [T : ThermoSystemCore System]
+
+/-- The state of a composed system associated to a pair of component states. -/
+def comp_state {Γ₁ Γ₂ : System} (p : T.State Γ₁ × T.State Γ₂) :
+    T.State (T.comp Γ₁ Γ₂) :=
+  T.state_of_comp_equiv.symm p
+
+/-- The state of a nonzero-scaled system associated to a state of the original system. -/
+def scale_state {t : ℝ} (ht : t ≠ 0) {Γ : System} (X : T.State Γ) :
+    T.State (T.scale t Γ) :=
+  (T.state_of_scale_equiv ht).symm X
+
+/-- The zero-system state space is inhabited. -/
+instance instInhabitedZState (System : Type u) [T : ThermoSystemCore System] :
+    Inhabited (T.State T.ZSystem) :=
+  ⟨T.State_ZSystem_is_Unit.default⟩
+
+end Core
+
+end Thermodynamics

Physlib/Thermodynamics/Foundation/Entropy.lean

@@ -0,0 +1,151 @@
+/-
+Copyright (c) 2026 Nathaneal Sajan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaneal Sajan
+-/
+module
+
+public import Physlib.Thermodynamics.Foundation.Comparability
+
+/-!
+# Entropy representations
+
+## i. Overview
+
+The **Entropy Principle** asks for a single real-valued function `S` on all states of all systems
+that encodes the adiabatic-accessibility preorder `≺`: monotone (`X ≺ Y ⟺ S(X) ≤ S(Y)` on
+comparable states), additive under composition, and extensive under scaling.
+`EntropyRepresentation` bundles `S` together with exactly these three properties.
+Lieb-Yngvason build such an `S` explicitly as `S(X) = sup {t | R_t ≺ X}`, where
+`R_t = ((1-t)•X₀, t•X₁)` mixes two fixed reference states `X₀ ≺≺ X₁`; the accessibility axioms
+A1-A6 are what make that supremum well-defined, monotone, additive and extensive.
+
+The `Monotonicity` field is conditioned on `Comparable` and the equivalence
+`X ≺ Y ↔ S(X) ≤ S(Y)` is asserted only when `X` and `Y` are comparable. This follows
+Lieb-Yngvason, who state the equivalence only in that case, and it keeps to the design
+choice that comparison hypotheses are carried as explicit assumptions rather than built
+into the accessibility relation `≺`
+
+## ii. Key results
+
+- `AllStates` — the sigma-typed domain: every state packaged with its system.
+- `EntropyRepresentation` — entropy `S` bundled with monotonicity, additivity, extensivity.
+- `entropy_equiv_iff_eq` / `entropy_strict_iff_lt` — the equivalence and strict forms of
+  monotonicity.
+- `AffineUniqueness` — the statement (not a field, not proved here) that any two
+  representations agree up to a positive affine recalibration `S ↦ aS + b`.
+
+## iii. Table of contents
+
+- A. The domain of entropy
+- B. Entropy as an order representation
+- C. Consequences of the entropy principle
+- D. Essential uniqueness
+
+## iv. References
+
+- E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of
+  Thermodynamics*, Physics Reports **310** (1999)
+- E.H. Lieb and J. Yngvason, *The Mathematical Structure of the Second Law of
+  Thermodynamics*, Current Developments in Mathematics **2001** (2002)
+-/
+
+@[expose] public section
+
+namespace Thermodynamics
+
+universe u
+
+/-! ## A. The domain of entropy
+
+An entropy function must range over *all* states of *all* systems at once, compound
+systems included, so that additivity `S(X, Y) = S(X) + S(Y)` can even be stated across
+systems. We package a state together with the system it belongs to as a sigma type. -/
+
+/-- The type of all states of all systems in a thermodynamic core: a state packaged with
+the system it belongs to. This sigma type is the domain of an entropy representation. -/
+def AllStates (System : Type u) [T : ThermoSystemCore System] :=
+  Σ Γ : System, T.State Γ
+
+/-! ## B. Entropy as an order representation
+
+This section turns the Entropy Principle into the structure `EntropyRepresentation`: an `S`
+on `AllStates` bundling monotonicity, additivity, and extensivity.
+
+Extensivity can almost be derived from additivity, which makes the small gap between them
+one of the more interesting features of the entropy principle. For rational scaling factors
+there is no gap at all: given the recombination axiom A5, which lets equal samples of a
+state be combined into a scaled copy, additivity already forces `S(t • X) = t · S(X)`
+whenever `t` is rational. Extensivity earns its independence at the irrational factors. By
+the axiom of choice, through a Hamel-basis construction, any `S` satisfying monotonicity and
+additivity can be altered so that extensivity fails at some irrational `t`. So extensivity
+is never quite redundant, even when A5 holds, and here, where the structure is only a bare
+`ThermoSystemCore` without A5, it must be assumed outright for every factor. -/
+
+/-- An entropy representation of a thermodynamic core: a real-valued `S` on `AllStates` with
+monotonicity, additivity, and extensivity as its fields. -/
+structure EntropyRepresentation (System : Type u) [T : ThermoSystemCore System] where
+  /-- The entropy of an arbitrary state, packaged with its system. -/
+  S : AllStates System → ℝ
+  /-- Monotonicity: for comparable states, accessibility is equivalent to entropy
+  increase, `X ≺ Y ↔ S(X) ≤ S(Y)`. Conditioned on `Comparable` because the equivalence is
+  claimed only for comparable states. -/
+  Monotonicity {Γ₁ Γ₂ : System} (X : T.State Γ₁) (Y : T.State Γ₂) :
+    Comparable (T := T) X Y → (T.le X Y ↔ S ⟨Γ₁, X⟩ ≤ S ⟨Γ₂, Y⟩)
+  /-- Additivity: `S(X, Y) = S(X) + S(Y)` across a composition. -/
+  Additivity {Γ₁ Γ₂ : System} (X : T.State Γ₁) (Y : T.State Γ₂) :
+    S ⟨T.comp Γ₁ Γ₂, T.state_of_comp_equiv.symm (X, Y)⟩ =
+      S ⟨Γ₁, X⟩ + S ⟨Γ₂, Y⟩
+  /-- Extensivity: `S(t • X) = t · S(X)` for `t > 0`. -/
+  Extensivity {Γ : System} (X : T.State Γ) {t : ℝ} (ht : 0 < t) :
+    S ⟨T.scale t Γ, (T.state_of_scale_equiv (ne_of_gt ht)).symm X⟩ =
+      t * S ⟨Γ, X⟩
+
+/-! ## C. Consequences of the entropy principle
+
+Monotonicity has two immediate corollaries. On comparable states, adiabatic equivalence is
+equality of entropy and strict accessibility is strict entropy increase. These are the
+"entropy increases in an irreversible process" readings of `S`. -/
+
+section Consequences
+
+variable {System : Type u} [T : ThermoSystemCore System]
+
+local infix:50 " ≺ " => T.le
+local notation:50 X " ≈ " Y => X ≺ Y ∧ Y ≺ X
+local infix:50 " ≺≺ " => StrictlyPrecedes (T := T)
+
+/-- For comparable states, adiabatic equivalence is equality of entropy `X ≈ Y ↔ S(X) = S(Y)`. -/
+lemma entropy_equiv_iff_eq {E : EntropyRepresentation System} {Γ₁ Γ₂ : System}
+    (X : T.State Γ₁) (Y : T.State Γ₂) (h_comp : Comparable (T := T) X Y) :
+    (X ≈ Y) ↔ E.S ⟨Γ₁, X⟩ = E.S ⟨Γ₂, Y⟩ := by
+  rw [E.Monotonicity X Y h_comp]
+  have h_comp_symm : Comparable (T := T) Y X := Comparable.symm h_comp
+  rw [E.Monotonicity Y X h_comp_symm]
+  exact le_antisymm_iff.symm
+
+/-- For comparable states, strict accessibility is strict entropy increase:
+`X ≺≺ Y ↔ S(X) < S(Y)`. -/
+lemma entropy_strict_iff_lt {E : EntropyRepresentation System} {Γ₁ Γ₂ : System}
+    (X : T.State Γ₁) (Y : T.State Γ₂) (h_comp : Comparable (T := T) X Y) :
+    X ≺≺ Y ↔ E.S ⟨Γ₁, X⟩ < E.S ⟨Γ₂, Y⟩ := by
+  rw [StrictlyPrecedes]
+  rw [E.Monotonicity X Y h_comp]
+  have h_comp_symm : Comparable (T := T) Y X := Comparable.symm h_comp
+  rw [E.Monotonicity Y X h_comp_symm]
+  exact Iff.symm lt_iff_le_not_ge
+
+end Consequences
+
+/-! ## D. Essential uniqueness
+
+Lieb-Yngvason's entropy is unique only up to a positive affine change of scale
+`S ↦ aS + b`. We record that statement as a `Prop`. -/
+
+/-- Essential affine uniqueness of entropy representations: any two
+representations agree up to a positive affine recalibration `S ↦ a * S + b` (`a > 0`). -/
+def AffineUniqueness (System : Type u) [T : ThermoSystemCore System] : Prop :=
+  ∀ E E' : EntropyRepresentation System,
+    ∃ a b : ℝ, 0 < a ∧ ∀ x, E'.S x = a * E.S x + b
+
+end Thermodynamics