thermodynamicPotentialCount
plain-language theorem explainer
The declaration establishes that the set of thermodynamic potentials has cardinality five, matching the configuration dimension in Recognition Science thermochemistry. Researchers assembling equilibrium certificates from the J-cost minimum would cite this count when populating the ThermochemistryCert structure. The proof is a one-line decide tactic that computes the cardinality from the derived Fintype instance on the inductive type.
Claim. The set of thermodynamic potentials has cardinality five, where the potentials are internal energy $U$, enthalpy $H$, Helmholtz free energy $F$, Gibbs free energy $G$, and grand potential $Ω$.
background
The ThermochemistryFromRS module defines ThermodynamicPotential as an inductive type with five constructors corresponding to the canonical potentials. The module states that these five potentials equal configDim D=5, with RS equilibrium identified as the state where J=0 (free energy minimum) and non-equilibrium states requiring J>0. The upstream equilibrium theorem from NonlinearDynamicsFromRS states that Jcost 1 = 0, supplying the J-cost foundation for the chemical equilibrium claim.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. Because ThermodynamicPotential derives DecidableEq, Repr, BEq, and Fintype, the tactic reduces the cardinality equality to finite enumeration of the five constructors and verifies it by decidable computation.
why it matters
This theorem supplies the five_potentials field inside the downstream thermochemistryCert definition, which assembles the full certificate including equilibrium and nonequilibrium cost components. It implements the module claim that five potentials equal configDim D=5 and ties directly to the Recognition Science equilibrium condition J=0. The result closes the thermochemistry scaffolding with zero sorry and no open hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.