23.3. The energy family: distinguishing kinds by defining construction
ISO 80000-5 item 5-20 lists energy <thermodynamics> (5-20.1) as a genus and the
thermodynamic potentials — internal energy (5-20.2), enthalpy (5-20.3), the Helmholtz
energy (5-20.4), and the Gibbs energy (5-20.5) — as items beneath it. Every one has
dimension M·L²·T⁻² and ratio scale. The standard distinguishes them only in prose, by
which thermodynamic variables are natural to the potential: internal energy is a state
function of S, V, N; the enthalpy is H = U + pV; the Helmholtz energy is A = U − TS;
the Gibbs energy is G = H − TS. A dimension-only model sees one type, "a real number of
joules", for all of them — and cannot even separate them from a Part-4 torque.
This is requirement R2 again, now on the thermodynamic potentials — the pattern Part 3 set on the length family and Part 4 on the force family. Item 5-20.1 is the broad genus; each later item is a species of energy, distinguished not by fiat but by an explicit defining construction (Dybkær's examination principle, §7.5). The species are then provably distinct kinds while remaining mutually comparable as energies.
An energy species is a ratio-scale quantity-kind of dimension
M·L²·T⁻² carrying an examination principle — this work's own
terse descriptor of the defining construction that distinguishes it (natural in S-V-N,
in S-p, in T-V, in T-p), never the standard's normative definition. Internal energy, the
enthalpy, and the Helmholtz and Gibbs energies are all species of the general energy kind
(item 5-20.1).
Lean code for Definition23.3.1●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/Iso80000/Part5.leancomplete
def PropertyKindCalculus.Iso80000.Part5.energySpecies (id : String) (p : PropertyKindCalculus.ExaminationPrinciple) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
def PropertyKindCalculus.Iso80000.Part5.energySpecies (id : String) (p : PropertyKindCalculus.ExaminationPrinciple) : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
An energy species: dimension `M·L²·T⁻²`, ratio-scale, individuated by its defining construction (examination principle).
energySpecies id p := { kind := { id, scale := .ratio, examPrinciple := some p.id },
dim := TDim.energy }. The general energy carries no examination principle; the
direct-parent edges of the family are collected in an Edge relation, each species an
edge to energy (mirroring the standard's "energy (item 5-20.1) … given by …").
The Helmholtz and Gibbs energies are distinct kinds — by defining construction, not by
fiat. They share dimension M·L²·T⁻² and are both "free energies", yet are different
kinds because they are defined by different natural variables (A = U − TS, natural in
T,V; G = H − TS, natural in T,p), proved through distinct_of_examPrinciple (§7.5). This
is the thermodynamic-potential analogue of width ≠ distance and static ≠ kinetic friction
force. Uses the examination principle.
Lean code for Theorem23.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part5.leancomplete
theorem PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy_ne_gibbsEnergy : PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part5.gibbsEnergy.kind LTMCTDimensionBase
theorem PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy_ne_gibbsEnergy : PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy.kind LTMCTDimensionBase ≠ PropertyKindCalculus.Iso80000.Part5.gibbsEnergy.kind LTMCTDimensionBase
**The Helmholtz and Gibbs energies are distinct kinds — by defining construction, not by fiat.** They have the same dimension `M·L²·T⁻²` and are both "free energies", yet they are different kinds *because they are defined by different natural variables* (`A = U − TS`, natural in T,V; `G = H − TS`, natural in T,p), proved through `distinct_of_examPrinciple` (§7.5) rather than by appealing to their `id` strings. This is the thermodynamic-potential analogue of width ≠ distance and static ≠ kinetic friction force.
helmholtzEnergy_ne_gibbsEnergy : helmholtzEnergy.kind ≠ gibbsEnergy.kind, from
KindOfProperty.distinct_of_examPrinciple applied to the differing principles natural-T-V
and natural-T-p (a decide on the Option String links). The companions
internalEnergy_ne_enthalpy and internalEnergy_ne_energy separate the other species, and
internalEnergy_examinedBy checks the kind-to-principle link. Axiom-free.
Comparability is preserved. The Helmholtz and Gibbs energies, though distinct kinds,
remain mutually comparable — they share the super-kind energy, so combining them is
possible but only via an explicit up-cast, never silently. The companion
internalEnergy_specializes_energy records that internal energy specializes energy. Uses
specialization.
Lean code for Theorem23.3.3●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/Iso80000/Part5.leancomplete
theorem PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy_gibbsEnergy_comparable : PropertyKindCalculus.MutuallyComparable PropertyKindCalculus.Iso80000.Part5.Edge (PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part5.gibbsEnergy.kind LTMCTDimensionBase)
theorem PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy_gibbsEnergy_comparable : PropertyKindCalculus.MutuallyComparable PropertyKindCalculus.Iso80000.Part5.Edge (PropertyKindCalculus.Iso80000.Part5.helmholtzEnergy.kind LTMCTDimensionBase) (PropertyKindCalculus.Iso80000.Part5.gibbsEnergy.kind LTMCTDimensionBase)
**Mutual comparability is preserved.** The Helmholtz and Gibbs energies, though distinct kinds, remain *mutually comparable* — they share the super-kind energy, so combining them is possible but only via an explicit up-cast, never silently.
helmholtzEnergy_gibbsEnergy_comparable : MutuallyComparable Edge helmholtzEnergy.kind
gibbsEnergy.kind, with witness energy.kind, each species reaching it by one edge.
Axiom-free.