27.1. Quantity-kinds and units of ISO 80000-9
A catalogued kind pairs a dimensioned quantity-kind with its exact source in the series — the part, the printed item designation (e.g. "9-12.1"), 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.
Lean code for Definition27.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. ISO 80000-9, Second edition, 2019-08 item 9-12.1. The catalogue lists all 62
items in item order — the mole (9-2), the molar quantities (9-4 … 9-8), the concentrations
(9-9.1 … 9-12.2), the activities (9-18 … 9-27.3), the partition functions (9-35.1 …
9-35.4), the conductivities (9-44, 9-45), … — each paired with its coherent SI unit symbol.