31.1. Quantity-kinds and units of IEC 80000-13
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
Associated Lean declarations
-
structuredefined in PropertyKindCalculus/Iso80000/Catalogue.leancomplete
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.
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.