A Property Kind Calculus for Measurement Metrology

23.1. Quantity-kinds and units of ISO 80000-5🔗

Definition23.1.1
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the temperature generator Θ , so the standard's dimensional facts — heat is M·L²·T⁻² , entropy M·L²·T⁻²·Θ⁻¹ , a linear expansion coefficient Θ⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a kelvin and a joule are not interchangeable. (2)
Group member previews
Preview
Theorem 23.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

A catalogued kind pairs a dimensioned quantity-kind with its exact source in the series — the part, the printed item designation (e.g. "5-20.3"), the principal quantity symbol, and the coherent SI unit symbol. The citation travels with the kind as data, so the source of each definition can be rendered or audited downstream rather than kept in a comment.

Lean code for Definition23.1.1●1 definition
  • structure(5 fields)defined in PropertyKindCalculus/Iso80000/Catalogue.lean
    complete
    structure PropertyKindCalculus.Iso80000.CataloguedKind : Type
    structure PropertyKindCalculus.Iso80000.CataloguedKind :
  Type
    A **catalogued quantity-kind**: a {dimensioned kind} together with its exact
source in the 80000 series — the part, the printed item designation, the principal
quantity symbol, and the coherent SI unit symbol. Every field other than `qk` is a
*citation locator*; the citation travels with the kind as data, so a downstream
model can render or audit the source of each definition. Shared by every part
module, so the structure is defined once rather than per part.

    Fields

    ref : PropertyKindCalculus.Iso80000.StandardRef
    The part of the series this kind is defined in. 
    item : String
    The item designation as printed, e.g. "3-3". 
    symbol : String
    The principal quantity symbol, e.g. "A". 
    coherentUnit : String
    The coherent SI unit symbol, e.g. "m²" (a citation locator). 
    qk : PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
    The dimensioned kind itself.
Proof for Definition 23.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. ISO 80000-5, Second edition, 2019-08 item 5-18. The catalogue lists all 54 items in item order — thermodynamic temperature (5-1), heat (5-6.1), entropy (5-18), the thermodynamic potentials (5-20.1 … 5-20.5), the dew-point temperature (5-36), … — each paired with its coherent SI unit symbol.

Theorem23.1.2
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the temperature generator Θ , so the standard's dimensional facts — heat is M·L²·T⁻² , entropy M·L²·T⁻²·Θ⁻¹ , a linear expansion coefficient Θ⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a kelvin and a joule are not interchangeable. (2)
Group member previews
Preview
Definition 23.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Entropy is M·L²·T⁻²·Θ⁻¹ (item 5-18). The catalogued entropy kind carries temperature-exponent minus one in PhysLib's dimension group — the standard's dimensional statement reproduced as a checked computation over the temperature generator Θ, not an annotation. Uses the dimension map.

Lean code for Theorem23.1.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part5.entropy_dim_temperature :
  (PropertyKindCalculus.Iso80000.Part5.entropy.dim
        LTMCTDimensionBase).temperature =
    -1
    theorem PropertyKindCalculus.Iso80000.Part5.entropy_dim_temperature :
  (PropertyKindCalculus.Iso80000.Part5.entropy.dim
        LTMCTDimensionBase).temperature =
    -1
    Entropy is `M·L²·T⁻²·Θ⁻¹`: its temperature-exponent is `-1` (ISO 80000-5 item
5-18). The temperature generator `Θ` enters through the `energy / temperature`
quotient.
Proof for Theorem 23.1.2
uses 0

Proved as entropy_dim_temperature : entropy.dim.temperature = -1 in the Iso80000 library, discharged by norm_num over the PhysLib dimension lemmas for the temperature generator. The companions heatCapacity_dim_temperature = -1, heat_dim_length = 2 (item 5-6.1), and linearExpansionCoefficient_dim_temperature = -1 (item 5-3.1) record the rest of the thermodynamic algebra.

Theorem23.1.3
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , now over the temperature generator Θ , so the standard's dimensional facts — heat is M·L²·T⁻² , entropy M·L²·T⁻²·Θ⁻¹ , a linear expansion coefficient Θ⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a kelvin and a joule are not interchangeable. (2)
Group member previews
Preview
Definition 23.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

A kelvin and a joule are not commensurable. Thermodynamic temperature and energy are distinct kinds, so their units cannot be compared by ratio — a type-level fact, not a runtime check. Uses metrological units.

Lean code for Theorem23.1.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part5.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part5.kelvin_joule_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part5.kelvin.Commensurable
      PropertyKindCalculus.Iso80000.Part5.joule
    theorem PropertyKindCalculus.Iso80000.Part5.kelvin_joule_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part5.kelvin.Commensurable
      PropertyKindCalculus.Iso80000.Part5.joule
    The kelvin and the joule are **not** commensurable — thermodynamic temperature and
energy are distinct kinds (a type-level fact).
Proof for Theorem 23.1.3
uses 0

Proved as kelvin_joule_not_commensurable : ¬ kelvin.Commensurable joule by unfolding Commensurable to the underlying kinds and decide. The kelvin and the joule are each WellFormed (thermodynamic temperature and energy are ratio-scale).