30.1. Quantity-kinds and units of ISO 80000-12
A catalogued kind pairs a dimensioned quantity-kind with its exact source in the series — the part, the printed item designation (e.g. "12-27.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 Definition30.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-12, Second edition, 2019-08 item 12-27.1. The catalogue lists all 60
items in item order — the lattice geometry (12-1.1 … 12-8), the band energies (12-24.1 …
12-27.2), the carrier densities (12-29.1 … 12-29.5), the superconductivity quantities
(12-35.1 … 12-38.2), … — each paired with its coherent SI unit symbol.