From 0f7d3ac3994b020c4285e5ed5ec1b7f51a1f9f93 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 11:56:47 +0400 Subject: [PATCH 1/8] feat(Thermodynamics): add accessibility and entropy interfaces 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. --- .../Foundation/Accessibility.lean | 361 ++++++++++++++++++ .../Thermodynamics/Foundation/Entropy.lean | 144 +++++++ 2 files changed, 505 insertions(+) create mode 100644 Physlib/Thermodynamics/Foundation/Accessibility.lean create mode 100644 Physlib/Thermodynamics/Foundation/Entropy.lean diff --git a/Physlib/Thermodynamics/Foundation/Accessibility.lean b/Physlib/Thermodynamics/Foundation/Accessibility.lean new file mode 100644 index 000000000..01cb4fabf --- /dev/null +++ b/Physlib/Thermodynamics/Foundation/Accessibility.lean @@ -0,0 +1,361 @@ +/- +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.Order.Filter.AtTopBot.Defs +public import Mathlib.Topology.Instances.Real.Lemmas + +/-! +# Adiabatic accessibility + +## i. Overview + +This module defines a thermodynamics interface for the abstract Lieb-Yngvason accessibility +foundation. + +The primitive is a preorder `≺` 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 have moved in a +gravitational field (Lieb-Yngvason 1999, §II.A). From `≺` one reads off adiabatic +equivalence `X ≈ Y` (`X ≺ Y` and `Y ≺ X`) and strict accessibility `X ≺≺ Y` (`X ≺ Y` +but not `Y ≺ X`), the latter being the irreversible processes. + +The eventual goal would be 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`). + +The file is split into two classes: + +* `ThermoSystemCore` contains the operational vocabulary: systems, their state + spaces, composition, scaling, the zero system, and the primitive adiabatic-accessibility + relation `≺`. +* `ThermoWorld` extends the core with the algebraic identities on systems, the + accessibility axioms A1-A6, and the cast-coherence axioms needed because Lean + distinguishes propositionally-equal state spaces that Lieb-Yngvason identify. + +## ii. Key results + +- `ThermoSystemCore` / `ThermoWorld` — the two-layer abstract interface. +- `Comparable`, `ComparisonHypothesis`, `GlobalComparisonHypothesis` — the comparability + vocabulary. The comparison hypothesis is stated as a *hypothesis*, carried separately, + never baked into the axioms (see §C). +- `StrictlyPrecedes` (`≺≺`) — irreversible accessibility. +- `thermo_le_refl`, `thermo_le_trans`, `thermo_equiv_refl`, `thermo_equiv_symm`, + `calcTransThermoLe` — the preorder API exposing A1/A2 for calculation. + +## iii. Table of contents + +- A. Operational core (`ThermoSystemCore`) +- B. Lieb-Yngvason worlds (`ThermoWorld`) + - B.1. System algebra + - B.2. Accessibility axioms A1-A6 + - B.3. Coherence of casts +- C. Comparability +- D. Core API +- E. World API + +## iv. References + +- E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of + Thermodynamics*, Physics Reports **310** (1999) 1-96. Adiabatic accessibility and its + operational definition, §II.A; the entropy principle, §II.B; the order axioms A1-A6 and + the comparison hypothesis CH, §II.C. +- E.H. Lieb and J. Yngvason, *The Mathematical Structure of the Second Law of + Thermodynamics*, Current Developments in Mathematics **2001** (2002) 89-129; + arXiv:math-ph/0204007. A streamlined re-presentation of the same axiomatics. +-/ + +@[expose] public section + +namespace Thermodynamics + +universe u v + +/-! ## A. Operational core + +We first fix the operational vocabulary of thermodynamics with no axioms attached. +A `ThermoSystemCore` records, for each *system*, its space of equilibrium *states*, +together with the two ways of building new systems — composition `⊗` (placing two systems +side by side) and scaling `•` (taking a `t`-sized copy) — the zero system, and the +primitive adiabatic-accessibility relation `≺`. Separating this core from the axioms lets +later layers depend only on the vocabulary they actually use. -/ + +/-- The operational core of a thermodynamic accessibility structure. + +A `ThermoSystemCore` records the state space indexed by each system, system composition, +system scaling, the zero system, and the primitive adiabatic-accessibility relation.-/ +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`: `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. States may belong to different systems. -/ + 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. Lieb-Yngvason worlds + +A `ThermoWorld` extends the core with the assumptions Lieb-Yngvason place on `≺`. These +fall into three groups: the algebraic identities making composition an associative, +commutative operation on which scaling acts compatibly; the six accessibility +axioms A1-A6; and coherence axioms relating states across *equal* systems. The last +group has no Lieb-Yngvason axiom number: the paper treats identities like +`(Γ₁ ⊗ Γ₂) = (Γ₂ ⊗ Γ₁)` as strict equalities of state spaces and uses them silently, but in +Lean equal systems yield state spaces that are only propositionally equal, so each identity +is paired with a statement that transporting a state along it lands on an +adiabatically-equivalent state. + +The fields are assumptions of the abstract world. -/ + +/-- +This extends `ThermoSystemCore` with the structural equalities, accessibility axioms A1-A6, +and coherence axioms needed to reason about casts induced by equalities of systems.-/ +class ThermoWorld (System : Type u) extends ThermoSystemCore System where + /-- Scaling by zero gives the zero system. -/ + scale_zero_is_ZSystem (Γ : System) : scale 0 Γ = ZSystem + + /-- Composition of systems is associative, up to equality of systems. -/ + comp_assoc (Γ₁ Γ₂ Γ₃ : System) : comp (comp Γ₁ Γ₂) Γ₃ = comp Γ₁ (comp Γ₂ Γ₃) + /-- Composition of systems is commutative, up to equality of systems. -/ + comp_comm (Γ₁ Γ₂ : System) : comp Γ₁ Γ₂ = comp Γ₂ Γ₁ + /-- Scaling distributes over composition of systems. -/ + scale_distrib_comp (t : ℝ) (Γ₁ Γ₂ : System) : + scale t (comp Γ₁ Γ₂) = comp (scale t Γ₁) (scale t Γ₂) + /-- Successive scalings multiply their scale factors. -/ + smul_smul (t s : ℝ) (Γ : System) : scale (t * s) Γ = scale t (scale s Γ) + /-- Scaling by one leaves the system unchanged. -/ + one_smul (Γ : System) : scale 1 Γ = Γ + + /-- A1, reflexivity: every state is accessible from itself, `X ≺ X`. -/ + A1 {Γ : System} (X : State Γ) : le X X + /-- A2, transitivity: `X ≺ Y` and `Y ≺ Z` give `X ≺ Z`. -/ + A2 {Γ₁ Γ₂ Γ₃ : System} {X : State Γ₁} {Y : State Γ₂} {Z : State Γ₃} : + le X Y → le Y Z → le X Z + /-- A3, consistency: accessibility is preserved by composition — + `X₁ ≺ Y₁` and `X₂ ≺ Y₂` give `(X₁, X₂) ≺ (Y₁, Y₂)`. -/ + A3 {Γ₁ Γ₂ Γ₃ Γ₄ : System} + {X₁ : State Γ₁} {X₂ : State Γ₂} {Y₁ : State Γ₃} {Y₂ : State Γ₄} : + le X₁ Y₁ → le X₂ Y₂ → + le (state_of_comp_equiv.symm (X₁, X₂)) (state_of_comp_equiv.symm (Y₁, Y₂)) + /-- A4, scaling invariance: if `X ≺ Y` then `t • X ≺ t • Y` for every `t > 0`. -/ + A4 {Γ₁ Γ₂ : System} {X : State Γ₁} {Y : State Γ₂} {t : ℝ} (ht : 0 < t) : + le X Y → le ((state_of_scale_equiv ht.ne.symm).symm X) + ((state_of_scale_equiv ht.ne.symm).symm Y) + /-- A5, splitting and recombination: for `0 < t < 1` a state is adiabatically equivalent + to its split into a `t`-copy and a `(1−t)`-copy, `X ≈ (t • X, (1−t) • X)`. -/ + A5 {Γ : System} (X : State Γ) {t : ℝ} (ht : 0 < t ∧ t < 1) : + le X + (state_of_comp_equiv.symm + (((state_of_scale_equiv ht.1.ne').symm X), + ((state_of_scale_equiv (t := 1 - t) (by + have hpos : 0 < 1 - t := sub_pos.mpr ht.2 + exact hpos.ne')).symm X))) ∧ + le (state_of_comp_equiv.symm + (((state_of_scale_equiv ht.1.ne').symm X), + ((state_of_scale_equiv (t := 1 - t) (by + have hpos : 0 < 1 - t := sub_pos.mpr ht.2 + exact hpos.ne')).symm X))) X + /-- A6, stability: accessibility cannot be created by an infinitesimal perturbation. + + If `(X, epsilon_n Z₀)` is adiabatically accessible to `(Y, epsilon_n Z₁)` for some states + `Z₀, Z₁` along a positive sequence `epsilon_n` tending to zero, then `X` is adiabatically + accessible to `Y`. Lieb-Yngvason: one cannot enlarge the set of accessible states "with an + infinitesimal grain of dust." -/ + A6_seq {ΓX ΓY ΓZ₀ ΓZ₁ : System} (X : State ΓX) (Y : State ΓY) + (Z₀ : State ΓZ₀) (Z₁ : State ΓZ₁) : + (∃ (ε_seq : ℕ → ℝ) (hpos : ∀ n, 0 < ε_seq n), + Filter.Tendsto ε_seq Filter.atTop (nhds 0) ∧ + (∀ n, + le + (state_of_comp_equiv.symm + (X, (state_of_scale_equiv (ne_of_gt (hpos n))).symm Z₀)) + (state_of_comp_equiv.symm + (Y, (state_of_scale_equiv (ne_of_gt (hpos n))).symm Z₁)))) → le X Y + + /-- Coherence of casting along an equality of systems: transporting a state along the + equality yields an adiabatically-equivalent state. This and the coherence fields below are + not Lieb-Yngvason axioms — they are needed only because Lean does not identify + propositionally-equal state spaces. -/ + state_equiv_coherence {Γ₁ Γ₂ : System} (h_sys : Γ₁ = Γ₂) (X : State Γ₁) : + le X (Equiv.cast (congrArg State h_sys) X) ∧ + le (Equiv.cast (congrArg State h_sys) X) X + /-- Coherence of composing with the zero system. -/ + comp_ZSystem_is_identity (Γ : System) (X : State Γ) : + le (state_of_comp_equiv.symm (X, State_ZSystem_is_Unit.default)) X ∧ + le X (state_of_comp_equiv.symm (X, State_ZSystem_is_Unit.default)) + /-- Coherence of successive scaling: `t` applied to `s` applied to `X` agrees with `(t * s)` + applied to `X`, up to adiabatic equivalence after the system cast. -/ + scale_coherence {t s : ℝ} (ht : t ≠ 0) (hs : s ≠ 0) {Γ : System} (X : State Γ) : + let X_s := (state_of_scale_equiv hs).symm X + let X_ts := (state_of_scale_equiv ht).symm X_s + let X_mul := (state_of_scale_equiv (mul_ne_zero ht hs)).symm X + let h_eq := smul_smul t s Γ + le (Equiv.cast (congrArg State h_eq) X_mul) X_ts ∧ + le X_ts (Equiv.cast (congrArg State h_eq) X_mul) + /-- Coherence of equal scaling factors. -/ + scale_eq_coherence {t₁ t₂ : ℝ} (h_eq : t₁ = t₂) (ht₁ : t₁ ≠ 0) {Γ : System} + (X : State Γ) : + let ht₂ : t₂ ≠ 0 := h_eq ▸ ht₁ + let X₁ := (state_of_scale_equiv ht₁).symm X + let X₂ := (state_of_scale_equiv ht₂).symm X + let h_sys_eq := congrArg (fun r => scale r Γ) h_eq + le (Equiv.cast (congrArg State h_sys_eq) X₁) X₂ ∧ + le X₂ (Equiv.cast (congrArg State h_sys_eq) X₁) + /-- Coherence of scaling by one. -/ + one_smul_coherence {Γ : System} (X : State Γ) : + let X_1 := (state_of_scale_equiv (show (1 : ℝ) ≠ 0 from one_ne_zero)).symm X + let h_eq := one_smul Γ + le (Equiv.cast (congrArg State h_eq) X_1) X ∧ + le X (Equiv.cast (congrArg State h_eq) X_1) + /-- Coherence of scaling a composed state. -/ + scale_comp_coherence {t : ℝ} (ht : t ≠ 0) {Γ₁ Γ₂ : System} + (X : State Γ₁) (Y : State Γ₂) : + let XY := state_of_comp_equiv.symm (X, Y) + let tXY := (state_of_scale_equiv ht).symm XY + let tX := (state_of_scale_equiv ht).symm X + let tY := (state_of_scale_equiv ht).symm Y + let tXtY := state_of_comp_equiv.symm (tX, tY) + let h_eq := scale_distrib_comp t Γ₁ Γ₂ + le (Equiv.cast (congrArg State h_eq) tXY) tXtY ∧ + le tXtY (Equiv.cast (congrArg State h_eq) tXY) + /-- Coherence of commutativity of composition. -/ + comp_comm_coherence {Γ₁ Γ₂ : System} (X : State Γ₁) (Y : State Γ₂) : + let XY := state_of_comp_equiv.symm (X, Y) + let YX := state_of_comp_equiv.symm (Y, X) + let h_eq := comp_comm Γ₁ Γ₂ + le (Equiv.cast (congrArg State h_eq.symm) YX) XY ∧ + le XY (Equiv.cast (congrArg State h_eq.symm) YX) + /-- Coherence of associativity of composition. -/ + comp_assoc_coherence {Γ₁ Γ₂ Γ₃ : System} (X : State Γ₁) (Y : State Γ₂) + (Z : State Γ₃) : + let XY := state_of_comp_equiv.symm (X, Y) + let XYZ_L := state_of_comp_equiv.symm (XY, Z) + let YZ := state_of_comp_equiv.symm (Y, Z) + let XYZ_R := state_of_comp_equiv.symm (X, YZ) + let h_eq := comp_assoc Γ₁ Γ₂ Γ₃ + le (Equiv.cast (congrArg State h_eq) XYZ_L) XYZ_R ∧ + le XYZ_R (Equiv.cast (congrArg State h_eq) XYZ_L) + +/-! ## C. Comparability + +Two states are *comparable* when at least one is accessible from the other; they are +*adiabatically equivalent* when each is. Lieb-Yngvason's **comparison hypothesis** (CH) +asserts that any two states of one state space are comparable. Crucially CH is a +*hypothesis*, not one of A1-A6: the paper's programme 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 rather than folding it into accessibility. +`GlobalComparisonHypothesis` is the compound-system strengthening. -/ + +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 + +/-- Two states are comparable if either is adiabatically accessible from the other, +`X ≺ Y ∨ Y ≺ X` (Lieb-Yngvason 1999, §II.A). -/ +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. +Stated as a hypothesis, not an axiom — Lieb-Yngvason derive it for simple systems rather than +assuming it (§II.C, §III-IV). -/ +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. This is named at A0 because later entropy constructions carry it as a separate +hypothesis rather than baking it into accessibility. -/ +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 + +/-! ## D. Core API + +Small consequences that need only `ThermoSystemCore`. -/ + +/-- 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 + +/-! ## E. World API + +Notation (`≺`, `≈`, `⊗`, `•`, `≺≺`) and the preorder lemmas exposing axioms A1 and A2 as +reflexivity and transitivity, plus a `Trans` instance so accessibility chains compose in +`calc` blocks. -/ + +section World + +variable {System : Type u} [TW : ThermoWorld System] + +local infix:50 " ≺ " => TW.le +local notation:50 X " ≈ " Y => X ≺ Y ∧ Y ≺ X +local infixr:70 " ⊗ " => TW.comp +local infixr:80 " • " => TW.scale +local infix:50 " ≺≺ " => StrictlyPrecedes (T := TW) + +/-- Reflexivity of adiabatic accessibility, exposed as a lemma from A1. -/ +lemma thermo_le_refl {Γ : System} (X : TW.State Γ) : X ≺ X := + TW.A1 X + +/-- Transitivity of adiabatic accessibility, exposed as a lemma from A2. -/ +lemma thermo_le_trans {Γ₁ Γ₂ Γ₃ : System} {X : TW.State Γ₁} {Y : TW.State Γ₂} + {Z : TW.State Γ₃} (hXY : X ≺ Y) (hYZ : Y ≺ Z) : X ≺ Z := + TW.A2 hXY hYZ + +/-- Adiabatic equivalence is reflexive. -/ +lemma thermo_equiv_refl {Γ : System} (X : TW.State Γ) : X ≈ X := + ⟨thermo_le_refl X, thermo_le_refl X⟩ + +/-- Adiabatic equivalence is symmetric. -/ +lemma thermo_equiv_symm {Γ₁ Γ₂ : System} {X : TW.State Γ₁} {Y : TW.State Γ₂} + (h : X ≈ Y) : Y ≈ X := + And.symm h + +/-- A `Trans` instance for calculations with adiabatic accessibility. -/ +instance calcTransThermoLe {Γ₁ Γ₂ Γ₃ : System} : + Trans (TW.le : TW.State Γ₁ → TW.State Γ₂ → Prop) + (TW.le : TW.State Γ₂ → TW.State Γ₃ → Prop) + (TW.le : TW.State Γ₁ → TW.State Γ₃ → Prop) where + trans := TW.A2 + +end World + +end Thermodynamics diff --git a/Physlib/Thermodynamics/Foundation/Entropy.lean b/Physlib/Thermodynamics/Foundation/Entropy.lean new file mode 100644 index 000000000..4cff8eb1a --- /dev/null +++ b/Physlib/Thermodynamics/Foundation/Entropy.lean @@ -0,0 +1,144 @@ +/- +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.Accessibility + +/-! +# 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 conditional on `Comparable`. This is faithful to +Lieb-Yngvason's eq. (2.3), which asserts the accessibility/entropy equivalence only for +comparable states, and to the design choice (see `Accessibility.lean`) that comparison +hypotheses are carried explicitly rather than baked into accessibility. + +## 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 (Lieb-Yngvason eq. 2.6). +- `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) 1-96. The entropy principle and its + properties (monotonicity, additivity, extensivity), §II.B, eqns (2.3)-(2.6); essential + uniqueness up to affine scale, §II.C; the canonical construction of `S`, §II.E. +-/ + +@[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, +letting `S` compare states across different systems. -/ +def AllStates (System : Type u) [T : ThermoSystemCore System] := + Σ Γ : System, T.State Γ + +/-! ## B. Entropy as an order representation + +An `EntropyRepresentation` is the Entropy Principle turned into a structure: a real-valued `S` +on `AllStates` that represents `≺` on comparable states (monotonicity), is additive under +composition, and is extensive under positive scaling.-/ + +/-- An abstract entropy representation of a thermodynamic core: the Lieb-Yngvason Entropy +Principle as a structure. A real-valued `S` on `AllStates` that represents adiabatic +accessibility on comparable states, is additive under composition, and is extensive under +positive scaling.-/ +structure EntropyRepresentation (System : Type u) [T : ThermoSystemCore System] where + /-- The entropy of an arbitrary state, packaged with its system. -/ + S : AllStates System → ℝ + /-- Monotonicity (Lieb-Yngvason eq. 2.3): 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 (Lieb-Yngvason eq. 2.4): `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 (Lieb-Yngvason eq. 2.5): `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 + +Immediate rephrasings of monotonicity : 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)`- + entropy strictly increases in an irreversible process. -/ +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 From 1e2b96ae935f23d0455c0ed02df36caea966e8de Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 11:57:49 +0400 Subject: [PATCH 2/8] feat(Thermodynamics): add smooth fundamental relations 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. --- .../FundamentalRelation/Basic.lean | 135 ++++++ .../FundamentalRelation/Euler.lean | 142 +++++++ .../FundamentalRelation/Intensive.lean | 394 ++++++++++++++++++ 3 files changed, 671 insertions(+) create mode 100644 Physlib/Thermodynamics/FundamentalRelation/Basic.lean create mode 100644 Physlib/Thermodynamics/FundamentalRelation/Euler.lean create mode 100644 Physlib/Thermodynamics/FundamentalRelation/Intensive.lean diff --git a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean new file mode 100644 index 000000000..ca904ea08 --- /dev/null +++ b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean @@ -0,0 +1,135 @@ +/- +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.Analysis.Calculus.ContDiff.Basic +public import Mathlib.Analysis.Calculus.Deriv.MeanValue + +/-! +# The fundamental relation of a simple thermodynamic system + +## i. Overview + +In the entropy representation, all thermodynamic information about a simple system is +contained in its **fundamental relation** `S = S(U, V, N)`, the entropy as a +function of the extensive parameters internal energy `U`, volume `V`, and particle number `N`. + +Design choices: +- **`S` is kept total** (`ℝ → ℝ → ℝ → ℝ`); positivity is carried by field hypotheses and by + `ExtensiveState`. +- **The domain of regularity is the positive orthant** (`posOrthant` / `ExtensiveState`); `S` is + not assumed regular where a coordinate vanishes. +- **`StrictMonoOn` in `U` is derived**, not a field: `dS_dU_pos` (pointwise `∂S/∂U > 0`) is the + primitive, and `strictMonoOn_U` follows from it. + +This file records the assumptions used by the current entropy-representation layer: +degree-one homogeneity (`homogeneous`), smoothness on the positive orthant (`smooth`), and +positive energy derivative (`dS_dU_pos`, equivalently `T > 0`). These are bundled in +`FundamentalRelation`. Stability, concavity, and third-law behavior are not fields of this +structure. + +## ii. Key results + +- `ExtensiveState` — a positive extensive state `(U, V, N)`, the physical coordinate domain. +- `posOrthant` — the open positive orthant of `ℝ × ℝ × ℝ` on which a relation is regular. +- `FundamentalRelation` — the smooth entropy surface `S(U, V, N)` with its three fields. +- `FundamentalRelation.strictMonoOn_U` — entropy is strictly increasing in `U` (derived from + `dS_dU_pos`). + +## iii. Table of contents + +- A. Extensive states and the coordinate domain +- B. The fundamental relation +- C. Derived monotonicity in energy + +## iv. References + +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley (1985). +-/ + +@[expose] public section + +namespace Thermodynamics + +open scoped ContDiff + +/-! ## A. Extensive states and the coordinate domain + +A `FundamentalRelation` is regular only on physically admissible states — those with strictly +positive `U`, `V`, `N`. We carry that positivity in two ways: `ExtensiveState` for the physical +states the later bridge charts, and `posOrthant` for the open set on which smoothness and the +energy derivative are asserted. Keeping positivity here, rather than in the type of `S`, lets the +calculus treat `S` as an ordinary total function. -/ + +/-- A positive **extensive state** `(U, V, N)` of a simple system: internal energy, +volume and particle number, all strictly positive. This is the physical domain over +which a `FundamentalRelation` is smooth, homogeneous, and monotone. -/ +structure ExtensiveState where + /-- Internal energy. -/ + U : ℝ + /-- Volume. -/ + V : ℝ + /-- Particle number. -/ + N : ℝ + /-- Positivity of the internal energy. -/ + hU : 0 < U + /-- Positivity of the volume. -/ + hV : 0 < V + /-- Positivity of the particle number. -/ + hN : 0 < N + +/-- The positive orthant of `ℝ × ℝ × ℝ` — the coordinate domain on which a +`FundamentalRelation` is regular. -/ +def posOrthant : Set (ℝ × ℝ × ℝ) := {p | 0 < p.1 ∧ 0 < p.2.1 ∧ 0 < p.2.2} + +/-! ## B. The fundamental relation + +The structure bundles the entropy surface `S` with Postulate III: it is C^∞ (`smooth`), +has positive energy derivative (`dS_dU_pos`, giving `T > 0`), and is homogeneous of degree one +(`homogeneous`, i.e. extensivity). Concavity/stability (Postulate II) is deferred. -/ + +/-- A **fundamental relation** in the entropy representation: a total entropy function +`S(U, V, N)` that is C^∞, has positive energy derivative, and is homogeneous of degree one on the +positive orthant. -/ +structure FundamentalRelation where + /-- The entropy as a total function of `(U, V, N)`. Positivity is imposed by the field + hypotheses below, not by the type of `S`. -/ + S : ℝ → ℝ → ℝ → ℝ + /-- Regularity: `S` is C^∞ on the positive orthant. -/ + smooth : ContDiffOn ℝ ∞ (fun p : ℝ × ℝ × ℝ => S p.1 p.2.1 p.2.2) posOrthant + /-- Postulate III (`T > 0`): for positive states, `∂S/∂U > 0`, i.e. + `1 / T > 0` pointwise. This yields positive temperature without invoking concavity. -/ + dS_dU_pos : ∀ U V N, 0 < U → 0 < V → 0 < N → 0 < deriv (fun u => S u V N) U + /-- Extensivity: `S` is homogeneous of degree one on the positive orthant, + `S(lU, lV, lN) = l · S(U, V, N)` for `l > 0` (Callen's extensivity of the entropy). -/ + homogeneous : ∀ ⦃l : ℝ⦄, 0 < l → ∀ U V N, 0 < U → 0 < V → 0 < N → + S (l * U) (l * V) (l * N) = l * S U V N + +/-! ## C. Derived monotonicity in energy + +Strict monotonicity of entropy in `U` is derived from the pointwise `dS_dU_pos` via +`strictMonoOn_of_deriv_pos`, and `T > 0` is a consequence. -/ + +/-- Derived: for fixed positive `V, N`, entropy is strictly increasing in the energy on +`Ioi 0`. Obtained from `dS_dU_pos` via `strictMonoOn_of_deriv_pos`. -/ +lemma FundamentalRelation.strictMonoOn_U (Φ : FundamentalRelation) (V N : ℝ) + (hV : 0 < V) (hN : 0 < N) : + StrictMonoOn (fun U => Φ.S U V N) (Set.Ioi 0) := by + apply strictMonoOn_of_deriv_pos (convex_Ioi 0) + · change ContinuousOn ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun U : ℝ => (U, (V, N))) (Set.Ioi 0) + exact Φ.smooth.continuousOn.comp + (by + show ContinuousOn (fun U : ℝ => (U, (V, N))) (Set.Ioi 0) + fun_prop) + (by + intro U hU + exact ⟨hU, hV, hN⟩) + · rw [interior_Ioi] + intro U hU + exact Φ.dS_dU_pos U V N hU hV hN + +end Thermodynamics diff --git a/Physlib/Thermodynamics/FundamentalRelation/Euler.lean b/Physlib/Thermodynamics/FundamentalRelation/Euler.lean new file mode 100644 index 000000000..8e808d975 --- /dev/null +++ b/Physlib/Thermodynamics/FundamentalRelation/Euler.lean @@ -0,0 +1,142 @@ +/- +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.Analysis.Calculus.Deriv.Comp +public import Mathlib.Analysis.Calculus.Deriv.Mul +public import Mathlib.Analysis.Calculus.Deriv.Prod +public import Physlib.Thermodynamics.FundamentalRelation.Intensive + +/-! +# Euler relation for fundamental thermodynamic relations + +## i. Overview + +For a simple system in the entropy representation, extensivity says that the fundamental +relation is homogeneous of degree one: + +`S(lU, lV, lN) = l * S(U, V, N)` for `l > 0`. + +Differentiating this scaling identity at `l = 1` gives Euler's homogeneous-function identity + +`U * ∂S/∂U + V * ∂S/∂V + N * ∂S/∂N = S`. + +This file proves that identity for any `FundamentalRelation`. The proof differentiates the +same scaling curve in two ways: first by the chain rule and the total-derivative formula +from `Intensive.lean`, and second by the homogeneity field of `FundamentalRelation`. + +The final theorem rewrites the homogeneous-function identity using the intensive parameters +defined from the entropy partials: + +`U = T * S - P * V + μ * N`. + +## ii. Key results + +- `FundamentalRelation.euler` - Euler's homogeneous-function identity for entropy. +- `FundamentalRelation.euler_relation` - the thermodynamic Euler relation + `U = T * S - P * V + μ * N`. + +## iii. Table of contents + +- A. Differentiating the scaling identity +- B. Euler identities + +## iv. References + +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley + (1985). +-/ + +@[expose] public section + +namespace Thermodynamics + +open scoped ContDiff + +noncomputable section + +/-! ## A. Differentiating the scaling identity + +The proof of Euler's identity compares two derivatives of the same one-variable curve +`l ↦ S(lU, lV, lN)` at `l = 1`. The left calculation uses the chain rule together with the +total derivative formula from `Intensive.lean`; the right calculation uses the degree-one +homogeneity assumption directly. -/ + +/-- The derivative of the scaling curve computed by the chain rule. + +For `l ↦ S(lU, lV, lN)`, differentiating through the coordinate map +`l ↦ (lU, lV, lN)` gives + +`U * ∂S/∂U + V * ∂S/∂V + N * ∂S/∂N` + +at `l = 1`. -/ +private lemma hasDerivAt_scaling_left (Φ : FundamentalRelation) (e : ExtensiveState) : + HasDerivAt (fun l => Φ.S (l * e.U) (l * e.V) (l * e.N)) + (e.U * Φ.dS_dU e + e.V * Φ.dS_dV e + e.N * Φ.dS_dN e) 1 := by + set D := fderiv ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + (e.U, e.V, e.N) with hD + have hdiag : HasDerivAt (fun l : ℝ => (l * e.U, l * e.V, l * e.N)) + (e.U, e.V, e.N) 1 := + (hasDerivAt_mul_const e.U).prodMk + ((hasDerivAt_mul_const e.V).prodMk (hasDerivAt_mul_const e.N)) + have hfderiv1 : HasFDerivAt (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) D + ((fun l : ℝ => (l * e.U, l * e.V, l * e.N)) 1) := by + simpa [one_mul] using Φ.hasFDerivAt_joint e + have hLHS : HasDerivAt (fun l => Φ.S (l * e.U) (l * e.V) (l * e.N)) + (D (e.U, e.V, e.N)) 1 := by + change HasDerivAt ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun l : ℝ => (l * e.U, (l * e.V, l * e.N))) (D (e.U, e.V, e.N)) 1 + exact hfderiv1.comp_hasDerivAt (1 : ℝ) hdiag + rwa [Φ.fderiv_S_apply e e.U e.V e.N] at hLHS + +/-- The derivative of the scaling curve computed from extensivity. + +Near `l = 1`, positivity of `l` lets the homogeneity field rewrite +`S(lU, lV, lN)` as `l * S(U, V, N)`, whose derivative at `1` is `S(U,V,N)`. -/ +private lemma hasDerivAt_scaling_right (Φ : FundamentalRelation) (e : ExtensiveState) : + HasDerivAt (fun l => Φ.S (l * e.U) (l * e.V) (l * e.N)) (Φ.S e.U e.V e.N) 1 := by + have heq : (fun l => Φ.S (l * e.U) (l * e.V) (l * e.N)) + =ᶠ[nhds (1 : ℝ)] (fun l => l * Φ.S e.U e.V e.N) := by + filter_upwards [isOpen_Ioi.mem_nhds (show (1 : ℝ) ∈ Set.Ioi 0 by norm_num)] with l hl + exact Φ.homogeneous hl e.U e.V e.N e.hU e.hV e.hN + exact (hasDerivAt_mul_const (Φ.S e.U e.V e.N)).congr_of_eventuallyEq heq + +/-! ## B. Euler identities + +Equating the two derivatives of the scaling curve gives Euler's homogeneous-function identity +for entropy. Substituting the definitions of `temperature`, `pressure`, and +`chemicalPotential` then gives the usual thermodynamic Euler relation. -/ + +/-- Euler's homogeneous-function identity for entropy: + +`U * ∂S/∂U + V * ∂S/∂V + N * ∂S/∂N = S`. + +It follows by differentiating the degree-one scaling law for `S` at scale `l = 1`. -/ +lemma FundamentalRelation.euler (Φ : FundamentalRelation) (e : ExtensiveState) : + e.U * Φ.dS_dU e + e.V * Φ.dS_dV e + e.N * Φ.dS_dN e = Φ.S e.U e.V e.N := + (hasDerivAt_scaling_left Φ e).unique (hasDerivAt_scaling_right Φ e) + +/-- The thermodynamic Euler relation in entropy-representation variables: + +`U = T * S - P * V + μ * N`. + +This is `FundamentalRelation.euler` rewritten using `T = (∂S/∂U)⁻¹`, +`P = T * ∂S/∂V`, and `μ = -T * ∂S/∂N`. -/ +lemma FundamentalRelation.euler_relation (Φ : FundamentalRelation) (e : ExtensiveState) : + e.U = Φ.temperature e * Φ.S e.U e.V e.N + - Φ.pressure e * e.V + Φ.chemicalPotential e * e.N := by + have hne : Φ.dS_dU e ≠ 0 := + ne_of_gt (by + simpa [FundamentalRelation.dS_dU] using Φ.dS_dU_pos e.U e.V e.N e.hU e.hV e.hN) + have he := Φ.euler e + simp only [FundamentalRelation.temperature, FundamentalRelation.pressure, + FundamentalRelation.chemicalPotential] + field_simp + linear_combination he + +end + +end Thermodynamics diff --git a/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean b/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean new file mode 100644 index 000000000..15c0bf249 --- /dev/null +++ b/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean @@ -0,0 +1,394 @@ +/- +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.Analysis.Calculus.Deriv.Comp +public import Mathlib.Analysis.Calculus.Deriv.Prod +public import Mathlib.Analysis.Calculus.MeanValue +public import Physlib.Thermodynamics.FundamentalRelation.Basic + +/-! +# Intensive parameters from a fundamental relation + +## i. Overview + +In the entropy representation, a simple system is described by a fundamental relation +`S = S(U, V, N)`, where `U` is internal energy, `V` is volume, and `N` is particle number. +The intensive parameters are obtained from the entropy differential + +`dS = (1 / T) dU + (P / T) dV - (μ / T) dN`. + +For a `FundamentalRelation Φ`, this file names the three coordinate derivatives +`∂S/∂U`, `∂S/∂V`, and `∂S/∂N`, defines the corresponding temperature, pressure, and chemical +potential, and proves `T > 0` from the assumed positivity of `∂S/∂U`. + +The differentiability lemmas connect the joint smoothness hypothesis on `S(U, V, N)` to the +one-coordinate derivative statements used by these definitions. The total derivative lemma +then identifies the Fréchet derivative of `S` with the expected linear expression in the +three entropy partials. + +The final theorem is a determination result for fundamental relations. If two fundamental +relations have the same `U` and `V` entropy partials and agree at one positive reference +state, then their residual vanishes everywhere on the positive orthant. Thus the two entropy +functions agree exactly on positive extensive states. The theorem is useful when a later +model identifies the equations of state first and then needs equality of the whole +fundamental relation. + +## ii. Key results + +- `FundamentalRelation.dS_dU`, `dS_dV`, `dS_dN` — entropy partial derivatives at a positive + extensive state. +- `FundamentalRelation.temperature`, `pressure`, `chemicalPotential` — intensive parameters + in the entropy representation. +- `FundamentalRelation.temperature_pos` — positivity of temperature from + `FundamentalRelation.dS_dU_pos`. +- `FundamentalRelation.fderiv_S_apply` — the total derivative of `S` as + `a * ∂S/∂U + b * ∂S/∂V + c * ∂S/∂N`. +- `FundamentalRelation.eq_of_dS_dU_dS_dV_eq_of_eq_at` — exact equality from entropy partials + and one reference value. + +## iii. Table of contents + +- A. Entropy partial derivatives +- B. Intensive parameters +- C. Coordinate derivatives and the total differential +- D. Uniqueness from entropy partials + +## iv. References + +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley + (1985). +-/ + +@[expose] public section + +namespace Thermodynamics + +open scoped ContDiff + +noncomputable section + +/-! ## A. Entropy partial derivatives + +The coordinate partials of the fundamental relation are defined by fixing two extensive +coordinates and differentiating with respect to the third. These are ordinary one-variable +`deriv`s evaluated at a positive `ExtensiveState`. -/ + +/-- 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) : ℝ := + deriv (fun u => Φ.S u e.V e.N) e.U + +/-- The volume partial derivative `∂S/∂V` at a positive extensive state. + +In the entropy differential, this is the coefficient `P / T` of `dV`. -/ +def FundamentalRelation.dS_dV (Φ : FundamentalRelation) (e : ExtensiveState) : ℝ := + deriv (fun v => Φ.S e.U v e.N) e.V + +/-- The particle-number partial derivative `∂S/∂N` at a positive extensive state. + +In the entropy differential, this is the coefficient `-μ / T` of `dN`. -/ +def FundamentalRelation.dS_dN (Φ : FundamentalRelation) (e : ExtensiveState) : ℝ := + deriv (fun n => Φ.S e.U e.V n) e.N + +/-! ## B. Intensive parameters + +The intensive parameters are recovered from the entropy partials by solving + +`∂S/∂U = 1 / T`, `∂S/∂V = P / T`, and `∂S/∂N = -μ / T`. + +The definitions here are real-valued coordinate functions on positive extensive states; no +particular equation of state is assumed. -/ + +/-- Temperature as the reciprocal of the energy derivative of entropy: +`T = (∂S/∂U)⁻¹`. -/ +def FundamentalRelation.temperature (Φ : FundamentalRelation) (e : ExtensiveState) : ℝ := + (Φ.dS_dU e)⁻¹ + +/-- Pressure from the entropy representation: `P = T * ∂S/∂V`. -/ +def FundamentalRelation.pressure (Φ : FundamentalRelation) (e : ExtensiveState) : ℝ := + Φ.temperature e * Φ.dS_dV e + +/-- Chemical potential from the entropy representation: `μ = -T * ∂S/∂N`. -/ +def FundamentalRelation.chemicalPotential (Φ : FundamentalRelation) (e : ExtensiveState) : ℝ := + -Φ.temperature e * Φ.dS_dN e + +/-- Temperature is positive on positive extensive states. + +This is the reciprocal form of Postulate III's monotonicity condition `∂S/∂U > 0`, recorded +here as `FundamentalRelation.dS_dU_pos`. -/ +lemma FundamentalRelation.temperature_pos (Φ : FundamentalRelation) (e : ExtensiveState) : + 0 < Φ.temperature e := by + have h := Φ.dS_dU_pos e.U e.V e.N e.hU e.hV e.hN + simpa [FundamentalRelation.temperature, FundamentalRelation.dS_dU] using inv_pos.mpr h + +/-! ## C. Coordinate derivatives and the total differential + +The smoothness field of `FundamentalRelation` is a joint regularity statement for +`S(U, V, N)` on the positive orthant. The lemmas in this section extract differentiability of +the one-coordinate maps and then compute the Fréchet derivative in terms of the three +coordinate partials. -/ + +/-- The positive orthant is open in `ℝ × ℝ × ℝ`. + +This lets the joint `ContDiffOn` hypothesis be used as differentiability at each positive +extensive state. -/ +lemma isOpen_posOrthant : IsOpen posOrthant := by + have hset : posOrthant = + {p : ℝ × ℝ × ℝ | 0 < p.1} ∩ {p | 0 < p.2.1} ∩ {p | 0 < p.2.2} := by + ext p + simp only [posOrthant, Set.mem_setOf_eq, Set.mem_inter_iff] + tauto + rw [hset] + exact ((isOpen_lt continuous_const continuous_fst).inter + (isOpen_lt continuous_const (continuous_fst.comp continuous_snd))).inter + (isOpen_lt continuous_const (continuous_snd.comp continuous_snd)) + +/-- The one-coordinate map `u ↦ S(u, V, N)` is differentiable at a positive extensive +state. -/ +lemma FundamentalRelation.differentiableAt_slice_U (Φ : FundamentalRelation) + (e : ExtensiveState) : + DifferentiableAt ℝ (fun u => Φ.S u e.V e.N) e.U := by + change DifferentiableAt ℝ ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun u : ℝ => (u, (e.V, e.N))) e.U + have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hjoint : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + (e.U, e.V, e.N) := + (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) + have hline : DifferentiableAt ℝ (fun u : ℝ => (u, e.V, e.N)) e.U := by + fun_prop + exact hjoint.comp e.U hline + +/-- The one-coordinate map `v ↦ S(U, v, N)` is differentiable at a positive extensive +state. -/ +lemma FundamentalRelation.differentiableAt_slice_V (Φ : FundamentalRelation) + (e : ExtensiveState) : + DifferentiableAt ℝ (fun v => Φ.S e.U v e.N) e.V := by + change DifferentiableAt ℝ ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun v : ℝ => (e.U, (v, e.N))) e.V + have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hjoint : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + (e.U, e.V, e.N) := + (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) + have hline : DifferentiableAt ℝ (fun v : ℝ => (e.U, v, e.N)) e.V := by + fun_prop + exact hjoint.comp e.V hline + +/-- The one-coordinate map `n ↦ S(U, V, n)` is differentiable at a positive extensive +state. -/ +lemma FundamentalRelation.differentiableAt_slice_N (Φ : FundamentalRelation) + (e : ExtensiveState) : + DifferentiableAt ℝ (fun n => Φ.S e.U e.V n) e.N := by + change DifferentiableAt ℝ ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun n : ℝ => (e.U, (e.V, n))) e.N + have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hjoint : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + (e.U, e.V, e.N) := + (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) + have hline : DifferentiableAt ℝ (fun n : ℝ => (e.U, e.V, n)) e.N := by + fun_prop + exact hjoint.comp e.N hline + +/-- The definition of `∂S/∂U` gives the corresponding `HasDerivAt` statement in the energy +coordinate. -/ +lemma FundamentalRelation.hasDerivAt_dS_dU (Φ : FundamentalRelation) (e : ExtensiveState) : + HasDerivAt (fun u => Φ.S u e.V e.N) (Φ.dS_dU e) e.U := + (Φ.differentiableAt_slice_U e).hasDerivAt + +/-- The definition of `∂S/∂V` gives the corresponding `HasDerivAt` statement in the volume +coordinate. -/ +lemma FundamentalRelation.hasDerivAt_dS_dV (Φ : FundamentalRelation) (e : ExtensiveState) : + HasDerivAt (fun v => Φ.S e.U v e.N) (Φ.dS_dV e) e.V := + (Φ.differentiableAt_slice_V e).hasDerivAt + +/-- The definition of `∂S/∂N` gives the corresponding `HasDerivAt` statement in the +particle-number coordinate. -/ +lemma FundamentalRelation.hasDerivAt_dS_dN (Φ : FundamentalRelation) (e : ExtensiveState) : + HasDerivAt (fun n => Φ.S e.U e.V n) (Φ.dS_dN e) e.N := + (Φ.differentiableAt_slice_N e).hasDerivAt + +/-- The joint entropy map is Fréchet-differentiable at a positive extensive state. -/ +lemma FundamentalRelation.hasFDerivAt_joint (Φ : FundamentalRelation) (e : ExtensiveState) : + HasFDerivAt (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + (fderiv ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N)) + (e.U, e.V, e.N) := by + have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hdiff : DifferentiableAt ℝ + (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N) := + (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) + exact hdiff.hasFDerivAt + +/-- The total derivative of `S` expressed through its coordinate partials: + +`D S(e) (a, b, c) = a * ∂S/∂U + b * ∂S/∂V + c * ∂S/∂N`. + +This is the formal version of `dS = (1/T)dU + (P/T)dV - (μ/T)dN`. -/ +lemma FundamentalRelation.fderiv_S_apply (Φ : FundamentalRelation) (e : ExtensiveState) + (a b c : ℝ) : + (fderiv ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N)) + (a, b, c) + = a * Φ.dS_dU e + b * Φ.dS_dV e + c * Φ.dS_dN e := by + set D := fderiv ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + (e.U, e.V, e.N) with hD + have hfderiv : HasFDerivAt (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) + D (e.U, e.V, e.N) := + Φ.hasFDerivAt_joint e + have hDU : D (1, 0, 0) = Φ.dS_dU e := by + have hline : HasDerivAt (fun u : ℝ => (u, e.V, e.N)) (1, 0, 0) e.U := + (hasDerivAt_id e.U).prodMk (hasDerivAt_const e.U (e.V, e.N)) + have hcomp : HasDerivAt (fun u => Φ.S u e.V e.N) (D (1, 0, 0)) e.U := by + change HasDerivAt ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun u : ℝ => (u, (e.V, e.N))) (D (1, 0, 0)) e.U + exact hfderiv.comp_hasDerivAt e.U hline + exact hcomp.unique (Φ.hasDerivAt_dS_dU e) + have hDV : D (0, 1, 0) = Φ.dS_dV e := by + have hline : HasDerivAt (fun v : ℝ => (e.U, v, e.N)) (0, 1, 0) e.V := + (hasDerivAt_const e.V e.U).prodMk + ((hasDerivAt_id e.V).prodMk (hasDerivAt_const e.V e.N)) + have hcomp : HasDerivAt (fun v => Φ.S e.U v e.N) (D (0, 1, 0)) e.V := by + change HasDerivAt ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun v : ℝ => (e.U, (v, e.N))) (D (0, 1, 0)) e.V + exact hfderiv.comp_hasDerivAt e.V hline + exact hcomp.unique (Φ.hasDerivAt_dS_dV e) + have hDN : D (0, 0, 1) = Φ.dS_dN e := by + have hline : HasDerivAt (fun n : ℝ => (e.U, e.V, n)) (0, 0, 1) e.N := + (hasDerivAt_const e.N e.U).prodMk + ((hasDerivAt_const e.N e.V).prodMk (hasDerivAt_id e.N)) + have hcomp : HasDerivAt (fun n => Φ.S e.U e.V n) (D (0, 0, 1)) e.N := by + change HasDerivAt ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ + fun n : ℝ => (e.U, (e.V, n))) (D (0, 0, 1)) e.N + exact hfderiv.comp_hasDerivAt e.N hline + exact hcomp.unique (Φ.hasDerivAt_dS_dN e) + have hsplit : ((a, b, c) : ℝ × ℝ × ℝ) + = a • (1, 0, 0) + b • (0, 1, 0) + c • (0, 0, 1) := by + simp [Prod.smul_mk, smul_eq_mul] + rw [hsplit, map_add, map_add, map_smul, map_smul, map_smul, hDU, hDV, hDN] + simp [smul_eq_mul] + +/-! ## D. Uniqueness from entropy partials + +The last lemmas show that a fundamental relation can be determined from its entropy partials +and one normalization value. The one-dimensional helper says that a function with zero +derivative everywhere on `Ioi 0` is constant there. + +The main theorem applies this to the residual `Φ.S - Ψ.S`. Equality of the `U` and `V` +entropy partials makes the residual independent of those coordinates. Extensivity controls +the remaining scaling direction, and agreement at one positive reference state makes the +residual vanish everywhere. -/ + +/-- A one-dimensional helper: if a real function has zero derivative everywhere on +`Ioi 0`, then it is constant on `Ioi 0`. -/ +private lemma eq_on_Ioi_of_hasDerivAt_zero {f : ℝ → ℝ} + (hf : ∀ {x : ℝ}, 0 < x → HasDerivAt f 0 x) + {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : + f x = f y := by + have hdiff : DifferentiableOn ℝ f (Set.Ioi (0 : ℝ)) := by + intro z hz + exact ((hf hz).differentiableAt).differentiableWithinAt + have hderiv : Set.EqOn (deriv f) 0 (Set.Ioi (0 : ℝ)) := by + intro z hz + exact (hf hz).deriv + exact (isOpen_Ioi (a := (0 : ℝ))).is_const_of_deriv_eq_zero + (isPreconnected_Ioi (a := (0 : ℝ))) hdiff hderiv hx hy + +/-- Uniqueness of a fundamental relation from its entropy partials and one reference value. + +If two fundamental relations have the same `∂S/∂U` and `∂S/∂V` at every positive extensive +state, and agree at one positive reference state, then the residual `Φ.S - Ψ.S` vanishes +everywhere on the positive orthant. Equivalently, the two fundamental relations agree exactly +on positive extensive states. -/ +lemma FundamentalRelation.eq_of_dS_dU_dS_dV_eq_of_eq_at + (Φ Ψ : FundamentalRelation) {U0 V0 N0 : ℝ} + (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + (hU : ∀ e : ExtensiveState, Φ.dS_dU e = Ψ.dS_dU e) + (hV : ∀ e : ExtensiveState, Φ.dS_dV e = Ψ.dS_dV e) + (href : Φ.S U0 V0 N0 = Ψ.S U0 V0 N0) : + ∀ e : ExtensiveState, Φ.S e.U e.V e.N = Ψ.S e.U e.V e.N := by + let sResidual : ℝ → ℝ → ℝ → ℝ := fun U V N => Φ.S U V N - Ψ.S U V N + have hResidual_hasDerivAt_U : + ∀ {U V N : ℝ}, 0 < U → 0 < V → 0 < N → + HasDerivAt (fun u => sResidual u V N) 0 U := by + intro U V N hUpos hVpos hNpos + let e : ExtensiveState := ⟨U, V, N, hUpos, hVpos, hNpos⟩ + have hΦ := Φ.hasDerivAt_dS_dU e + have hΨ := Ψ.hasDerivAt_dS_dU e + have hres : HasDerivAt ((fun u => Φ.S u V N) - fun u => Ψ.S u V N) + (Φ.dS_dU e - Ψ.dS_dU e) U := by + simpa [e] using hΦ.sub hΨ + have hzero : Φ.dS_dU e - Ψ.dS_dU e = 0 := by + rw [hU e] + ring + have hres0 : HasDerivAt ((fun u => Φ.S u V N) - fun u => Ψ.S u V N) 0 U := by + simpa [hzero] using hres + convert hres0 using 1 + ext u + simp [sResidual] + have hResidual_hasDerivAt_V : + ∀ {U V N : ℝ}, 0 < U → 0 < V → 0 < N → + HasDerivAt (fun v => sResidual U v N) 0 V := by + intro U V N hUpos hVpos hNpos + let e : ExtensiveState := ⟨U, V, N, hUpos, hVpos, hNpos⟩ + have hΦ := Φ.hasDerivAt_dS_dV e + have hΨ := Ψ.hasDerivAt_dS_dV e + have hres : HasDerivAt ((fun v => Φ.S U v N) - fun v => Ψ.S U v N) + (Φ.dS_dV e - Ψ.dS_dV e) V := by + simpa [e] using hΦ.sub hΨ + have hzero : Φ.dS_dV e - Ψ.dS_dV e = 0 := by + rw [hV e] + ring + have hres0 : HasDerivAt ((fun v => Φ.S U v N) - fun v => Ψ.S U v N) 0 V := by + simpa [hzero] using hres + convert hres0 using 1 + ext v + simp [sResidual] + have hConstU : + ∀ {U₁ U₂ V N : ℝ}, 0 < U₁ → 0 < U₂ → 0 < V → 0 < N → + sResidual U₁ V N = sResidual U₂ V N := by + intro U₁ U₂ V N hU₁ hU₂ hVpos hNpos + exact eq_on_Ioi_of_hasDerivAt_zero + (fun hUpos => hResidual_hasDerivAt_U hUpos hVpos hNpos) hU₁ hU₂ + have hConstV : + ∀ {U V₁ V₂ N : ℝ}, 0 < U → 0 < V₁ → 0 < V₂ → 0 < N → + sResidual U V₁ N = sResidual U V₂ N := by + intro U V₁ V₂ N hUpos hV₁ hV₂ hNpos + exact eq_on_Ioi_of_hasDerivAt_zero + (fun hVpos => hResidual_hasDerivAt_V hUpos hVpos hNpos) hV₁ hV₂ + have hConstUV : + ∀ {U₁ U₂ V₁ V₂ N : ℝ}, 0 < U₁ → 0 < U₂ → 0 < V₁ → 0 < V₂ → 0 < N → + sResidual U₁ V₁ N = sResidual U₂ V₂ N := by + intro U₁ U₂ V₁ V₂ N hU₁ hU₂ hV₁ hV₂ hNpos + calc + sResidual U₁ V₁ N = sResidual U₂ V₁ N := hConstU hU₁ hU₂ hV₁ hNpos + _ = sResidual U₂ V₂ N := hConstV hU₂ hV₁ hV₂ hNpos + have hResidual_hom : + ∀ {l : ℝ}, 0 < l → + sResidual (l * U0) (l * V0) (l * N0) = l * sResidual U0 V0 N0 := by + intro l hl + have hΦ := Φ.homogeneous hl U0 V0 N0 hU0 hV0 hN0 + have hΨ := Ψ.homogeneous hl U0 V0 N0 hU0 hV0 hN0 + dsimp [sResidual] + rw [hΦ, hΨ] + ring + intro e + let l : ℝ := e.N / N0 + have hl : 0 < l := div_pos e.hN hN0 + have hNl : l * N0 = e.N := by + dsimp [l] + field_simp [hN0.ne'] + have hzero : sResidual e.U e.V e.N = 0 := by + calc + sResidual e.U e.V e.N = sResidual (l * U0) (l * V0) e.N := + hConstUV e.hU (mul_pos hl hU0) e.hV (mul_pos hl hV0) e.hN + _ = sResidual (l * U0) (l * V0) (l * N0) := by rw [hNl] + _ = l * sResidual U0 V0 N0 := hResidual_hom hl + _ = 0 := by simp [sResidual, href] + dsimp [sResidual] at hzero + exact sub_eq_zero.mp hzero + +end + +end Thermodynamics From 3f03d3387bf0d3501f96f8a7dd0fc77b88e58431 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 11:58:55 +0400 Subject: [PATCH 3/8] feat(Thermodynamics): add ThermoModel bridge 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. --- .../FundamentalRelation/Model.lean | 109 ++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 Physlib/Thermodynamics/FundamentalRelation/Model.lean diff --git a/Physlib/Thermodynamics/FundamentalRelation/Model.lean b/Physlib/Thermodynamics/FundamentalRelation/Model.lean new file mode 100644 index 000000000..6bf6a8f25 --- /dev/null +++ b/Physlib/Thermodynamics/FundamentalRelation/Model.lean @@ -0,0 +1,109 @@ +/- +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.Entropy +public import Physlib.Thermodynamics.FundamentalRelation.Basic + +/-! +# The thermodynamic bridge + +## i. Overview + +A `ThermoModel Φ` is a model of a smooth coordinate fundamental relation `Φ` +(Callen's `S = S(U, V, N)`) as a concrete abstract thermodynamic core. +It supplies a single system `Γ`, a chart `coords` from positive extensive states into the +abstract state space, an entropy representation, and two linking +hypotheses — `entropy_agrees` (the coordinate entropy equals the abstract entropy on charted +states) and `comparison` (the Lieb-Yngvason Comparison Hypothesis on `Γ`). + +From these we *derive* the **Entropy Principle** for the model (`entropyPrinciple`): on charted +states, Callen's entropy order coincides with adiabatic accessibility, +`Φ.S e₁ ≤ Φ.S e₂ ↔ coords e₁ ≺ coords e₂` . + +## ii. Key results + +- `ThermoModel` — a model of `Φ`, bundling a core, chart, entropy representation, and the two + linking hypotheses `entropy_agrees` and `comparison`. +- `ThermoModel.entropyPrinciple` — the derived Entropy Principle: entropy order coincides with + adiabatic accessibility on charted states. + +## iii. Table of contents + +- A. The model +- B. The entropy principle (derived) + +## iv. References + +- E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of + Thermodynamics*, Physics Reports **310** (1999) 1-96. The Entropy Principle (monotonicity), + §II.B eq. (2.3); the Comparison Hypothesis as a hypothesis, §II; proved for simple systems, + §III-IV. +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley + (1985). The fundamental relation `S = S(U, V, N)`, §1.10. +-/ + +@[expose] public section + +namespace Thermodynamics + +universe u + +/-! ## A. The model + +`ThermoModel Φ` exhibits the smooth fundamental relation `Φ` as a model of the abstract +interface. It charts only positive extensive states into one abstract system `Γ`, identifies +the two entropies there (`entropy_agrees`), and assumes the Comparison Hypothesis on `Γ` +(`comparison`). -/ + +/-- A model of the smooth coordinate fundamental relation `Φ` inside the abstract +accessibility-and-entropy interface. + +The bundled `core` is only a `ThermoSystemCore`, so this bridge needs no `ThermoWorld`. +`coords` charts positive extensive states into a single abstract system `Γ`; `entropy_agrees` +identifies the coordinate and abstract entropies there; and `comparison` is the Lieb-Yngvason +Comparison Hypothesis on `Γ`. -/ +structure ThermoModel (Φ : FundamentalRelation) where + /-- The abstract type of thermodynamic systems used by this model. -/ + {System : Type u} + /-- The operational thermodynamic core. No Lieb-Yngvason axioms are required by the bridge. -/ + core : ThermoSystemCore System + /-- The abstract system charted by the positive extensive coordinate states. -/ + Γ : System + /-- The abstract entropy representation associated to the core. -/ + entropy : @EntropyRepresentation System core + /-- The coordinate chart from positive extensive states into the abstract state space. -/ + coords : ExtensiveState → core.State Γ + /-- The coordinate entropy agrees with the abstract entropy on charted states: + `Φ.S e = entropy.S ⟨Γ, coords e⟩`. Equivalently, `coords` is entropy-preserving. -/ + entropy_agrees : ∀ e : ExtensiveState, + Φ.S e.U e.V e.N = entropy.S ⟨Γ, coords e⟩ + /-- The Lieb-Yngvason Comparison Hypothesis on the charted system: any two states of `Γ` are + adiabatically comparable. -/ + comparison : ComparisonHypothesis (T := core) Γ + +namespace ThermoModel + +/-! ## B. The entropy principle + +The Entropy Principle for the model is a theorem, obtained by discharging the entropy +representation's conditional monotonicity with the Comparison Hypothesis. -/ + +/-- The **Entropy Principle** for the model: on charted states, Callen's coordinate-entropy order +coincides with primitive adiabatic accessibility, `Φ.S e₁ ≤ Φ.S e₂ ↔ coords e₁ ≺ coords e₂`. +This is the entropy representation's conditional `Monotonicity` (valid on comparable states) +discharged everywhere on `Γ` by `comparison`. -/ +lemma entropyPrinciple {Φ : FundamentalRelation} (M : ThermoModel Φ) (e₁ e₂ : ExtensiveState) : + (Φ.S e₁.U e₁.V e₁.N ≤ Φ.S e₂.U e₂.V e₂.N) ↔ + M.core.le (M.coords e₁) (M.coords e₂) := by + letI := M.core + rw [M.entropy_agrees e₁, M.entropy_agrees e₂] + exact (M.entropy.Monotonicity (M.coords e₁) (M.coords e₂) + (M.comparison (M.coords e₁) (M.coords e₂))).symm + +end ThermoModel + +end Thermodynamics From d44b8f4a86798662172fe1c1ef48e900b73d12ce Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 11:59:55 +0400 Subject: [PATCH 4/8] feat(Thermodynamics): characterize the ideal gas fundamental relation 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. --- Physlib/Thermodynamics/IdealGas/Basic.lean | 292 +++++++++++++++++++-- 1 file changed, 277 insertions(+), 15 deletions(-) diff --git a/Physlib/Thermodynamics/IdealGas/Basic.lean b/Physlib/Thermodynamics/IdealGas/Basic.lean index 836054055..905753d8c 100644 --- a/Physlib/Thermodynamics/IdealGas/Basic.lean +++ b/Physlib/Thermodynamics/IdealGas/Basic.lean @@ -1,34 +1,74 @@ /- Copyright (c) 2025 Fabio Anza. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Mitch Scheffer, Fabio Anza +Authors: Mitch Scheffer, Fabio Anza, Nathaneal Sajan -/ module -public import Mathlib.Analysis.SpecialFunctions.Pow.Real -- for Real.rpow_def_of_pos +public import Mathlib.Analysis.SpecialFunctions.Log.Deriv +public import Mathlib.Analysis.SpecialFunctions.Pow.Real +public import Physlib.Thermodynamics.FundamentalRelation.Intensive /-! -# Ideal gas: basic entropy and adiabatic relations +# Ideal gas: entropy, equations of state, and characterization -In this module we formalize a simple thermodynamic model of a monophase -ideal gas. We: +## i. Overview -* Define the entropy - S(U,V,N) = N s₀ + N R (c \log(U/U₀) + \log(V/V₀) - (c+1)\log(N/N₀)), -* Prove equivalent formulations of the adiabatic relation for two states - (U_a, V_a) and (U_b, V_b) at fixed N: +This module formalizes the single-component simple ideal gas in the entropy representation. +The entropy is - 1. c \log(U_a/U_b) + \log(V_a/V_b) = 0, - 2. (U_a/U_b)^c (V_a/V_b) = 1, - 3. U_a^c V_a = U_b^c V_b (the latter follows from (2)). +`S(U,V,N) = N * s0 + N * R * + (c * log (U/U0) + log (V/V0) - (c+1) * log (N/N0))`. + +The first part records this entropy formula and two equivalent forms of the fixed-`N` +adiabatic relation. The rest of the file connects the entropy formula to the general +`FundamentalRelation` interface: it proves the needed coordinate derivatives and extensivity, +packages the entropy as a `FundamentalRelation`, and derives the mechanical and caloric +equations of state. + +The final theorem is a converse statement. If a `FundamentalRelation` satisfies the ideal-gas +mechanical equation `PV = NRT`, the caloric equation `U = cNRT`, and agrees with the ideal-gas +entropy at one positive reference state, then it agrees with the ideal-gas entropy at every +positive extensive state. This is determination of the fundamental equation from equations of +state and one normalization value. + +## ii. Key results + +- `entropy` - the simple ideal-gas entropy in the entropy representation. +- `adiabatic_relation_log`, `adiabatic_relation_UaUbVaVb` - fixed-`N` adiabatic relations. +- `idealGasFR` - the ideal-gas entropy packaged as a `FundamentalRelation`. +- `idealGas_law`, `idealGas_caloric` - the equations of state `PV = NRT` and `U = cNRT`. +- `idealGas_characterization` - determination of the entropy from those equations of state + and one reference value. + +## iii. Table of contents + +- A. Entropy and adiabatic relations +- B. Coordinate derivatives and extensivity +- C. The ideal-gas fundamental relation +- D. Equations of state +- E. Determination from equations of state + +## iv. References + +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley + (1985). -/ @[expose] public section open Real +open scoped ContDiff noncomputable section +namespace Thermodynamics.IdealGas + +/-! ## A. Entropy and adiabatic relations + +The file starts with the entropy formula for a single-component simple ideal gas and the +fixed-particle-number adiabatic relation obtained by equating that entropy at two states. -/ + /-- Entropy of a monophase ideal gas: S(U,V,N) = N s0 + N R (c log(U/U0) + log(V/V0) - (c+1) log(N/N0)). -/ def entropy @@ -43,7 +83,7 @@ def entropy If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then c * log (Ua/Ub) + log (Va/Vb) = 0. -/ -theorem adiabatic_relation_log +lemma adiabatic_relation_log {s0 U0 V0 N0 c R : ℝ} {Ua Ub Va Vb N : ℝ} (hUa : 0 < Ua) (hUb : 0 < Ub) @@ -71,8 +111,7 @@ theorem adiabatic_relation_log If S(Ua,Va,N) = S(Ub,Vb,N) with N fixed, then (Ua/Ub)^c * (Va/Vb) = 1. -/ - -theorem adiabatic_relation_UaUbVaVb +lemma adiabatic_relation_UaUbVaVb {s0 U0 V0 N0 c R : ℝ} {Ua Ub Va Vb N : ℝ} (hUa : 0 < Ua) (hUb : 0 < Ub) @@ -89,3 +128,226 @@ theorem adiabatic_relation_UaUbVaVb show (Ua / Ub) ^ c * (Va / Vb) = 1 rw [Real.rpow_def_of_pos (div_pos hUa hUb), ← Real.exp_log (div_pos hVa hVb), ← Real.exp_add, mul_comm (log (Ua / Ub)) c, hlog, Real.exp_zero] + +/-! ## B. Coordinate derivatives and extensivity + +The next lemmas compute the `U` and `V` coordinate derivatives of the ideal-gas entropy and +prove degree-one homogeneity on the positive orthant. These are the ingredients needed to +construct the `FundamentalRelation` below. -/ + +/-- Energy-coordinate derivative of the ideal-gas entropy: +`∂S/∂U = N * R * c / U`. -/ +lemma hasDerivAt_entropy_U (c R s0 U0 V0 N0 U V N : ℝ) + (hU : 0 < U) (hU0 : 0 < U0) : + HasDerivAt (fun u => entropy c R s0 U0 V0 N0 u V N) (N * R * c / U) U := by + have hlogU : HasDerivAt (fun u => log (u / U0)) (1 / U) U := by + change HasDerivAt (log ∘ fun u : ℝ => u / U0) (1 / U) U + have hquot : HasDerivAt (fun u : ℝ => u / U0) (1 / U0) U := by + simpa using (hasDerivAt_id U).div_const U0 + have hlog := (Real.hasDerivAt_log (div_ne_zero hU.ne' hU0.ne')).comp U hquot + have hval : U0 / U * U0⁻¹ = U⁻¹ := by + field_simp [hU.ne', hU0.ne'] + simpa [one_div, hval] using hlog + have hbracket : HasDerivAt + (fun u => c * log (u / U0) + log (V / V0) - (c + 1) * log (N / N0)) + (c * (1 / U)) U := by + exact ((hlogU.const_mul c).add_const _).sub_const _ + have htotal : HasDerivAt + (fun u => N * s0 + N * R * + (c * log (u / U0) + log (V / V0) - (c + 1) * log (N / N0))) + (N * R * (c * (1 / U))) U := by + exact (hbracket.const_mul (N * R)).const_add (N * s0) + have hval : N * R * (c * U⁻¹) = N * R * c / U := by + ring + simpa [entropy, one_div, hval] using htotal + +/-- Volume-coordinate derivative of the ideal-gas entropy: `∂S/∂V = N * R / V`. -/ +lemma hasDerivAt_entropy_V (c R s0 U0 V0 N0 U V N : ℝ) + (hV : 0 < V) (hV0 : 0 < V0) : + HasDerivAt (fun v => entropy c R s0 U0 V0 N0 U v N) (N * R / V) V := by + have hlogV : HasDerivAt (fun v => log (v / V0)) (1 / V) V := by + change HasDerivAt (log ∘ fun v : ℝ => v / V0) (1 / V) V + have hquot : HasDerivAt (fun v : ℝ => v / V0) (1 / V0) V := by + simpa using (hasDerivAt_id V).div_const V0 + have hlog := (Real.hasDerivAt_log (div_ne_zero hV.ne' hV0.ne')).comp V hquot + have hval : V0 / V * V0⁻¹ = V⁻¹ := by + field_simp [hV.ne', hV0.ne'] + simpa [one_div, hval] using hlog + have hbracket : HasDerivAt + (fun v => c * log (U / U0) + log (v / V0) - (c + 1) * log (N / N0)) + (1 / V) V := by + exact (hlogV.const_add _).sub_const _ + have htotal : HasDerivAt + (fun v => N * s0 + N * R * + (c * log (U / U0) + log (v / V0) - (c + 1) * log (N / N0))) + (N * R * (1 / V)) V := by + exact (hbracket.const_mul (N * R)).const_add (N * s0) + have hval : N * R * V⁻¹ = N * R / V := by + ring + simpa [entropy, one_div, hval] using htotal + +/-- Degree-one homogeneity of the ideal-gas entropy on the positive orthant: +`S(lU, lV, lN) = l * S(U,V,N)` for `l > 0`. -/ +lemma entropy_homogeneous (c R s0 U0 V0 N0 : ℝ) + (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + {l : ℝ} (hl : 0 < l) (U V N : ℝ) (hU : 0 < U) (hV : 0 < V) + (hN : 0 < N) : + entropy c R s0 U0 V0 N0 (l * U) (l * V) (l * N) = + l * entropy c R s0 U0 V0 N0 U V N := by + unfold entropy + rw [mul_div_assoc, mul_div_assoc, mul_div_assoc] + rw [Real.log_mul hl.ne' (div_ne_zero hU.ne' hU0.ne')] + rw [Real.log_mul hl.ne' (div_ne_zero hV.ne' hV0.ne')] + rw [Real.log_mul hl.ne' (div_ne_zero hN.ne' hN0.ne')] + ring + +/-! ## C. The ideal-gas fundamental relation + +The entropy formula is now packaged as a `FundamentalRelation`. The positivity assumptions on +`c`, `R`, and the reference coordinates ensure that the entropy is smooth on the positive +orthant, has positive `∂S/∂U`, and is extensive. -/ + +/-- The ideal-gas entropy packaged as a `FundamentalRelation`. + +The assumptions `0 < c` and `0 < R` give `∂S/∂U = N * R * c / U > 0`, while the positive +reference values keep the logarithmic entropy formula on its intended domain. -/ +def idealGasFR (c R s0 U0 V0 N0 : ℝ) + (hc : 0 < c) (hR : 0 < R) (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) : + FundamentalRelation where + S := entropy c R s0 U0 V0 N0 + smooth := by + intro x hx + apply ContDiffAt.contDiffWithinAt + obtain ⟨hU, hV, hN⟩ := hx + unfold entropy + fun_prop (disch := positivity) + dS_dU_pos := by + intro U V N hU _hV hN + have hderiv := hasDerivAt_entropy_U c R s0 U0 V0 N0 U V N hU hU0 + rw [hderiv.deriv] + positivity + homogeneous := by + intro l hl U V N hU hV hN + exact entropy_homogeneous c R s0 U0 V0 N0 hU0 hV0 hN0 hl U V N hU hV hN + +/-- The energy derivative of the ideal-gas fundamental relation: +`∂S/∂U = N * R * c / U`. -/ +lemma dS_dU_idealGasFR (c R s0 U0 V0 N0 : ℝ) + (hc : 0 < c) (hR : 0 < R) (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + (e : ExtensiveState) : + (idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0).dS_dU e = + e.N * R * c / e.U := by + unfold FundamentalRelation.dS_dU + exact (hasDerivAt_entropy_U c R s0 U0 V0 N0 e.U e.V e.N e.hU hU0).deriv + +/-- The volume derivative of the ideal-gas fundamental relation: +`∂S/∂V = N * R / V`. -/ +lemma dS_dV_idealGasFR (c R s0 U0 V0 N0 : ℝ) + (hc : 0 < c) (hR : 0 < R) (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + (e : ExtensiveState) : + (idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0).dS_dV e = + e.N * R / e.V := by + unfold FundamentalRelation.dS_dV + exact (hasDerivAt_entropy_V c R s0 U0 V0 N0 e.U e.V e.N e.hV hV0).deriv + +/-! ## D. Equations of state + +The derivative formulas give the usual simple-ideal-gas equations of state in the intensive +parameters associated to `idealGasFR`: the mechanical equation `PV = NRT` and the caloric +equation `U = cNRT`. -/ + +/-- The mechanical equation of state for the simple ideal gas: `PV = NRT`. -/ +lemma idealGas_law (c R s0 U0 V0 N0 : ℝ) + (hc : 0 < c) (hR : 0 < R) (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + (e : ExtensiveState) : + (idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0).pressure e * e.V = + e.N * R * (idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0).temperature e := by + simp only [FundamentalRelation.pressure, FundamentalRelation.temperature, + dS_dU_idealGasFR, dS_dV_idealGasFR] + field_simp [e.hU.ne', e.hV.ne', e.hN.ne', hc.ne', hR.ne'] + +/-- The caloric equation of state for the simple ideal gas: `U = cNRT`. -/ +lemma idealGas_caloric (c R s0 U0 V0 N0 : ℝ) + (hc : 0 < c) (hR : 0 < R) (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + (e : ExtensiveState) : + e.U = c * e.N * R * + (idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0).temperature e := by + simp only [FundamentalRelation.temperature, dS_dU_idealGasFR] + field_simp [e.hU.ne', e.hV.ne', e.hN.ne', hc.ne', hR.ne'] + +/-! ## E. Determination from equations of state + +The last theorem proves the converse direction. The private lemmas turn the assumed mechanical +and caloric equations of state back into equality of the `V` and `U` entropy partials. The +general uniqueness theorem for `FundamentalRelation`s in `intensive.lean` shows that the residual +against the ideal-gas entropy vanishes everywhere once one reference value is fixed. -/ + +/-- The caloric equation of state `U = cNRT` determines the energy entropy partial +`∂S/∂U = N * R * c / U`. -/ +private lemma dS_dU_eq_of_caloric (Φ : FundamentalRelation) (c R : ℝ) + (caloric : ∀ e : ExtensiveState, e.U = c * e.N * R * Φ.temperature e) + (e : ExtensiveState) : + Φ.dS_dU e = e.N * R * c / e.U := by + have hDpos : 0 < Φ.dS_dU e := by + simpa [FundamentalRelation.dS_dU] using + Φ.dS_dU_pos e.U e.V e.N e.hU e.hV e.hN + have hDne : Φ.dS_dU e ≠ 0 := hDpos.ne' + have hcal := caloric e + simp only [FundamentalRelation.temperature] at hcal + have hmul : e.U * Φ.dS_dU e = c * e.N * R := by + calc + e.U * Φ.dS_dU e = + (c * e.N * R * (Φ.dS_dU e)⁻¹) * Φ.dS_dU e := by rw [hcal] + _ = c * e.N * R := by field_simp [hDne] + calc + Φ.dS_dU e = (e.U * Φ.dS_dU e) / e.U := by field_simp [e.hU.ne'] + _ = (c * e.N * R) / e.U := by rw [hmul] + _ = e.N * R * c / e.U := by ring + +/-- The mechanical equation of state `PV = NRT` determines the volume entropy partial +`∂S/∂V = N * R / V`. -/ +private lemma dS_dV_eq_of_mechanical (Φ : FundamentalRelation) (R : ℝ) + (mechanical : ∀ e : ExtensiveState, Φ.pressure e * e.V = e.N * R * Φ.temperature e) + (e : ExtensiveState) : + Φ.dS_dV e = e.N * R / e.V := by + have hTne : Φ.temperature e ≠ 0 := (Φ.temperature_pos e).ne' + have hmech := mechanical e + simp only [FundamentalRelation.pressure] at hmech + calc + Φ.dS_dV e = + (Φ.temperature e * Φ.dS_dV e * e.V) / (Φ.temperature e * e.V) := by + field_simp [hTne, e.hV.ne'] + _ = (e.N * R * Φ.temperature e) / (Φ.temperature e * e.V) := by rw [hmech] + _ = e.N * R / e.V := by + field_simp [hTne, e.hV.ne'] + +/-- Determination of the ideal-gas entropy from its equations of state. + +If a `FundamentalRelation` satisfies the mechanical equation `PV = NRT`, the caloric equation +`U = cNRT`, and agrees with the ideal-gas entropy at one positive reference state, then it +equals the ideal-gas entropy on every positive extensive state. The proof converts the two +equations of state into equality of entropy partials and applies +`FundamentalRelation.eq_of_dS_dU_dS_dV_eq_of_eq_at`. -/ +lemma idealGas_characterization (Φ : FundamentalRelation) (c R s0 U0 V0 N0 : ℝ) + (hc : 0 < c) (hR : 0 < R) (hU0 : 0 < U0) (hV0 : 0 < V0) (hN0 : 0 < N0) + (href : Φ.S U0 V0 N0 = entropy c R s0 U0 V0 N0 U0 V0 N0) + (mechanical : ∀ e : ExtensiveState, Φ.pressure e * e.V = e.N * R * Φ.temperature e) + (caloric : ∀ e : ExtensiveState, e.U = c * e.N * R * Φ.temperature e) : + ∀ e : ExtensiveState, Φ.S e.U e.V e.N = + entropy c R s0 U0 V0 N0 e.U e.V e.N := by + -- The positivity assumptions are needed here to construct the ideal-gas + -- `FundamentalRelation`, whose `dS_dU_pos` field uses `∂S/∂U = N * R * c / U > 0`. + let Ψ := idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0 + have hU_eq : ∀ e : ExtensiveState, Φ.dS_dU e = Ψ.dS_dU e := by + intro e + rw [dS_dU_eq_of_caloric Φ c R caloric e] + exact (dS_dU_idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0 e).symm + have hV_eq : ∀ e : ExtensiveState, Φ.dS_dV e = Ψ.dS_dV e := by + intro e + rw [dS_dV_eq_of_mechanical Φ R mechanical e] + exact (dS_dV_idealGasFR c R s0 U0 V0 N0 hc hR hU0 hV0 hN0 e).symm + have hrefΨ : Φ.S U0 V0 N0 = Ψ.S U0 V0 N0 := by + simpa [Ψ, idealGasFR] using href + exact Φ.eq_of_dS_dU_dS_dV_eq_of_eq_at Ψ hU0 hV0 hN0 hU_eq hV_eq hrefΨ + +end Thermodynamics.IdealGas From f93e481edba2ad0178cf8b8ca0c759175e75500d Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 12:06:33 +0400 Subject: [PATCH 5/8] chore(Thermodynamics): register thermodynamics modules --- Physlib.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/Physlib.lean b/Physlib.lean index 4096ac4a2..7a4b32084 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -464,6 +464,12 @@ 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.Accessibility +public import Physlib.Thermodynamics.Foundation.Entropy +public import Physlib.Thermodynamics.FundamentalRelation.Basic +public import Physlib.Thermodynamics.FundamentalRelation.Intensive +public import Physlib.Thermodynamics.FundamentalRelation.Euler +public import Physlib.Thermodynamics.FundamentalRelation.Model public import Physlib.Thermodynamics.IdealGas.Basic public import Physlib.Thermodynamics.Temperature.Basic public import Physlib.Thermodynamics.Temperature.TemperatureUnits From 7a256366fd54269f10112db1047a52fc853d96f9 Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 13:24:22 +0400 Subject: [PATCH 6/8] chore(Thermodynamics): fix linter findings --- Physlib.lean | 2 +- .../Foundation/Accessibility.lean | 5 ++--- .../Thermodynamics/Foundation/Entropy.lean | 22 +++++++++---------- .../FundamentalRelation/Basic.lean | 2 +- .../FundamentalRelation/Euler.lean | 3 --- .../FundamentalRelation/Intensive.lean | 1 - .../FundamentalRelation/Model.lean | 2 +- 7 files changed, 16 insertions(+), 21 deletions(-) diff --git a/Physlib.lean b/Physlib.lean index 7a4b32084..7165bcf8d 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -467,8 +467,8 @@ public import Physlib.Thermodynamics.Basic public import Physlib.Thermodynamics.Foundation.Accessibility public import Physlib.Thermodynamics.Foundation.Entropy public import Physlib.Thermodynamics.FundamentalRelation.Basic -public import Physlib.Thermodynamics.FundamentalRelation.Intensive public import Physlib.Thermodynamics.FundamentalRelation.Euler +public import Physlib.Thermodynamics.FundamentalRelation.Intensive public import Physlib.Thermodynamics.FundamentalRelation.Model public import Physlib.Thermodynamics.IdealGas.Basic public import Physlib.Thermodynamics.Temperature.Basic diff --git a/Physlib/Thermodynamics/Foundation/Accessibility.lean b/Physlib/Thermodynamics/Foundation/Accessibility.lean index 01cb4fabf..3ce78b56e 100644 --- a/Physlib/Thermodynamics/Foundation/Accessibility.lean +++ b/Physlib/Thermodynamics/Foundation/Accessibility.lean @@ -5,7 +5,6 @@ Authors: Nathaneal Sajan -/ module -public import Mathlib.Order.Filter.AtTopBot.Defs public import Mathlib.Topology.Instances.Real.Lemmas /-! @@ -85,7 +84,7 @@ later layers depend only on the vocabulary they actually use. -/ /-- The operational core of a thermodynamic accessibility structure. A `ThermoSystemCore` records the state space indexed by each system, system composition, -system scaling, the zero system, and the primitive adiabatic-accessibility relation.-/ +system scaling, the zero system, and the primitive adiabatic-accessibility relation. -/ class ThermoSystemCore (System : Type u) where /-- The state space associated to a thermodynamic system. -/ State : System → Type v @@ -122,7 +121,7 @@ The fields are assumptions of the abstract world. -/ /-- This extends `ThermoSystemCore` with the structural equalities, accessibility axioms A1-A6, -and coherence axioms needed to reason about casts induced by equalities of systems.-/ +and coherence axioms needed to reason about casts induced by equalities of systems. -/ class ThermoWorld (System : Type u) extends ThermoSystemCore System where /-- Scaling by zero gives the zero system. -/ scale_zero_is_ZSystem (Γ : System) : scale 0 Γ = ZSystem diff --git a/Physlib/Thermodynamics/Foundation/Entropy.lean b/Physlib/Thermodynamics/Foundation/Entropy.lean index 4cff8eb1a..f74430b3f 100644 --- a/Physlib/Thermodynamics/Foundation/Entropy.lean +++ b/Physlib/Thermodynamics/Foundation/Entropy.lean @@ -71,34 +71,34 @@ def AllStates (System : Type u) [T : ThermoSystemCore System] := An `EntropyRepresentation` is the Entropy Principle turned into a structure: a real-valued `S` on `AllStates` that represents `≺` on comparable states (monotonicity), is additive under -composition, and is extensive under positive scaling.-/ +composition, and is extensive under positive scaling. -/ /-- An abstract entropy representation of a thermodynamic core: the Lieb-Yngvason Entropy Principle as a structure. A real-valued `S` on `AllStates` that represents adiabatic accessibility on comparable states, is additive under composition, and is extensive under -positive scaling.-/ +positive scaling. -/ structure EntropyRepresentation (System : Type u) [T : ThermoSystemCore System] where /-- The entropy of an arbitrary state, packaged with its system. -/ S : AllStates System → ℝ - /-- Monotonicity (Lieb-Yngvason eq. 2.3): for comparable states, accessibility is + /-- Monotonicity, Lieb-Yngvason eq. 2.3: 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 (Lieb-Yngvason eq. 2.4): `S(X, Y) = S(X) + S(Y)` across a composition. -/ + /-- Additivity, Lieb-Yngvason eq. 2.4: `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 (Lieb-Yngvason eq. 2.5): `S(t • X) = t · S(X)` for `t > 0`. -/ + /-- Extensivity, Lieb-Yngvason eq. 2.5: `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 -Immediate rephrasings of monotonicity : 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`. -/ +Immediate rephrasings of monotonicity: 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 @@ -117,8 +117,8 @@ lemma entropy_equiv_iff_eq {E : EntropyRepresentation System} {Γ₁ Γ₂ : Sys 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)`- - entropy strictly increases in an irreversible process. -/ +/-- 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 @@ -136,7 +136,7 @@ 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`).-/ +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 diff --git a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean index ca904ea08..ed56edcfc 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean @@ -100,7 +100,7 @@ structure FundamentalRelation where S : ℝ → ℝ → ℝ → ℝ /-- Regularity: `S` is C^∞ on the positive orthant. -/ smooth : ContDiffOn ℝ ∞ (fun p : ℝ × ℝ × ℝ => S p.1 p.2.1 p.2.2) posOrthant - /-- Postulate III (`T > 0`): for positive states, `∂S/∂U > 0`, i.e. + /-- Postulate III, `T > 0`: for positive states, `∂S/∂U > 0`, i.e. `1 / T > 0` pointwise. This yields positive temperature without invoking concavity. -/ dS_dU_pos : ∀ U V N, 0 < U → 0 < V → 0 < N → 0 < deriv (fun u => S u V N) U /-- Extensivity: `S` is homogeneous of degree one on the positive orthant, diff --git a/Physlib/Thermodynamics/FundamentalRelation/Euler.lean b/Physlib/Thermodynamics/FundamentalRelation/Euler.lean index 8e808d975..85e0df935 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Euler.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Euler.lean @@ -5,9 +5,6 @@ Authors: Nathaneal Sajan -/ module -public import Mathlib.Analysis.Calculus.Deriv.Comp -public import Mathlib.Analysis.Calculus.Deriv.Mul -public import Mathlib.Analysis.Calculus.Deriv.Prod public import Physlib.Thermodynamics.FundamentalRelation.Intensive /-! diff --git a/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean b/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean index 15c0bf249..31ab43b86 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean @@ -5,7 +5,6 @@ Authors: Nathaneal Sajan -/ module -public import Mathlib.Analysis.Calculus.Deriv.Comp public import Mathlib.Analysis.Calculus.Deriv.Prod public import Mathlib.Analysis.Calculus.MeanValue public import Physlib.Thermodynamics.FundamentalRelation.Basic diff --git a/Physlib/Thermodynamics/FundamentalRelation/Model.lean b/Physlib/Thermodynamics/FundamentalRelation/Model.lean index 6bf6a8f25..c74001d26 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Model.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Model.lean @@ -20,7 +20,7 @@ abstract state space, an entropy representation, and two linking hypotheses — `entropy_agrees` (the coordinate entropy equals the abstract entropy on charted states) and `comparison` (the Lieb-Yngvason Comparison Hypothesis on `Γ`). -From these we *derive* the **Entropy Principle** for the model (`entropyPrinciple`): on charted +From these we *derive* the **Entropy Principle** for the model via `entropyPrinciple`: on charted states, Callen's entropy order coincides with adiabatic accessibility, `Φ.S e₁ ≤ Φ.S e₂ ↔ coords e₁ ≺ coords e₂` . From 6527289bcace5f6f0425345b38258ef435240a0e Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Sat, 4 Jul 2026 14:15:13 +0400 Subject: [PATCH 7/8] refactor(Thermodynamics): rename ThermoModel.coords to stateOf --- .../FundamentalRelation/Basic.lean | 6 +-- .../FundamentalRelation/Model.lean | 43 ++++++++++--------- 2 files changed, 25 insertions(+), 24 deletions(-) diff --git a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean index ed56edcfc..6f71d611a 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean @@ -60,9 +60,9 @@ open scoped ContDiff A `FundamentalRelation` is regular only on physically admissible states — those with strictly positive `U`, `V`, `N`. We carry that positivity in two ways: `ExtensiveState` for the physical -states the later bridge charts, and `posOrthant` for the open set on which smoothness and the -energy derivative are asserted. Keeping positivity here, rather than in the type of `S`, lets the -calculus treat `S` as an ordinary total function. -/ +states the later bridge maps to abstract states, and `posOrthant` for the open set on which +smoothness and the energy derivative are asserted. Keeping positivity here, rather than in the +type of `S`, lets the calculus treat `S` as an ordinary total function. -/ /-- A positive **extensive state** `(U, V, N)` of a simple system: internal energy, volume and particle number, all strictly positive. This is the physical domain over diff --git a/Physlib/Thermodynamics/FundamentalRelation/Model.lean b/Physlib/Thermodynamics/FundamentalRelation/Model.lean index c74001d26..77c686047 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Model.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Model.lean @@ -15,21 +15,21 @@ public import Physlib.Thermodynamics.FundamentalRelation.Basic A `ThermoModel Φ` is a model of a smooth coordinate fundamental relation `Φ` (Callen's `S = S(U, V, N)`) as a concrete abstract thermodynamic core. -It supplies a single system `Γ`, a chart `coords` from positive extensive states into the +It supplies a single system `Γ`, a map `stateOf` from positive extensive states into the abstract state space, an entropy representation, and two linking -hypotheses — `entropy_agrees` (the coordinate entropy equals the abstract entropy on charted +hypotheses — `entropy_agrees` (the coordinate entropy equals the abstract entropy on mapped states) and `comparison` (the Lieb-Yngvason Comparison Hypothesis on `Γ`). -From these we *derive* the **Entropy Principle** for the model via `entropyPrinciple`: on charted +From these we *derive* the **Entropy Principle** for the model via `entropyPrinciple`: on mapped states, Callen's entropy order coincides with adiabatic accessibility, -`Φ.S e₁ ≤ Φ.S e₂ ↔ coords e₁ ≺ coords e₂` . +`Φ.S e₁ ≤ Φ.S e₂ ↔ stateOf e₁ ≺ stateOf e₂` . ## ii. Key results -- `ThermoModel` — a model of `Φ`, bundling a core, chart, entropy representation, and the two - linking hypotheses `entropy_agrees` and `comparison`. +- `ThermoModel` — a model of `Φ`, bundling a core, a coordinate map, an entropy representation, + and the two linking hypotheses `entropy_agrees` and `comparison`. - `ThermoModel.entropyPrinciple` — the derived Entropy Principle: entropy order coincides with - adiabatic accessibility on charted states. + adiabatic accessibility on mapped states. ## iii. Table of contents @@ -55,7 +55,7 @@ universe u /-! ## A. The model `ThermoModel Φ` exhibits the smooth fundamental relation `Φ` as a model of the abstract -interface. It charts only positive extensive states into one abstract system `Γ`, identifies +interface. It maps only positive extensive states into one abstract system `Γ`, identifies the two entropies there (`entropy_agrees`), and assumes the Comparison Hypothesis on `Γ` (`comparison`). -/ @@ -63,7 +63,7 @@ the two entropies there (`entropy_agrees`), and assumes the Comparison Hypothesi accessibility-and-entropy interface. The bundled `core` is only a `ThermoSystemCore`, so this bridge needs no `ThermoWorld`. -`coords` charts positive extensive states into a single abstract system `Γ`; `entropy_agrees` +`stateOf` maps positive extensive states into a single abstract system `Γ`; `entropy_agrees` identifies the coordinate and abstract entropies there; and `comparison` is the Lieb-Yngvason Comparison Hypothesis on `Γ`. -/ structure ThermoModel (Φ : FundamentalRelation) where @@ -71,17 +71,18 @@ structure ThermoModel (Φ : FundamentalRelation) where {System : Type u} /-- The operational thermodynamic core. No Lieb-Yngvason axioms are required by the bridge. -/ core : ThermoSystemCore System - /-- The abstract system charted by the positive extensive coordinate states. -/ + /-- The single abstract system the coordinate states map into. -/ Γ : System /-- The abstract entropy representation associated to the core. -/ entropy : @EntropyRepresentation System core - /-- The coordinate chart from positive extensive states into the abstract state space. -/ - coords : ExtensiveState → core.State Γ - /-- The coordinate entropy agrees with the abstract entropy on charted states: - `Φ.S e = entropy.S ⟨Γ, coords e⟩`. Equivalently, `coords` is entropy-preserving. -/ + /-- The abstract state of a coordinate state: sends each positive extensive state `(U, V, N)` + to its state in the abstract system `Γ`. -/ + stateOf : ExtensiveState → core.State Γ + /-- The coordinate entropy agrees with the abstract entropy on mapped states: + `Φ.S e = entropy.S ⟨Γ, stateOf e⟩`. Equivalently, `stateOf` is entropy-preserving. -/ entropy_agrees : ∀ e : ExtensiveState, - Φ.S e.U e.V e.N = entropy.S ⟨Γ, coords e⟩ - /-- The Lieb-Yngvason Comparison Hypothesis on the charted system: any two states of `Γ` are + Φ.S e.U e.V e.N = entropy.S ⟨Γ, stateOf e⟩ + /-- The Lieb-Yngvason Comparison Hypothesis on the system `Γ`: any two states of `Γ` are adiabatically comparable. -/ comparison : ComparisonHypothesis (T := core) Γ @@ -92,17 +93,17 @@ namespace ThermoModel The Entropy Principle for the model is a theorem, obtained by discharging the entropy representation's conditional monotonicity with the Comparison Hypothesis. -/ -/-- The **Entropy Principle** for the model: on charted states, Callen's coordinate-entropy order -coincides with primitive adiabatic accessibility, `Φ.S e₁ ≤ Φ.S e₂ ↔ coords e₁ ≺ coords e₂`. +/-- The **Entropy Principle** for the model: on mapped states, Callen's coordinate-entropy order +coincides with primitive adiabatic accessibility, `Φ.S e₁ ≤ Φ.S e₂ ↔ stateOf e₁ ≺ stateOf e₂`. This is the entropy representation's conditional `Monotonicity` (valid on comparable states) discharged everywhere on `Γ` by `comparison`. -/ lemma entropyPrinciple {Φ : FundamentalRelation} (M : ThermoModel Φ) (e₁ e₂ : ExtensiveState) : (Φ.S e₁.U e₁.V e₁.N ≤ Φ.S e₂.U e₂.V e₂.N) ↔ - M.core.le (M.coords e₁) (M.coords e₂) := by + M.core.le (M.stateOf e₁) (M.stateOf e₂) := by letI := M.core rw [M.entropy_agrees e₁, M.entropy_agrees e₂] - exact (M.entropy.Monotonicity (M.coords e₁) (M.coords e₂) - (M.comparison (M.coords e₁) (M.coords e₂))).symm + exact (M.entropy.Monotonicity (M.stateOf e₁) (M.stateOf e₂) + (M.comparison (M.stateOf e₁) (M.stateOf e₂))).symm end ThermoModel From 85a71af34ed9c24c9ba1067cc1f4b990bedab20d Mon Sep 17 00:00:00 2001 From: Nathaneal Date: Thu, 9 Jul 2026 12:35:08 +0400 Subject: [PATCH 8/8] refactor(Thermodynamics): address comments --- Physlib.lean | 5 +- .../Foundation/Accessibility.lean | 360 ------------------ .../Foundation/Comparability.lean | 95 +++++ Physlib/Thermodynamics/Foundation/Core.lean | 125 ++++++ .../Thermodynamics/Foundation/Entropy.lean | 65 ++-- Physlib/Thermodynamics/Foundation/World.lean | 291 ++++++++++++++ .../FundamentalRelation/Basic.lean | 92 ++--- .../FundamentalRelation/ExtensiveState.lean | 132 +++++++ .../FundamentalRelation/Intensive.lean | 56 ++- .../FundamentalRelation/Model.lean | 49 ++- 10 files changed, 755 insertions(+), 515 deletions(-) delete mode 100644 Physlib/Thermodynamics/Foundation/Accessibility.lean create mode 100644 Physlib/Thermodynamics/Foundation/Comparability.lean create mode 100644 Physlib/Thermodynamics/Foundation/Core.lean create mode 100644 Physlib/Thermodynamics/Foundation/World.lean create mode 100644 Physlib/Thermodynamics/FundamentalRelation/ExtensiveState.lean diff --git a/Physlib.lean b/Physlib.lean index 7165bcf8d..f66362d88 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -464,10 +464,13 @@ 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.Accessibility +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 diff --git a/Physlib/Thermodynamics/Foundation/Accessibility.lean b/Physlib/Thermodynamics/Foundation/Accessibility.lean deleted file mode 100644 index 3ce78b56e..000000000 --- a/Physlib/Thermodynamics/Foundation/Accessibility.lean +++ /dev/null @@ -1,360 +0,0 @@ -/- -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.Topology.Instances.Real.Lemmas - -/-! -# Adiabatic accessibility - -## i. Overview - -This module defines a thermodynamics interface for the abstract Lieb-Yngvason accessibility -foundation. - -The primitive is a preorder `≺` 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 have moved in a -gravitational field (Lieb-Yngvason 1999, §II.A). From `≺` one reads off adiabatic -equivalence `X ≈ Y` (`X ≺ Y` and `Y ≺ X`) and strict accessibility `X ≺≺ Y` (`X ≺ Y` -but not `Y ≺ X`), the latter being the irreversible processes. - -The eventual goal would be 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`). - -The file is split into two classes: - -* `ThermoSystemCore` contains the operational vocabulary: systems, their state - spaces, composition, scaling, the zero system, and the primitive adiabatic-accessibility - relation `≺`. -* `ThermoWorld` extends the core with the algebraic identities on systems, the - accessibility axioms A1-A6, and the cast-coherence axioms needed because Lean - distinguishes propositionally-equal state spaces that Lieb-Yngvason identify. - -## ii. Key results - -- `ThermoSystemCore` / `ThermoWorld` — the two-layer abstract interface. -- `Comparable`, `ComparisonHypothesis`, `GlobalComparisonHypothesis` — the comparability - vocabulary. The comparison hypothesis is stated as a *hypothesis*, carried separately, - never baked into the axioms (see §C). -- `StrictlyPrecedes` (`≺≺`) — irreversible accessibility. -- `thermo_le_refl`, `thermo_le_trans`, `thermo_equiv_refl`, `thermo_equiv_symm`, - `calcTransThermoLe` — the preorder API exposing A1/A2 for calculation. - -## iii. Table of contents - -- A. Operational core (`ThermoSystemCore`) -- B. Lieb-Yngvason worlds (`ThermoWorld`) - - B.1. System algebra - - B.2. Accessibility axioms A1-A6 - - B.3. Coherence of casts -- C. Comparability -- D. Core API -- E. World API - -## iv. References - -- E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of - Thermodynamics*, Physics Reports **310** (1999) 1-96. Adiabatic accessibility and its - operational definition, §II.A; the entropy principle, §II.B; the order axioms A1-A6 and - the comparison hypothesis CH, §II.C. -- E.H. Lieb and J. Yngvason, *The Mathematical Structure of the Second Law of - Thermodynamics*, Current Developments in Mathematics **2001** (2002) 89-129; - arXiv:math-ph/0204007. A streamlined re-presentation of the same axiomatics. --/ - -@[expose] public section - -namespace Thermodynamics - -universe u v - -/-! ## A. Operational core - -We first fix the operational vocabulary of thermodynamics with no axioms attached. -A `ThermoSystemCore` records, for each *system*, its space of equilibrium *states*, -together with the two ways of building new systems — composition `⊗` (placing two systems -side by side) and scaling `•` (taking a `t`-sized copy) — the zero system, and the -primitive adiabatic-accessibility relation `≺`. Separating this core from the axioms lets -later layers depend only on the vocabulary they actually use. -/ - -/-- The operational core of a thermodynamic accessibility structure. - -A `ThermoSystemCore` records the state space indexed by each system, system composition, -system scaling, the zero system, and the primitive adiabatic-accessibility relation. -/ -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`: `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. States may belong to different systems. -/ - 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. Lieb-Yngvason worlds - -A `ThermoWorld` extends the core with the assumptions Lieb-Yngvason place on `≺`. These -fall into three groups: the algebraic identities making composition an associative, -commutative operation on which scaling acts compatibly; the six accessibility -axioms A1-A6; and coherence axioms relating states across *equal* systems. The last -group has no Lieb-Yngvason axiom number: the paper treats identities like -`(Γ₁ ⊗ Γ₂) = (Γ₂ ⊗ Γ₁)` as strict equalities of state spaces and uses them silently, but in -Lean equal systems yield state spaces that are only propositionally equal, so each identity -is paired with a statement that transporting a state along it lands on an -adiabatically-equivalent state. - -The fields are assumptions of the abstract world. -/ - -/-- -This extends `ThermoSystemCore` with the structural equalities, accessibility axioms A1-A6, -and coherence axioms needed to reason about casts induced by equalities of systems. -/ -class ThermoWorld (System : Type u) extends ThermoSystemCore System where - /-- Scaling by zero gives the zero system. -/ - scale_zero_is_ZSystem (Γ : System) : scale 0 Γ = ZSystem - - /-- Composition of systems is associative, up to equality of systems. -/ - comp_assoc (Γ₁ Γ₂ Γ₃ : System) : comp (comp Γ₁ Γ₂) Γ₃ = comp Γ₁ (comp Γ₂ Γ₃) - /-- Composition of systems is commutative, up to equality of systems. -/ - comp_comm (Γ₁ Γ₂ : System) : comp Γ₁ Γ₂ = comp Γ₂ Γ₁ - /-- Scaling distributes over composition of systems. -/ - scale_distrib_comp (t : ℝ) (Γ₁ Γ₂ : System) : - scale t (comp Γ₁ Γ₂) = comp (scale t Γ₁) (scale t Γ₂) - /-- Successive scalings multiply their scale factors. -/ - smul_smul (t s : ℝ) (Γ : System) : scale (t * s) Γ = scale t (scale s Γ) - /-- Scaling by one leaves the system unchanged. -/ - one_smul (Γ : System) : scale 1 Γ = Γ - - /-- A1, reflexivity: every state is accessible from itself, `X ≺ X`. -/ - A1 {Γ : System} (X : State Γ) : le X X - /-- A2, transitivity: `X ≺ Y` and `Y ≺ Z` give `X ≺ Z`. -/ - A2 {Γ₁ Γ₂ Γ₃ : System} {X : State Γ₁} {Y : State Γ₂} {Z : State Γ₃} : - le X Y → le Y Z → le X Z - /-- A3, consistency: accessibility is preserved by composition — - `X₁ ≺ Y₁` and `X₂ ≺ Y₂` give `(X₁, X₂) ≺ (Y₁, Y₂)`. -/ - A3 {Γ₁ Γ₂ Γ₃ Γ₄ : System} - {X₁ : State Γ₁} {X₂ : State Γ₂} {Y₁ : State Γ₃} {Y₂ : State Γ₄} : - le X₁ Y₁ → le X₂ Y₂ → - le (state_of_comp_equiv.symm (X₁, X₂)) (state_of_comp_equiv.symm (Y₁, Y₂)) - /-- A4, scaling invariance: if `X ≺ Y` then `t • X ≺ t • Y` for every `t > 0`. -/ - A4 {Γ₁ Γ₂ : System} {X : State Γ₁} {Y : State Γ₂} {t : ℝ} (ht : 0 < t) : - le X Y → le ((state_of_scale_equiv ht.ne.symm).symm X) - ((state_of_scale_equiv ht.ne.symm).symm Y) - /-- A5, splitting and recombination: for `0 < t < 1` a state is adiabatically equivalent - to its split into a `t`-copy and a `(1−t)`-copy, `X ≈ (t • X, (1−t) • X)`. -/ - A5 {Γ : System} (X : State Γ) {t : ℝ} (ht : 0 < t ∧ t < 1) : - le X - (state_of_comp_equiv.symm - (((state_of_scale_equiv ht.1.ne').symm X), - ((state_of_scale_equiv (t := 1 - t) (by - have hpos : 0 < 1 - t := sub_pos.mpr ht.2 - exact hpos.ne')).symm X))) ∧ - le (state_of_comp_equiv.symm - (((state_of_scale_equiv ht.1.ne').symm X), - ((state_of_scale_equiv (t := 1 - t) (by - have hpos : 0 < 1 - t := sub_pos.mpr ht.2 - exact hpos.ne')).symm X))) X - /-- A6, stability: accessibility cannot be created by an infinitesimal perturbation. - - If `(X, epsilon_n Z₀)` is adiabatically accessible to `(Y, epsilon_n Z₁)` for some states - `Z₀, Z₁` along a positive sequence `epsilon_n` tending to zero, then `X` is adiabatically - accessible to `Y`. Lieb-Yngvason: one cannot enlarge the set of accessible states "with an - infinitesimal grain of dust." -/ - A6_seq {ΓX ΓY ΓZ₀ ΓZ₁ : System} (X : State ΓX) (Y : State ΓY) - (Z₀ : State ΓZ₀) (Z₁ : State ΓZ₁) : - (∃ (ε_seq : ℕ → ℝ) (hpos : ∀ n, 0 < ε_seq n), - Filter.Tendsto ε_seq Filter.atTop (nhds 0) ∧ - (∀ n, - le - (state_of_comp_equiv.symm - (X, (state_of_scale_equiv (ne_of_gt (hpos n))).symm Z₀)) - (state_of_comp_equiv.symm - (Y, (state_of_scale_equiv (ne_of_gt (hpos n))).symm Z₁)))) → le X Y - - /-- Coherence of casting along an equality of systems: transporting a state along the - equality yields an adiabatically-equivalent state. This and the coherence fields below are - not Lieb-Yngvason axioms — they are needed only because Lean does not identify - propositionally-equal state spaces. -/ - state_equiv_coherence {Γ₁ Γ₂ : System} (h_sys : Γ₁ = Γ₂) (X : State Γ₁) : - le X (Equiv.cast (congrArg State h_sys) X) ∧ - le (Equiv.cast (congrArg State h_sys) X) X - /-- Coherence of composing with the zero system. -/ - comp_ZSystem_is_identity (Γ : System) (X : State Γ) : - le (state_of_comp_equiv.symm (X, State_ZSystem_is_Unit.default)) X ∧ - le X (state_of_comp_equiv.symm (X, State_ZSystem_is_Unit.default)) - /-- Coherence of successive scaling: `t` applied to `s` applied to `X` agrees with `(t * s)` - applied to `X`, up to adiabatic equivalence after the system cast. -/ - scale_coherence {t s : ℝ} (ht : t ≠ 0) (hs : s ≠ 0) {Γ : System} (X : State Γ) : - let X_s := (state_of_scale_equiv hs).symm X - let X_ts := (state_of_scale_equiv ht).symm X_s - let X_mul := (state_of_scale_equiv (mul_ne_zero ht hs)).symm X - let h_eq := smul_smul t s Γ - le (Equiv.cast (congrArg State h_eq) X_mul) X_ts ∧ - le X_ts (Equiv.cast (congrArg State h_eq) X_mul) - /-- Coherence of equal scaling factors. -/ - scale_eq_coherence {t₁ t₂ : ℝ} (h_eq : t₁ = t₂) (ht₁ : t₁ ≠ 0) {Γ : System} - (X : State Γ) : - let ht₂ : t₂ ≠ 0 := h_eq ▸ ht₁ - let X₁ := (state_of_scale_equiv ht₁).symm X - let X₂ := (state_of_scale_equiv ht₂).symm X - let h_sys_eq := congrArg (fun r => scale r Γ) h_eq - le (Equiv.cast (congrArg State h_sys_eq) X₁) X₂ ∧ - le X₂ (Equiv.cast (congrArg State h_sys_eq) X₁) - /-- Coherence of scaling by one. -/ - one_smul_coherence {Γ : System} (X : State Γ) : - let X_1 := (state_of_scale_equiv (show (1 : ℝ) ≠ 0 from one_ne_zero)).symm X - let h_eq := one_smul Γ - le (Equiv.cast (congrArg State h_eq) X_1) X ∧ - le X (Equiv.cast (congrArg State h_eq) X_1) - /-- Coherence of scaling a composed state. -/ - scale_comp_coherence {t : ℝ} (ht : t ≠ 0) {Γ₁ Γ₂ : System} - (X : State Γ₁) (Y : State Γ₂) : - let XY := state_of_comp_equiv.symm (X, Y) - let tXY := (state_of_scale_equiv ht).symm XY - let tX := (state_of_scale_equiv ht).symm X - let tY := (state_of_scale_equiv ht).symm Y - let tXtY := state_of_comp_equiv.symm (tX, tY) - let h_eq := scale_distrib_comp t Γ₁ Γ₂ - le (Equiv.cast (congrArg State h_eq) tXY) tXtY ∧ - le tXtY (Equiv.cast (congrArg State h_eq) tXY) - /-- Coherence of commutativity of composition. -/ - comp_comm_coherence {Γ₁ Γ₂ : System} (X : State Γ₁) (Y : State Γ₂) : - let XY := state_of_comp_equiv.symm (X, Y) - let YX := state_of_comp_equiv.symm (Y, X) - let h_eq := comp_comm Γ₁ Γ₂ - le (Equiv.cast (congrArg State h_eq.symm) YX) XY ∧ - le XY (Equiv.cast (congrArg State h_eq.symm) YX) - /-- Coherence of associativity of composition. -/ - comp_assoc_coherence {Γ₁ Γ₂ Γ₃ : System} (X : State Γ₁) (Y : State Γ₂) - (Z : State Γ₃) : - let XY := state_of_comp_equiv.symm (X, Y) - let XYZ_L := state_of_comp_equiv.symm (XY, Z) - let YZ := state_of_comp_equiv.symm (Y, Z) - let XYZ_R := state_of_comp_equiv.symm (X, YZ) - let h_eq := comp_assoc Γ₁ Γ₂ Γ₃ - le (Equiv.cast (congrArg State h_eq) XYZ_L) XYZ_R ∧ - le XYZ_R (Equiv.cast (congrArg State h_eq) XYZ_L) - -/-! ## C. Comparability - -Two states are *comparable* when at least one is accessible from the other; they are -*adiabatically equivalent* when each is. Lieb-Yngvason's **comparison hypothesis** (CH) -asserts that any two states of one state space are comparable. Crucially CH is a -*hypothesis*, not one of A1-A6: the paper's programme 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 rather than folding it into accessibility. -`GlobalComparisonHypothesis` is the compound-system strengthening. -/ - -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 - -/-- Two states are comparable if either is adiabatically accessible from the other, -`X ≺ Y ∨ Y ≺ X` (Lieb-Yngvason 1999, §II.A). -/ -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. -Stated as a hypothesis, not an axiom — Lieb-Yngvason derive it for simple systems rather than -assuming it (§II.C, §III-IV). -/ -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. This is named at A0 because later entropy constructions carry it as a separate -hypothesis rather than baking it into accessibility. -/ -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 - -/-! ## D. Core API - -Small consequences that need only `ThermoSystemCore`. -/ - -/-- 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 - -/-! ## E. World API - -Notation (`≺`, `≈`, `⊗`, `•`, `≺≺`) and the preorder lemmas exposing axioms A1 and A2 as -reflexivity and transitivity, plus a `Trans` instance so accessibility chains compose in -`calc` blocks. -/ - -section World - -variable {System : Type u} [TW : ThermoWorld System] - -local infix:50 " ≺ " => TW.le -local notation:50 X " ≈ " Y => X ≺ Y ∧ Y ≺ X -local infixr:70 " ⊗ " => TW.comp -local infixr:80 " • " => TW.scale -local infix:50 " ≺≺ " => StrictlyPrecedes (T := TW) - -/-- Reflexivity of adiabatic accessibility, exposed as a lemma from A1. -/ -lemma thermo_le_refl {Γ : System} (X : TW.State Γ) : X ≺ X := - TW.A1 X - -/-- Transitivity of adiabatic accessibility, exposed as a lemma from A2. -/ -lemma thermo_le_trans {Γ₁ Γ₂ Γ₃ : System} {X : TW.State Γ₁} {Y : TW.State Γ₂} - {Z : TW.State Γ₃} (hXY : X ≺ Y) (hYZ : Y ≺ Z) : X ≺ Z := - TW.A2 hXY hYZ - -/-- Adiabatic equivalence is reflexive. -/ -lemma thermo_equiv_refl {Γ : System} (X : TW.State Γ) : X ≈ X := - ⟨thermo_le_refl X, thermo_le_refl X⟩ - -/-- Adiabatic equivalence is symmetric. -/ -lemma thermo_equiv_symm {Γ₁ Γ₂ : System} {X : TW.State Γ₁} {Y : TW.State Γ₂} - (h : X ≈ Y) : Y ≈ X := - And.symm h - -/-- A `Trans` instance for calculations with adiabatic accessibility. -/ -instance calcTransThermoLe {Γ₁ Γ₂ Γ₃ : System} : - Trans (TW.le : TW.State Γ₁ → TW.State Γ₂ → Prop) - (TW.le : TW.State Γ₂ → TW.State Γ₃ → Prop) - (TW.le : TW.State Γ₁ → TW.State Γ₃ → Prop) where - trans := TW.A2 - -end World - -end Thermodynamics diff --git a/Physlib/Thermodynamics/Foundation/Comparability.lean b/Physlib/Thermodynamics/Foundation/Comparability.lean new file mode 100644 index 000000000..0b524319e --- /dev/null +++ b/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 diff --git a/Physlib/Thermodynamics/Foundation/Core.lean b/Physlib/Thermodynamics/Foundation/Core.lean new file mode 100644 index 000000000..0a0c6a679 --- /dev/null +++ b/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 diff --git a/Physlib/Thermodynamics/Foundation/Entropy.lean b/Physlib/Thermodynamics/Foundation/Entropy.lean index f74430b3f..bc845756a 100644 --- a/Physlib/Thermodynamics/Foundation/Entropy.lean +++ b/Physlib/Thermodynamics/Foundation/Entropy.lean @@ -5,7 +5,7 @@ Authors: Nathaneal Sajan -/ module -public import Physlib.Thermodynamics.Foundation.Accessibility +public import Physlib.Thermodynamics.Foundation.Comparability /-! # Entropy representations @@ -20,17 +20,18 @@ Lieb-Yngvason build such an `S` explicitly as `S(X) = sup {t | R_t ≺ X}`, wher `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 conditional on `Comparable`. This is faithful to -Lieb-Yngvason's eq. (2.3), which asserts the accessibility/entropy equivalence only for -comparable states, and to the design choice (see `Accessibility.lean`) that comparison -hypotheses are carried explicitly rather than baked into accessibility. +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 (Lieb-Yngvason eq. 2.6). + monotonicity. - `AffineUniqueness` — the statement (not a field, not proved here) that any two representations agree up to a positive affine recalibration `S ↦ aS + b`. @@ -44,9 +45,9 @@ hypotheses are carried explicitly rather than baked into accessibility. ## iv. References - E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of - Thermodynamics*, Physics Reports **310** (1999) 1-96. The entropy principle and its - properties (monotonicity, additivity, extensivity), §II.B, eqns (2.3)-(2.6); essential - uniqueness up to affine scale, §II.C; the canonical construction of `S`, §II.E. + 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 @@ -57,48 +58,54 @@ 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 +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, -letting `S` compare states across different systems. -/ +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 -An `EntropyRepresentation` is the Entropy Principle turned into a structure: a real-valued `S` -on `AllStates` that represents `≺` on comparable states (monotonicity), is additive under -composition, and is extensive under positive scaling. -/ - -/-- An abstract entropy representation of a thermodynamic core: the Lieb-Yngvason Entropy -Principle as a structure. A real-valued `S` on `AllStates` that represents adiabatic -accessibility on comparable states, is additive under composition, and is extensive under -positive scaling. -/ +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, Lieb-Yngvason eq. 2.3: 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: 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, Lieb-Yngvason eq. 2.4: `S(X, Y) = S(X) + S(Y)` across a composition. -/ + /-- 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, Lieb-Yngvason eq. 2.5: `S(t • X) = t · S(X)` for `t > 0`. -/ + /-- 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 -Immediate rephrasings of monotonicity: 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`. -/ +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 diff --git a/Physlib/Thermodynamics/Foundation/World.lean b/Physlib/Thermodynamics/Foundation/World.lean new file mode 100644 index 000000000..ac010ad34 --- /dev/null +++ b/Physlib/Thermodynamics/Foundation/World.lean @@ -0,0 +1,291 @@ +/- +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.Topology.Instances.Real.Lemmas +public import Physlib.Thermodynamics.Foundation.Comparability + +/-! +# Lieb-Yngvason worlds + +## i. Overview + +A `ThermoWorld` extends the operational core (`Core.lean`) with the assumptions +Lieb-Yngvason place on the adiabatic-accessibility relation `≺`. These fall into three +groups, each carried by its own class so it can be assumed or discharged independently: +`SystemAlgebra`, the algebraic identities making composition an associative, commutative +operation on which scaling acts compatibly; `AccessibilityAxioms`, the six accessibility +axioms A1-A6; and `CastCoherence`, the coherence axioms relating states across *equal* +systems. + +The coherence group has no Lieb-Yngvason axiom number. The paper treats identities like +`(Γ₁ ⊗ Γ₂) = (Γ₂ ⊗ Γ₁)` as strict equalities of state spaces and uses them silently, but +in Lean equal systems yield state spaces that are only propositionally equal. So each +identity is paired with a statement that transporting a state along it lands on an +adiabatically-equivalent state, a state `Y` with `X ≈ Y` (`X ≺ Y` and `Y ≺ X`). + +## ii. Key results + +- `SystemAlgebra` — the algebraic identities of composition and scaling. +- `AccessibilityAxioms` — the six accessibility axioms A1-A6 on `≺`. +- `CastCoherence` — the coherence-of-casts assumptions. +- `ThermoWorld` — the abstract interface bundling all three. +- `thermo_le_refl`, `thermo_le_trans`, `thermo_equiv_refl`, `thermo_equiv_symm`, + `calcTransThermoLe` — the preorder API exposing A1/A2 for calculation. +- `state_equiv_coherence`, `scale_eq_coherence` — cast-coherence facts derived from A1 + rather than assumed as fields. + +## iii. Table of contents + +- A. System algebra +- B. Accessibility axioms +- C. Coherence of casts +- D. Lieb-Yngvason worlds +- E. World 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. System algebra + +These identities of systems are used silently in informal treatments, where equal systems +are treated as literally the same. Each is paired with a coherence field in `CastCoherence` +below, which discharges the induced cast on state spaces. -/ + +/-- `SystemAlgebra` records the algebraic identities of the system constructors: composition +is associative and commutative, scaling distributes over it and composes multiplicatively, +scaling by one is trivial, and scaling by zero gives the zero system. -/ +class SystemAlgebra (System : Type u) extends ThermoSystemCore System where + /-- Scaling by zero gives the zero system. -/ + scale_zero_is_ZSystem (Γ : System) : scale 0 Γ = ZSystem + + /-- Composition of systems is associative, up to equality of systems. -/ + comp_assoc (Γ₁ Γ₂ Γ₃ : System) : comp (comp Γ₁ Γ₂) Γ₃ = comp Γ₁ (comp Γ₂ Γ₃) + /-- Composition of systems is commutative, up to equality of systems. -/ + comp_comm (Γ₁ Γ₂ : System) : comp Γ₁ Γ₂ = comp Γ₂ Γ₁ + /-- Scaling distributes over composition of systems. -/ + scale_distrib_comp (t : ℝ) (Γ₁ Γ₂ : System) : + scale t (comp Γ₁ Γ₂) = comp (scale t Γ₁) (scale t Γ₂) + /-- Successive scalings multiply their scale factors. -/ + smul_smul (t s : ℝ) (Γ : System) : scale (t * s) Γ = scale t (scale s Γ) + /-- Scaling by one leaves the system unchanged. -/ + one_smul (Γ : System) : scale 1 Γ = Γ + +/-! ## B. Accessibility axioms + +The fields `A1`-`A6` are reflexivity, transitivity, consistency, scaling invariance, +splitting/recombination (bidirectional, as `≈`), and stability (with an explicit +sequence); none is derivable from the others. + +Stability (A6) says accessibility cannot be manufactured from an infinitesimal side +effect: if `(X, εₙ • Z₀) ≺ (Y, εₙ • Z₁)` holds along some sequence `εₙ → 0`, for auxiliary +states `Z₀, Z₁`, then `X ≺ Y` outright, with no auxiliary system needed. It implies the +cancellation law by Theorem 2.1, which is what makes `≺` entropy-representable. -/ + +/-- `AccessibilityAxioms` bundles the six Lieb-Yngvason axioms A1-A6 on the +adiabatic-accessibility relation `≺`: reflexivity, transitivity, consistency, scaling +invariance, splitting/recombination, and stability. It assumes only the operational core. -/ +class AccessibilityAxioms (System : Type u) extends ThermoSystemCore System where + /-- A1, reflexivity: every state is accessible from itself, `X ≺ X`. -/ + A1 {Γ : System} (X : State Γ) : le X X + /-- A2, transitivity: `X ≺ Y` and `Y ≺ Z` give `X ≺ Z`. -/ + A2 {Γ₁ Γ₂ Γ₃ : System} {X : State Γ₁} {Y : State Γ₂} {Z : State Γ₃} : + le X Y → le Y Z → le X Z + /-- A3, consistency: accessibility is preserved by composition — + `X₁ ≺ Y₁` and `X₂ ≺ Y₂` give `(X₁, X₂) ≺ (Y₁, Y₂)`. -/ + A3 {Γ₁ Γ₂ Γ₃ Γ₄ : System} + {X₁ : State Γ₁} {X₂ : State Γ₂} {Y₁ : State Γ₃} {Y₂ : State Γ₄} : + le X₁ Y₁ → le X₂ Y₂ → + le (state_of_comp_equiv.symm (X₁, X₂)) (state_of_comp_equiv.symm (Y₁, Y₂)) + /-- A4, scaling invariance: if `X ≺ Y` then `t • X ≺ t • Y` for every `t > 0`. -/ + A4 {Γ₁ Γ₂ : System} {X : State Γ₁} {Y : State Γ₂} {t : ℝ} (ht : 0 < t) : + le X Y → le ((state_of_scale_equiv ht.ne.symm).symm X) + ((state_of_scale_equiv ht.ne.symm).symm Y) + /-- A5, splitting and recombination: for `0 < t < 1` a state is adiabatically equivalent + to its split into a `t`-copy and a `(1−t)`-copy, `X ≈ (t • X, (1−t) • X)`. -/ + A5 {Γ : System} (X : State Γ) {t : ℝ} (ht : 0 < t ∧ t < 1) : + le X + (state_of_comp_equiv.symm + (((state_of_scale_equiv ht.1.ne').symm X), + ((state_of_scale_equiv (t := 1 - t) (by + have hpos : 0 < 1 - t := sub_pos.mpr ht.2 + exact hpos.ne')).symm X))) ∧ + le (state_of_comp_equiv.symm + (((state_of_scale_equiv ht.1.ne').symm X), + ((state_of_scale_equiv (t := 1 - t) (by + have hpos : 0 < 1 - t := sub_pos.mpr ht.2 + exact hpos.ne')).symm X))) X + /-- A6, stability: accessibility cannot be created by an infinitesimal perturbation. + If `(X, epsilon_n Z₀)` is adiabatically accessible to `(Y, epsilon_n Z₁)` for some states + `Z₀, Z₁` along a positive sequence `epsilon_n` tending to zero, then `X` is adiabatically + accessible to `Y`. -/ + A6_seq {ΓX ΓY ΓZ₀ ΓZ₁ : System} (X : State ΓX) (Y : State ΓY) + (Z₀ : State ΓZ₀) (Z₁ : State ΓZ₁) : + (∃ (ε_seq : ℕ → ℝ) (hpos : ∀ n, 0 < ε_seq n), + Filter.Tendsto ε_seq Filter.atTop (nhds 0) ∧ + (∀ n, + le + (state_of_comp_equiv.symm + (X, (state_of_scale_equiv (ne_of_gt (hpos n))).symm Z₀)) + (state_of_comp_equiv.symm + (Y, (state_of_scale_equiv (ne_of_gt (hpos n))).symm Z₁)))) → le X Y + +/-! ## C. Coherence of casts + +Each coherence field relates two *different* constructions (distinct equiv applications, or +`(X, Y)` versus `(Y, X)`) and is not derivable from A1-A6. Every transport is phrased +against a `SystemAlgebra` identity — each `h_eq` is one of `smul_smul`, `one_smul`, +`scale_distrib_comp`, `comp_comm`, `comp_assoc` — which is why this class extends +`SystemAlgebra` rather than the bare core. The two coherence statements that *are* derivable +are provided instead as the lemmas `state_equiv_coherence` and `scale_eq_coherence`; +`comp_ZSystem_is_identity` is the only field making `ZSystem` a composition identity at the +state level. -/ + +/-- `CastCoherence` supplies the coherence assumptions relating states across *equal* systems: +transporting a state along a `SystemAlgebra` identity lands on an adiabatically-equivalent +state. -/ +class CastCoherence (System : Type u) extends SystemAlgebra System where + /-- Coherence of composing with the zero system: composing a state with the zero system's + unique state is adiabatically neutral. -/ + comp_ZSystem_is_identity (Γ : System) (X : State Γ) : + le (state_of_comp_equiv.symm (X, State_ZSystem_is_Unit.default)) X ∧ + le X (state_of_comp_equiv.symm (X, State_ZSystem_is_Unit.default)) + /-- Coherence of successive scaling: `t` applied to `s` applied to `X` agrees with `(t * s)` + applied to `X`, up to adiabatic equivalence after the system cast. -/ + scale_coherence {t s : ℝ} (ht : t ≠ 0) (hs : s ≠ 0) {Γ : System} (X : State Γ) : + let X_s := (state_of_scale_equiv hs).symm X + let X_ts := (state_of_scale_equiv ht).symm X_s + let X_mul := (state_of_scale_equiv (mul_ne_zero ht hs)).symm X + let h_eq := smul_smul t s Γ + le (Equiv.cast (congrArg State h_eq) X_mul) X_ts ∧ + le X_ts (Equiv.cast (congrArg State h_eq) X_mul) + /-- Coherence of scaling by one. -/ + one_smul_coherence {Γ : System} (X : State Γ) : + let X_1 := (state_of_scale_equiv (show (1 : ℝ) ≠ 0 from one_ne_zero)).symm X + let h_eq := one_smul Γ + le (Equiv.cast (congrArg State h_eq) X_1) X ∧ + le X (Equiv.cast (congrArg State h_eq) X_1) + /-- Coherence of scaling a composed state. -/ + scale_comp_coherence {t : ℝ} (ht : t ≠ 0) {Γ₁ Γ₂ : System} + (X : State Γ₁) (Y : State Γ₂) : + let XY := state_of_comp_equiv.symm (X, Y) + let tXY := (state_of_scale_equiv ht).symm XY + let tX := (state_of_scale_equiv ht).symm X + let tY := (state_of_scale_equiv ht).symm Y + let tXtY := state_of_comp_equiv.symm (tX, tY) + let h_eq := scale_distrib_comp t Γ₁ Γ₂ + le (Equiv.cast (congrArg State h_eq) tXY) tXtY ∧ + le tXtY (Equiv.cast (congrArg State h_eq) tXY) + /-- Coherence of commutativity of composition. -/ + comp_comm_coherence {Γ₁ Γ₂ : System} (X : State Γ₁) (Y : State Γ₂) : + let XY := state_of_comp_equiv.symm (X, Y) + let YX := state_of_comp_equiv.symm (Y, X) + let h_eq := comp_comm Γ₁ Γ₂ + le (Equiv.cast (congrArg State h_eq.symm) YX) XY ∧ + le XY (Equiv.cast (congrArg State h_eq.symm) YX) + /-- Coherence of associativity of composition. -/ + comp_assoc_coherence {Γ₁ Γ₂ Γ₃ : System} (X : State Γ₁) (Y : State Γ₂) + (Z : State Γ₃) : + let XY := state_of_comp_equiv.symm (X, Y) + let XYZ_L := state_of_comp_equiv.symm (XY, Z) + let YZ := state_of_comp_equiv.symm (Y, Z) + let XYZ_R := state_of_comp_equiv.symm (X, YZ) + let h_eq := comp_assoc Γ₁ Γ₂ Γ₃ + le (Equiv.cast (congrArg State h_eq) XYZ_L) XYZ_R ∧ + le XYZ_R (Equiv.cast (congrArg State h_eq) XYZ_L) + +/-! ## D. Lieb-Yngvason worlds + +`ThermoWorld` combines the three assumption groups into the single abstract interface used +throughout the development. Every field, `A1`-`A6`, the algebra identities, and the +coherence fields are then available on an instance by plain dot notation. -/ + +/-- `ThermoWorld` is the abstract Lieb-Yngvason interface, bundling the accessibility axioms +(`AccessibilityAxioms`) with the cast-coherence layer (`CastCoherence`, which carries the +`SystemAlgebra` identities). -/ +class ThermoWorld (System : Type u) extends + AccessibilityAxioms System, CastCoherence System + +/-! ## E. World API + +Notation (`≺`, `≈`, `⊗`, `•`, `≺≺`) and the preorder lemmas exposing axioms A1 and A2 as +reflexivity and transitivity, plus a `Trans` instance so accessibility chains compose in +`calc` blocks. The section also proves the two cast-coherence statements that need no axiom +of their own: `state_equiv_coherence` and `scale_eq_coherence` each relate a state to its +own transport along a `subst`-able equality, so A1 suffices. -/ + +section World + +variable {System : Type u} [TW : ThermoWorld System] + +local infix:50 " ≺ " => TW.le +local notation:50 X " ≈ " Y => X ≺ Y ∧ Y ≺ X +local infixr:70 " ⊗ " => TW.comp +local infixr:80 " • " => TW.scale +local infix:50 " ≺≺ " => StrictlyPrecedes (T := TW) + +/-- Reflexivity of adiabatic accessibility, exposed as a lemma from A1. -/ +lemma thermo_le_refl {Γ : System} (X : TW.State Γ) : X ≺ X := + TW.A1 X + +/-- Transitivity of adiabatic accessibility, exposed as a lemma from A2. -/ +lemma thermo_le_trans {Γ₁ Γ₂ Γ₃ : System} {X : TW.State Γ₁} {Y : TW.State Γ₂} + {Z : TW.State Γ₃} (hXY : X ≺ Y) (hYZ : Y ≺ Z) : X ≺ Z := + TW.A2 hXY hYZ + +/-- Adiabatic equivalence is reflexive. -/ +lemma thermo_equiv_refl {Γ : System} (X : TW.State Γ) : X ≈ X := + ⟨thermo_le_refl X, thermo_le_refl X⟩ + +/-- Adiabatic equivalence is symmetric. -/ +lemma thermo_equiv_symm {Γ₁ Γ₂ : System} {X : TW.State Γ₁} {Y : TW.State Γ₂} + (h : X ≈ Y) : Y ≈ X := + And.symm h + +/-- A `Trans` instance for calculations with adiabatic accessibility. -/ +instance calcTransThermoLe {Γ₁ Γ₂ Γ₃ : System} : + Trans (TW.le : TW.State Γ₁ → TW.State Γ₂ → Prop) + (TW.le : TW.State Γ₂ → TW.State Γ₃ → Prop) + (TW.le : TW.State Γ₁ → TW.State Γ₃ → Prop) where + trans := TW.A2 + +/-- Coherence of casting along an equality of systems: transporting a state along the +equality yields an adiabatically-equivalent state. Derivable from A1: substituting the +equality reduces the cast to the identity. -/ +lemma state_equiv_coherence {Γ₁ Γ₂ : System} (h_sys : Γ₁ = Γ₂) (X : TW.State Γ₁) : + TW.le X (Equiv.cast (congrArg TW.State h_sys) X) ∧ + TW.le (Equiv.cast (congrArg TW.State h_sys) X) X := by + subst h_sys + exact ⟨TW.A1 X, TW.A1 X⟩ + +/-- Coherence of equal scaling factors: equal factors give the same scaled state up to a +cast along the induced equality of systems. Derivable from A1: substituting `t₁ = t₂` +reduces the cast to the identity. -/ +lemma scale_eq_coherence {t₁ t₂ : ℝ} (h_eq : t₁ = t₂) (ht₁ : t₁ ≠ 0) {Γ : System} + (X : TW.State Γ) : + let ht₂ : t₂ ≠ 0 := h_eq ▸ ht₁ + let X₁ := (TW.state_of_scale_equiv ht₁).symm X + let X₂ := (TW.state_of_scale_equiv ht₂).symm X + let h_sys_eq := congrArg (fun r => TW.scale r Γ) h_eq + TW.le (Equiv.cast (congrArg TW.State h_sys_eq) X₁) X₂ ∧ + TW.le X₂ (Equiv.cast (congrArg TW.State h_sys_eq) X₁) := by + subst h_eq + exact ⟨TW.A1 _, TW.A1 _⟩ + +end World + +end Thermodynamics diff --git a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean index 6f71d611a..d776874fa 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Basic.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Basic.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Calculus.ContDiff.Basic public import Mathlib.Analysis.Calculus.Deriv.MeanValue +public import Physlib.Thermodynamics.FundamentalRelation.ExtensiveState /-! # The fundamental relation of a simple thermodynamic system @@ -14,41 +15,31 @@ public import Mathlib.Analysis.Calculus.Deriv.MeanValue ## i. Overview In the entropy representation, all thermodynamic information about a simple system is -contained in its **fundamental relation** `S = S(U, V, N)`, the entropy as a -function of the extensive parameters internal energy `U`, volume `V`, and particle number `N`. - -Design choices: -- **`S` is kept total** (`ℝ → ℝ → ℝ → ℝ`); positivity is carried by field hypotheses and by - `ExtensiveState`. -- **The domain of regularity is the positive orthant** (`posOrthant` / `ExtensiveState`); `S` is - not assumed regular where a coordinate vanishes. -- **`StrictMonoOn` in `U` is derived**, not a field: `dS_dU_pos` (pointwise `∂S/∂U > 0`) is the - primitive, and `strictMonoOn_U` follows from it. - -This file records the assumptions used by the current entropy-representation layer: -degree-one homogeneity (`homogeneous`), smoothness on the positive orthant (`smooth`), and -positive energy derivative (`dS_dU_pos`, equivalently `T > 0`). These are bundled in -`FundamentalRelation`. Stability, concavity, and third-law behavior are not fields of this -structure. +contained in its **fundamental relation** `S = S(U, V, N)`, the entropy as a function of the +extensive parameters internal energy `U`, volume `V`, and particle number `N`. The +`FundamentalRelation` structure bundles that surface with three assumptions: smoothness on +the positive orthant (`smooth`), a positive energy derivative (`dS_dU_pos`, equivalently +`T > 0`), and degree-one homogeneity (`homogeneous`). The entropy `S` is kept total +(`ℝ → ℝ → ℝ → ℝ`), 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. ## ii. Key results -- `ExtensiveState` — a positive extensive state `(U, V, N)`, the physical coordinate domain. -- `posOrthant` — the open positive orthant of `ℝ × ℝ × ℝ` on which a relation is regular. -- `FundamentalRelation` — the smooth entropy surface `S(U, V, N)` with its three fields. -- `FundamentalRelation.strictMonoOn_U` — entropy is strictly increasing in `U` (derived from +- `FundamentalRelation` - the smooth entropy surface `S(U, V, N)` with its three fields. +- `FundamentalRelation.strictMonoOn_U` - entropy is strictly increasing in `U` (derived from `dS_dU_pos`). ## iii. Table of contents -- A. Extensive states and the coordinate domain -- B. The fundamental relation -- C. Derived monotonicity in energy +- A. The fundamental relation +- B. Derived monotonicity in energy ## iv. References -- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley (1985). --/ +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley + (1985). -/ @[expose] public section @@ -56,47 +47,18 @@ namespace Thermodynamics open scoped ContDiff -/-! ## A. Extensive states and the coordinate domain - -A `FundamentalRelation` is regular only on physically admissible states — those with strictly -positive `U`, `V`, `N`. We carry that positivity in two ways: `ExtensiveState` for the physical -states the later bridge maps to abstract states, and `posOrthant` for the open set on which -smoothness and the energy derivative are asserted. Keeping positivity here, rather than in the -type of `S`, lets the calculus treat `S` as an ordinary total function. -/ - -/-- A positive **extensive state** `(U, V, N)` of a simple system: internal energy, -volume and particle number, all strictly positive. This is the physical domain over -which a `FundamentalRelation` is smooth, homogeneous, and monotone. -/ -structure ExtensiveState where - /-- Internal energy. -/ - U : ℝ - /-- Volume. -/ - V : ℝ - /-- Particle number. -/ - N : ℝ - /-- Positivity of the internal energy. -/ - hU : 0 < U - /-- Positivity of the volume. -/ - hV : 0 < V - /-- Positivity of the particle number. -/ - hN : 0 < N - -/-- The positive orthant of `ℝ × ℝ × ℝ` — the coordinate domain on which a -`FundamentalRelation` is regular. -/ -def posOrthant : Set (ℝ × ℝ × ℝ) := {p | 0 < p.1 ∧ 0 < p.2.1 ∧ 0 < p.2.2} - -/-! ## B. The fundamental relation - -The structure bundles the entropy surface `S` with Postulate III: it is C^∞ (`smooth`), -has positive energy derivative (`dS_dU_pos`, giving `T > 0`), and is homogeneous of degree one -(`homogeneous`, i.e. extensivity). Concavity/stability (Postulate II) is deferred. -/ +/-! ## A. The fundamental relation + +The structure bundles the entropy surface `S` with the three properties of Postulate III: +continuity and differentiability (`smooth`), monotonicity in the energy (`dS_dU_pos`, i.e. +`∂S/∂U = 1/T > 0`), and degree-one homogeneity (`homogeneous`). The `smooth` field is taken +as C^∞, stronger than the continuity and differentiability the postulate states. -/ /-- A **fundamental relation** in the entropy representation: a total entropy function -`S(U, V, N)` that is C^∞, has positive energy derivative, and is homogeneous of degree one on the -positive orthant. -/ +`S(U, V, N)` that is C^∞ on the positive orthant, has positive energy derivative +(`dS_dU_pos`), and is homogeneous of degree one (`homogeneous`). -/ structure FundamentalRelation where - /-- The entropy as a total function of `(U, V, N)`. Positivity is imposed by the field - hypotheses below, not by the type of `S`. -/ + /-- The entropy as a total function of `(U, V, N)`. -/ S : ℝ → ℝ → ℝ → ℝ /-- Regularity: `S` is C^∞ on the positive orthant. -/ smooth : ContDiffOn ℝ ∞ (fun p : ℝ × ℝ × ℝ => S p.1 p.2.1 p.2.2) posOrthant @@ -104,11 +66,11 @@ structure FundamentalRelation where `1 / T > 0` pointwise. This yields positive temperature without invoking concavity. -/ dS_dU_pos : ∀ U V N, 0 < U → 0 < V → 0 < N → 0 < deriv (fun u => S u V N) U /-- Extensivity: `S` is homogeneous of degree one on the positive orthant, - `S(lU, lV, lN) = l · S(U, V, N)` for `l > 0` (Callen's extensivity of the entropy). -/ + `S(lU, lV, lN) = l · S(U, V, N)` for `l > 0` (extensivity of the entropy). -/ homogeneous : ∀ ⦃l : ℝ⦄, 0 < l → ∀ U V N, 0 < U → 0 < V → 0 < N → S (l * U) (l * V) (l * N) = l * S U V N -/-! ## C. Derived monotonicity in energy +/-! ## B. Derived monotonicity in energy Strict monotonicity of entropy in `U` is derived from the pointwise `dS_dU_pos` via `strictMonoOn_of_deriv_pos`, and `T > 0` is a consequence. -/ diff --git a/Physlib/Thermodynamics/FundamentalRelation/ExtensiveState.lean b/Physlib/Thermodynamics/FundamentalRelation/ExtensiveState.lean new file mode 100644 index 000000000..404996370 --- /dev/null +++ b/Physlib/Thermodynamics/FundamentalRelation/ExtensiveState.lean @@ -0,0 +1,132 @@ +/- +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 + +/-! +# Extensive states of a simple thermodynamic system + +## i. Overview + +An **extensive state** of a single-component simple system is a triple `(U, V, N)` of +internal energy, volume, and particle number, all strictly positive. This module defines the +coordinate domain `posOrthant`, the state type `ExtensiveState` as the subtype of +`ℝ × ℝ × ℝ` cut out by it, and the accessors and constructor used by the rest of the +fundamental-relation development. + +## ii. Key results + +- `posOrthant` - the open positive orthant of `ℝ × ℝ × ℝ`, the coordinate domain on which a + fundamental relation is regular. +- `ExtensiveState` - a positive extensive state `(U, V, N)`, as a subtype of `posOrthant`. +- `ExtensiveState.U`/`V`/`N`, `hU`/`hV`/`hN`, `mem_posOrthant` - the read API of coordinate + accessors, their positivity, and membership in the coordinate domain. +- `ExtensiveState.mk`, `ExtensiveState.ext` - constructor from coordinates with positivity + proofs, and extensionality from the three coordinates alone. + +## iii. Table of contents + +- A. The coordinate domain +- B. Extensive states +- C. Accessors and constructor +- D. Extensionality + +## iv. References + +- H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley + (1985). -/ + +@[expose] public section + +namespace Thermodynamics + +/-! ## A. The coordinate domain + +The calculus in `Intensive.lean` (`ContDiffOn`, `fderivWithin`, `IsOpen.mem_nhds`) +predicates over a *set* in the normed space `ℝ × ℝ × ℝ`, so the regularity domain must be +carried as such a set; smoothness cannot be stated "over `ExtensiveState`" directly. The set +is open because differentiability at a state needs a neighborhood inside the domain, and the +inequalities are strict because the entropy formulas divide by and take logs of the +coordinates. -/ + +/-- The open positive orthant of `ℝ × ℝ × ℝ`, the coordinate domain on which a +`FundamentalRelation` is regular. -/ +def posOrthant : Set (ℝ × ℝ × ℝ) := {p | 0 < p.1 ∧ 0 < p.2.1 ∧ 0 < p.2.2} + +/-! ## B. Extensive states + +The three coordinates completely characterize an equilibrium state of a simple system +(Postulate I) and are mutually independent, no coordinate being a function of the other two. +The state type is the subtype of `ℝ × ℝ × ℝ` cut out by `posOrthant`, so a state's positivity +is its membership in the coordinate domain. -/ + +/-- 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} + +namespace ExtensiveState + +/-! ## C. Accessors and constructor + +Thin accessors give the coordinate read API. Here `e.U` reduces definitionally, and `e.hU` +derives positivity from the subtype property. -/ + +/-- The internal energy of an extensive state. -/ +def U (e : ExtensiveState) : ℝ := e.1.1 + +/-- The volume of an extensive state. -/ +def V (e : ExtensiveState) : ℝ := e.1.2.1 + +/-- The particle number of an extensive state. -/ +def N (e : ExtensiveState) : ℝ := e.1.2.2 + +/-- Positivity of the internal energy, from the subtype property. -/ +lemma hU (e : ExtensiveState) : 0 < e.U := e.2.1 + +/-- Positivity of the volume, from the subtype property. -/ +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 + +/-- An extensive state's coordinates lie in the positive orthant. This is the subtype +property itself. -/ +lemma mem_posOrthant (e : ExtensiveState) : (e.U, e.V, e.N) ∈ posOrthant := e.2 + +/-- Construct an extensive state from its coordinates and their positivity. -/ +def mk (U V N : ℝ) (hU : 0 < U) (hV : 0 < V) (hN : 0 < N) : ExtensiveState := + ⟨(U, V, N), hU, hV, hN⟩ + +/-- The energy coordinate of a state built by `mk`. -/ +@[simp] lemma U_mk (U V N : ℝ) (hU : 0 < U) (hV : 0 < V) (hN : 0 < N) : + (mk U V N hU hV hN).U = U := rfl + +/-- The volume coordinate of a state built by `mk`. -/ +@[simp] lemma V_mk (U V N : ℝ) (hU : 0 < U) (hV : 0 < V) (hN : 0 < N) : + (mk U V N hU hV hN).V = V := rfl + +/-- The particle-number coordinate of a state built by `mk`. -/ +@[simp] lemma N_mk (U V N : ℝ) (hU : 0 < U) (hV : 0 < V) (hN : 0 < N) : + (mk U V N hU hV hN).N = N := rfl + +/-! ## D. Extensionality + +Extensionality needs only the three coordinates, since the positivity proof is +proof-irrelevant. -/ + +/-- Two extensive states with the same coordinates are equal, so `(U, V, N)` alone determine +the state. -/ +@[ext] lemma ext {e₁ e₂ : ExtensiveState} + (hU : e₁.U = e₂.U) (hV : e₁.V = e₂.V) (hN : e₁.N = e₂.N) : e₁ = e₂ := by + apply Subtype.ext + exact Prod.ext hU (Prod.ext hV hN) + +end ExtensiveState + +end Thermodynamics diff --git a/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean b/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean index 31ab43b86..c14a5f589 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Intensive.lean @@ -16,25 +16,9 @@ public import Physlib.Thermodynamics.FundamentalRelation.Basic In the entropy representation, a simple system is described by a fundamental relation `S = S(U, V, N)`, where `U` is internal energy, `V` is volume, and `N` is particle number. -The intensive parameters are obtained from the entropy differential - -`dS = (1 / T) dU + (P / T) dV - (μ / T) dN`. - -For a `FundamentalRelation Φ`, this file names the three coordinate derivatives -`∂S/∂U`, `∂S/∂V`, and `∂S/∂N`, defines the corresponding temperature, pressure, and chemical -potential, and proves `T > 0` from the assumed positivity of `∂S/∂U`. - -The differentiability lemmas connect the joint smoothness hypothesis on `S(U, V, N)` to the -one-coordinate derivative statements used by these definitions. The total derivative lemma -then identifies the Fréchet derivative of `S` with the expected linear expression in the -three entropy partials. - -The final theorem is a determination result for fundamental relations. If two fundamental -relations have the same `U` and `V` entropy partials and agree at one positive reference -state, then their residual vanishes everywhere on the positive orthant. Thus the two entropy -functions agree exactly on positive extensive states. The theorem is useful when a later -model identifies the equations of state first and then needs equality of the whole -fundamental relation. +For a `FundamentalRelation Φ`, this file names the three coordinate entropy partials, defines +the intensive parameters temperature, pressure, and chemical potential, identifies the total +derivative of `S`, and proves a determination result for fundamental relations. ## ii. Key results @@ -59,8 +43,7 @@ fundamental relation. ## iv. References - H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley - (1985). --/ + (1985). -/ @[expose] public section @@ -72,9 +55,10 @@ noncomputable section /-! ## A. Entropy partial derivatives -The coordinate partials of the fundamental relation are defined by fixing two extensive -coordinates and differentiating with respect to the third. These are ordinary one-variable -`deriv`s evaluated at a positive `ExtensiveState`. -/ +For a `FundamentalRelation Φ`, this section names the three coordinate derivatives `∂S/∂U`, +`∂S/∂V`, and `∂S/∂N`. The coordinate partials of the fundamental relation are defined by +fixing two extensive coordinates and differentiating with respect to the third. These are +ordinary one-variable `deriv`s evaluated at a positive `ExtensiveState`. -/ /-- The energy partial derivative `∂S/∂U` at a positive extensive state. @@ -96,12 +80,18 @@ def FundamentalRelation.dS_dN (Φ : FundamentalRelation) (e : ExtensiveState) : /-! ## B. Intensive parameters -The intensive parameters are recovered from the entropy partials by solving +The intensive parameters are obtained from the entropy differential + +`dS = (1 / T) dU + (P / T) dV - (μ / T) dN`. + +They are recovered from the entropy partials by solving `∂S/∂U = 1 / T`, `∂S/∂V = P / T`, and `∂S/∂N = -μ / T`. -The definitions here are real-valued coordinate functions on positive extensive states; no -particular equation of state is assumed. -/ +This section defines the corresponding temperature, pressure, and chemical potential, and +proves `T > 0` from the assumed positivity of `∂S/∂U`. The definitions here are real-valued +coordinate functions on positive extensive states; no particular equation of state is +assumed. -/ /-- Temperature as the reciprocal of the energy derivative of entropy: `T = (∂S/∂U)⁻¹`. -/ @@ -154,7 +144,7 @@ lemma FundamentalRelation.differentiableAt_slice_U (Φ : FundamentalRelation) DifferentiableAt ℝ (fun u => Φ.S u e.V e.N) e.U := by change DifferentiableAt ℝ ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ fun u : ℝ => (u, (e.V, e.N))) e.U - have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hmem : (e.U, e.V, e.N) ∈ posOrthant := e.mem_posOrthant have hjoint : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N) := (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) @@ -169,7 +159,7 @@ lemma FundamentalRelation.differentiableAt_slice_V (Φ : FundamentalRelation) DifferentiableAt ℝ (fun v => Φ.S e.U v e.N) e.V := by change DifferentiableAt ℝ ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ fun v : ℝ => (e.U, (v, e.N))) e.V - have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hmem : (e.U, e.V, e.N) ∈ posOrthant := e.mem_posOrthant have hjoint : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N) := (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) @@ -184,7 +174,7 @@ lemma FundamentalRelation.differentiableAt_slice_N (Φ : FundamentalRelation) DifferentiableAt ℝ (fun n => Φ.S e.U e.V n) e.N := by change DifferentiableAt ℝ ((fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) ∘ fun n : ℝ => (e.U, (e.V, n))) e.N - have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hmem : (e.U, e.V, e.N) ∈ posOrthant := e.mem_posOrthant have hjoint : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N) := (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) @@ -215,7 +205,7 @@ lemma FundamentalRelation.hasFDerivAt_joint (Φ : FundamentalRelation) (e : Exte HasFDerivAt (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (fderiv ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N)) (e.U, e.V, e.N) := by - have hmem : (e.U, e.V, e.N) ∈ posOrthant := ⟨e.hU, e.hV, e.hN⟩ + have hmem : (e.U, e.V, e.N) ∈ posOrthant := e.mem_posOrthant have hdiff : DifferentiableAt ℝ (fun p : ℝ × ℝ × ℝ => Φ.S p.1 p.2.1 p.2.2) (e.U, e.V, e.N) := (Φ.smooth.contDiffAt (isOpen_posOrthant.mem_nhds hmem)).differentiableAt (by norm_num) @@ -312,7 +302,7 @@ lemma FundamentalRelation.eq_of_dS_dU_dS_dV_eq_of_eq_at ∀ {U V N : ℝ}, 0 < U → 0 < V → 0 < N → HasDerivAt (fun u => sResidual u V N) 0 U := by intro U V N hUpos hVpos hNpos - let e : ExtensiveState := ⟨U, V, N, hUpos, hVpos, hNpos⟩ + let e : ExtensiveState := ExtensiveState.mk U V N hUpos hVpos hNpos have hΦ := Φ.hasDerivAt_dS_dU e have hΨ := Ψ.hasDerivAt_dS_dU e have hres : HasDerivAt ((fun u => Φ.S u V N) - fun u => Ψ.S u V N) @@ -330,7 +320,7 @@ lemma FundamentalRelation.eq_of_dS_dU_dS_dV_eq_of_eq_at ∀ {U V N : ℝ}, 0 < U → 0 < V → 0 < N → HasDerivAt (fun v => sResidual U v N) 0 V := by intro U V N hUpos hVpos hNpos - let e : ExtensiveState := ⟨U, V, N, hUpos, hVpos, hNpos⟩ + let e : ExtensiveState := ExtensiveState.mk U V N hUpos hVpos hNpos have hΦ := Φ.hasDerivAt_dS_dV e have hΨ := Ψ.hasDerivAt_dS_dV e have hres : HasDerivAt ((fun v => Φ.S U v N) - fun v => Ψ.S U v N) diff --git a/Physlib/Thermodynamics/FundamentalRelation/Model.lean b/Physlib/Thermodynamics/FundamentalRelation/Model.lean index 77c686047..be8accf2b 100644 --- a/Physlib/Thermodynamics/FundamentalRelation/Model.lean +++ b/Physlib/Thermodynamics/FundamentalRelation/Model.lean @@ -17,12 +17,12 @@ A `ThermoModel Φ` is a model of a smooth coordinate fundamental relation `Φ` (Callen's `S = S(U, V, N)`) as a concrete abstract thermodynamic core. It supplies a single system `Γ`, a map `stateOf` from positive extensive states into the abstract state space, an entropy representation, and two linking -hypotheses — `entropy_agrees` (the coordinate entropy equals the abstract entropy on mapped +hypotheses - `entropy_agrees` (the coordinate entropy equals the abstract entropy on mapped states) and `comparison` (the Lieb-Yngvason Comparison Hypothesis on `Γ`). From these we *derive* the **Entropy Principle** for the model via `entropyPrinciple`: on mapped -states, Callen's entropy order coincides with adiabatic accessibility, -`Φ.S e₁ ≤ Φ.S e₂ ↔ stateOf e₁ ≺ stateOf e₂` . +states, the coordinate entropy order coincides with adiabatic accessibility, +`Φ.S e₁ ≤ Φ.S e₂ ↔ stateOf e₁ ≺ stateOf e₂`. ## ii. Key results @@ -34,16 +34,14 @@ states, Callen's entropy order coincides with adiabatic accessibility, ## iii. Table of contents - A. The model -- B. The entropy principle (derived) +- B. The entropy principle ## iv. References - E.H. Lieb and J. Yngvason, *The Physics and Mathematics of the Second Law of - Thermodynamics*, Physics Reports **310** (1999) 1-96. The Entropy Principle (monotonicity), - §II.B eq. (2.3); the Comparison Hypothesis as a hypothesis, §II; proved for simple systems, - §III-IV. + Thermodynamics*, Physics Reports **310** (1999). - H.B. Callen, *Thermodynamics and an Introduction to Thermostatistics*, 2nd ed., Wiley - (1985). The fundamental relation `S = S(U, V, N)`, §1.10. + (1985). -/ @[expose] public section @@ -54,22 +52,20 @@ universe u /-! ## A. The model -`ThermoModel Φ` exhibits the smooth fundamental relation `Φ` as a model of the abstract -interface. It maps only positive extensive states into one abstract system `Γ`, identifies -the two entropies there (`entropy_agrees`), and assumes the Comparison Hypothesis on `Γ` -(`comparison`). -/ +`ThermoModel Φ` links the smooth coordinate fundamental relation `Φ` to the abstract +accessibility-and-entropy interface. It bundles a thermodynamic core with a distinguished +system `Γ` and an entropy representation, a map `stateOf` from positive extensive states +into `Γ`, and two hypotheses relating the two descriptions. One, `entropy_agrees`, says that +`Φ.S` equals the abstract entropy of the mapped state, and the other, `comparison`, is the +Comparison Hypothesis on `Γ`. From these, `entropyPrinciple` identifies the coordinate +entropy order with adiabatic accessibility on mapped states. -/ /-- A model of the smooth coordinate fundamental relation `Φ` inside the abstract -accessibility-and-entropy interface. - -The bundled `core` is only a `ThermoSystemCore`, so this bridge needs no `ThermoWorld`. -`stateOf` maps positive extensive states into a single abstract system `Γ`; `entropy_agrees` -identifies the coordinate and abstract entropies there; and `comparison` is the Lieb-Yngvason -Comparison Hypothesis on `Γ`. -/ +accessibility-and-entropy interface. -/ structure ThermoModel (Φ : FundamentalRelation) where /-- The abstract type of thermodynamic systems used by this model. -/ {System : Type u} - /-- The operational thermodynamic core. No Lieb-Yngvason axioms are required by the bridge. -/ + /-- The operational thermodynamic core. -/ core : ThermoSystemCore System /-- The single abstract system the coordinate states map into. -/ Γ : System @@ -82,21 +78,20 @@ structure ThermoModel (Φ : FundamentalRelation) where `Φ.S e = entropy.S ⟨Γ, stateOf e⟩`. Equivalently, `stateOf` is entropy-preserving. -/ entropy_agrees : ∀ e : ExtensiveState, Φ.S e.U e.V e.N = entropy.S ⟨Γ, stateOf e⟩ - /-- The Lieb-Yngvason Comparison Hypothesis on the system `Γ`: any two states of `Γ` are - adiabatically comparable. -/ + /-- The Comparison Hypothesis on the system `Γ`: any two states of `Γ` are adiabatically + comparable. -/ comparison : ComparisonHypothesis (T := core) Γ namespace ThermoModel /-! ## B. The entropy principle -The Entropy Principle for the model is a theorem, obtained by discharging the entropy -representation's conditional monotonicity with the Comparison Hypothesis. -/ +This section states the Entropy Principle for the model. On states in the image of +`stateOf`, the order given by the coordinate entropy `Φ.S` coincides with adiabatic +accessibility in the core. -/ -/-- The **Entropy Principle** for the model: on mapped states, Callen's coordinate-entropy order -coincides with primitive adiabatic accessibility, `Φ.S e₁ ≤ Φ.S e₂ ↔ stateOf e₁ ≺ stateOf e₂`. -This is the entropy representation's conditional `Monotonicity` (valid on comparable states) -discharged everywhere on `Γ` by `comparison`. -/ +/-- The **Entropy Principle** for the model. On mapped states, the coordinate-entropy order +coincides with adiabatic accessibility, `Φ.S e₁ ≤ Φ.S e₂ ↔ stateOf e₁ ≺ stateOf e₂`. -/ lemma entropyPrinciple {Φ : FundamentalRelation} (M : ThermoModel Φ) (e₁ e₂ : ExtensiveState) : (Φ.S e₁.U e₁.V e₁.N ≤ Φ.S e₂.U e₂.V e₂.N) ↔ M.core.le (M.stateOf e₁) (M.stateOf e₂) := by