A Property Kind Calculus for Measurement Metrology

30.1. Quantity-kinds and units of ISO 80000-12🔗

Definition30.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. "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
  • 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 30.1.1
uses 0

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.