23.2. Temperature: one dimension, two scales🔗

ISO 80000-5 lists thermodynamic temperature (5-1) and Celsius temperature (5-2) as separate items of the same dimension Θ. But they are not the same kind of quantity. Thermodynamic temperature has an absolute zero, so it is ratio-scale: ratios of temperatures are meaningful, and the kelvin admits × and ÷. Celsius temperature is measured from the arbitrary zero of the ice point (t = T − T₀), so it is interval-scale: only its differences are meaningful, and a ratio of Celsius temperatures is not a defined operation. A dimension-only model sees one type, "a real number of degrees", for both.

This is requirement R6 — the scale type fixes which operations are even defined — now on the real standard, the axis Part 3 and Part 4 (every quantity ratio-scale) could not exercise. The two temperatures are distinct kinds separated neither by dimension nor by an examination principle, but by their scale type alone.

Theorem23.2.1

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

Celsius temperature does not admit ×,÷. It is interval-scale (an arbitrary zero at the ice point), so a ratio of Celsius temperatures is not a meaningful operation — the scale layer refuses it where the dimension would not. Thermodynamic temperature, being ratio-scale, does admit it. Uses the scale type.

Lean code for Theorem23.2.1●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean

complete

theorem PropertyKindCalculus.Iso80000.Part5.celsiusTemperature_not_allowsRatio :
  ¬(PropertyKindCalculus.Iso80000.Part5.celsiusTemperature.kind
          LTMCTDimensionBase).scale.AllowsRatio

theorem PropertyKindCalculus.Iso80000.Part5.celsiusTemperature_not_allowsRatio :
  ¬(PropertyKindCalculus.Iso80000.Part5.celsiusTemperature.kind
          LTMCTDimensionBase).scale.AllowsRatio

**Celsius temperature does *not* admit `×`,`÷`.** It is interval-scale (an
arbitrary zero at the ice point), so a ratio of Celsius temperatures is not a
meaningful operation — the kind layer refuses it where dimension would not.

Proof for Theorem 23.2.1

uses 0

celsiusTemperature_not_allowsRatio : ¬ ScaleType.AllowsRatio celsiusTemperature.kind.scale, with the companion thermodynamicTemperature_allowsRatio for the ratio case. The degree Celsius is nonetheless WellFormed (degreeCelsius_wellFormed, via the differential scale), and thermodynamicTemperature_ne_celsiusTemperature (a decide) records that the two are distinct kinds.

Theorem23.2.2

groupuses 1used by 0✓L∃∀N

EffortsmallTagsproved

The scale disambiguation, on the standard. There exist distinct ISO 80000-5 kinds with the same dimension Θ that are separated by scale type alone — thermodynamic temperature (ratio) and Celsius temperature (interval) witness it. Neither the dimension nor an examination principle tells them apart; the scale layer does. This is requirement R6 on the standard. Uses the scale type.

Lean code for Theorem23.2.2●1 theorem

theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean

complete

theorem PropertyKindCalculus.Iso80000.Part5.iso80000_5_scale_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠ b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase = b.dim LTMCTDimensionBase ∧
        (a.kind LTMCTDimensionBase).scale ≠
          (b.kind LTMCTDimensionBase).scale

theorem PropertyKindCalculus.Iso80000.Part5.iso80000_5_scale_collision :
  ∃ a b,
    a.kind LTMCTDimensionBase ≠
        b.kind LTMCTDimensionBase ∧
      a.dim LTMCTDimensionBase =
          b.dim LTMCTDimensionBase ∧
        (a.kind
              LTMCTDimensionBase).scale ≠
          (b.kind
              LTMCTDimensionBase).scale

**The scale disambiguation, on standard quantities.** There exist distinct
ISO 80000-5 kinds with the same dimension `Θ` that are separated by *scale type* alone
— thermodynamic temperature (ratio) and Celsius temperature (interval) witness it.
Neither the dimension nor an examination principle tells them apart; the scale layer
does. This is requirement R6 on the standard, the axis Parts 3 and 4 could not show.

Proof for Theorem 23.2.2

uses 0

iso80000_5_scale_collision : ∃ a b : DimensionedKind, a.kind ≠ b.kind ∧ a.dim = b.dim ∧ a.kind.scale ≠ b.kind.scale, witnessed by ⟨thermodynamicTemperature, celsiusTemperature, …⟩ with reflexivity on the dimension and a decide on the differing scales. Axiom-free.