23.5. The algebraic Remarks as kind-laws: thermodynamics built from the earlier parts🔗

Many Part-5 remarks state a quantity's defining relation algebraically — and, in thermodynamics, the other quantities are often from earlier parts (mass from ISO 80000-4, area from ISO 80000-3) or from temperature, the base quantity this part introduces. Heat capacity is added heat per temperature (5-15); specific heat capacity is heat capacity / mass (5-16.1); specific entropy is entropy / mass (5-19); the density of heat flow rate is heat flow rate / area (5-8); thermal conductance is 1/R (5-13); the ratio of specific heats is cp/cV (5-17.1). Each is formalized as an R12 kind-law over the catalogued kinds, several composing a Part-5 kind out of an earlier part's kinds.

Theorem23.5.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Specific heat capacity is heat capacity / mass — a verified, cross-part construction. A specific heat capacity built as the quotient of a heat capacity (Part 5) by a mass (Part 4) carries its quotient certificate by construction, over the ℝ carrier, and canonicity makes the certificate determine the quantity. Uses the quotient kind-law.

Lean code for Theorem23.5.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part5.DefiningRelations.specificHeatCapacityOf_isQuotient
  (c :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part5.heatCapacity.kind
        LTMCTDimensionBase)
      ℝ)
  (m :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part4.mass.kind LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part5.DefiningRelations.specificHeatCapacity_quot_heatCapacity_mass
    (PropertyKindCalculus.Iso80000.Part5.DefiningRelations.specificHeatCapacityOf
      c m)
    c m

theorem PropertyKindCalculus.Iso80000.Part5.DefiningRelations.specificHeatCapacityOf_isQuotient
  (c :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part5.heatCapacity.kind
        LTMCTDimensionBase)
      ℝ)
  (m :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part4.mass.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsQuotient
    PropertyKindCalculus.Iso80000.Part5.DefiningRelations.specificHeatCapacity_quot_heatCapacity_mass
    (PropertyKindCalculus.Iso80000.Part5.DefiningRelations.specificHeatCapacityOf
      c m)
    c m

The constructed specific heat capacity satisfies the quotient certificate by
construction.

Proof for Theorem 23.5.1

uses 0

specificHeatCapacityOf c m := Quantity.div specificHeatCapacity_quot_heatCapacity_mass c m, and specificHeatCapacityOf_isQuotient is rfl; specificHeatCapacity_certificate_canonical is eq_div_of_isQuotient. The kind-law specificHeatCapacity_quot_heatCapacity_mass : QuotientKind heatCapacity.kind Part4.mass.kind specificHeatCapacity.kind is ⟨rfl, rfl, rfl⟩, and specificHeatCapacity_dim_from_heatCapacity_mass checks L²·T⁻²·Θ⁻¹ follows from the relation. The same families give densityOfHeatFlowRateOf (= heat flow rate / area) and thermalConductanceOf (= the reciprocal of thermal resistance).

Theorem23.5.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The ratio of specific heats is dimension one because it is a ratio of two specific heat capacities. From the remark γ = cp/cV, the specific heat capacities cancel and the dimension is computed to be one — not stipulated, the thermodynamic analogue of the plane angle being a ratio of two lengths and the efficiency a ratio of two powers. Yet the ratio remains a distinct kind from every other dimension-one quantity (the collision capstone above). Uses the dimension map.

Lean code for Theorem23.5.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part5.DefiningRelations.ratio_dim_from_specific_heats :
  PropertyKindCalculus.Iso80000.Part5.ratioOfSpecificHeatCapacities.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part5.specificHeatCapacityConstantPressure.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part5.specificHeatCapacityConstantVolume.dim
        LTMCTDimensionBase

theorem PropertyKindCalculus.Iso80000.Part5.DefiningRelations.ratio_dim_from_specific_heats :
  PropertyKindCalculus.Iso80000.Part5.ratioOfSpecificHeatCapacities.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Iso80000.Part5.specificHeatCapacityConstantPressure.dim
        LTMCTDimensionBase /
      PropertyKindCalculus.Iso80000.Part5.specificHeatCapacityConstantVolume.dim
        LTMCTDimensionBase

**The ratio of specific heat capacities is dimension one because it is a ratio of
two specific heat capacities.** The constant-pressure and constant-volume specific
heat capacities are both `L²·T⁻²·Θ⁻¹`, so `γ = cp/cV` cancels the dimension — the
ratio's dimensionlessness is a *checked computation from its defining relation*, not a
stipulation. (It nonetheless remains a distinct kind from every other dimension-one
quantity; see `Part5.iso80000_5_dim_one_collision`.) This is the thermodynamic
analogue of the plane angle being a ratio of two lengths and the efficiency being a
ratio of two powers.

Proof for Theorem 23.5.2

uses 0

ratio_dim_from_specific_heats : ratioOfSpecificHeatCapacities.dim = specificHeatCapacityConstantPressure.dim / specificHeatCapacityConstantVolume.dim, by reducing both sides via div_self' (a / a = 1). The kind-law ratioOfSpecificHeatCapacities_quot_cp_cV is ⟨rfl, rfl, rfl⟩.