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