A Property Kind Calculus for Measurement Metrology

31.1. Quantity-kinds and units of IEC 80000-13🔗

Definition31.1.1
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. "13-24"), the principal quantity symbol, and the unit symbol (for the information quantities, the special named unit — shannon, erlang, bit — rather than the bare 1). The citation travels with the kind as data.

Lean code for Definition31.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. 
    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 31.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. IEC 80000-13, Edition 2.0, 2025-02 item 13-24. The catalogue lists all 42 items in item order — the traffic quantities (13-1 … 13-8), storage (13-9, 13-10), the information content and entropies (13-24 … 13-37), the rates (13-38 … 13-42), … — each paired with its unit symbol.