30.3. The algebraic Remarks as kind-laws: thermoelectricity built by the kind algebra🔗

Two Part-12 definitions state the thermoelectric coefficients algebraically: the Seebeck coefficient is the thermoelectric voltage per temperature (12-21, S = dE/dT), and the Peltier coefficient is the Seebeck coefficient times temperature (12-22, Π = S·T, the Kelvin relation). Both are specified as R12 kind-laws, crossing to ISO 80000-5 for the thermodynamic temperature.

Theorem30.3.1

uses 1used by 0✓L∃∀N

EffortsmallTagsproved

Peltier coefficient is Seebeck coefficient × temperature — a verified construction (item 12-22). A Peltier coefficient built as the product of a Seebeck coefficient and a thermodynamic temperature carries its product certificate by construction, over the ℝ carrier. The companion seebeck_dim_from_voltage_temperature shows the Seebeck coefficient is V/K because it is a voltage per temperature. Uses the quotient kind-law.

Lean code for Theorem30.3.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part12/DefiningRelations.lean

complete

theorem PropertyKindCalculus.Iso80000.Part12.DefiningRelations.peltierOf_isProduct
  (s :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part12.seebeckCoefficient.kind
        LTMCTDimensionBase)
      ℝ)
  (t :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part5.thermodynamicTemperature.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part12.DefiningRelations.peltier_prod_seebeck_temperature
    (PropertyKindCalculus.Iso80000.Part12.DefiningRelations.peltierOf s
      t)
    s t

theorem PropertyKindCalculus.Iso80000.Part12.DefiningRelations.peltierOf_isProduct
  (s :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part12.seebeckCoefficient.kind
        LTMCTDimensionBase)
      ℝ)
  (t :
    PropertyKindCalculus.Quantity
      (PropertyKindCalculus.Iso80000.Part5.thermodynamicTemperature.kind
        LTMCTDimensionBase)
      ℝ) :
  PropertyKindCalculus.Quantity.IsProduct
    PropertyKindCalculus.Iso80000.Part12.DefiningRelations.peltier_prod_seebeck_temperature
    (PropertyKindCalculus.Iso80000.Part12.DefiningRelations.peltierOf
      s t)
    s t

The constructed Peltier coefficient satisfies the product certificate by
construction.

Proof for Theorem 30.3.1

uses 0

peltierOf s t := Quantity.mul peltier_prod_seebeck_temperature s t, and peltierOf_isProduct is rfl. The companion seebeckOf (= thermoelectric voltage / temperature) carries the quotient certificate, with seebeck_certificate_canonical its canonicity; both cross to ISO 80000-5.