IndisputableMonolith.Physics.ThermochemistryFromRS

   1import Mathlib
   2import IndisputableMonolith.Cost
   3
   4/-!
   5# Thermochemistry from RS — A1 Chemistry/Physics
   6
   7Five canonical thermodynamic potentials (internal energy U, enthalpy H,
   8Helmholtz free energy F, Gibbs free energy G, grand potential Ω)
   9= configDim D = 5.
  10
  11RS: equilibrium chemical state = J = 0 (free energy minimum).
  12Non-equilibrium: J > 0 (work needed to equilibrate).
  13
  14Lean: 5 potentials.
  15
  16Lean status: 0 sorry, 0 axiom.
  17-/
  18
  19namespace IndisputableMonolith.Physics.ThermochemistryFromRS
  20open Cost
  21
  22inductive ThermodynamicPotential where
  23  | internalEnergy | enthalpy | helmholtz | gibbs | grandPotential
  24  deriving DecidableEq, Repr, BEq, Fintype
  25
  26theorem thermodynamicPotentialCount : Fintype.card ThermodynamicPotential = 5 := by decide
  27
  28/-- Chemical equilibrium: J = 0. -/
  29theorem chemical_equilibrium : Jcost 1 = 0 := Jcost_unit0
  30
  31/-- Non-equilibrium: J > 0. -/
  32theorem nonequilibrium_cost {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  33    0 < Jcost r := Jcost_pos_of_ne_one r hr hne
  34
  35structure ThermochemistryCert where
  36  five_potentials : Fintype.card ThermodynamicPotential = 5
  37  equilibrium : Jcost 1 = 0
  38  nonequil : ∀ {r : ℝ}, 0 < r → r ≠ 1 → 0 < Jcost r
  39
  40def thermochemistryCert : ThermochemistryCert where
  41  five_potentials := thermodynamicPotentialCount
  42  equilibrium := chemical_equilibrium
  43  nonequil := nonequilibrium_cost
  44
  45end IndisputableMonolith.Physics.ThermochemistryFromRS
  46