A Property Kind Calculus for Measurement Metrology

21.1. Quantity-kinds and units of ISO 80000-3🔗

Definition21.1.1
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — area is L² , volume is L³ , speed is L·T⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a metre and a second are not interchangeable. (4)
Group member previews
Preview
Theorem 21.1.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
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. "3-3"), 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 rather than kept in a comment.

Lean code for Definition21.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.

    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.
Proof for Definition 21.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. ISO 80000-3, Second edition, 2019-10 item 3-3. The catalogue lists all 42 items in item order — length (3-1.1), area (3-3), volume (3-4), duration (3-9), speed (3-10.2), frequency (3-17.1), … — each paired with its coherent SI unit symbol.

Theorem21.1.2
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — area is L² , volume is L³ , speed is L·T⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a metre and a second are not interchangeable. (4)
Group member previews
Preview
Definition 21.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Area is L² (item 3-3). The catalogued area kind carries length-exponent two in PhysLib's dimension group — the standard's dimensional statement reproduced as a checked computation, not an annotation. Uses the dimension map.

Lean code for Theorem21.1.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.area_dim_length :
  (PropertyKindCalculus.Iso80000.Part3.area.dim
        LTMCTDimensionBase).length =
    2
    theorem PropertyKindCalculus.Iso80000.Part3.area_dim_length :
  (PropertyKindCalculus.Iso80000.Part3.area.dim
        LTMCTDimensionBase).length =
    2
    Area is `L²`: its length-exponent is `2` (ISO 80000-3 item 3-3).
Proof for Theorem 21.1.2
uses 0

Proved as area_dim_length : area.dim.length = 2 in the Iso80000 library, discharged by Dim.area_length from the Dimension layer. The companion volume_dim_length (item 3-4) gives length-exponent three.

Theorem21.1.3
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — area is L² , volume is L³ , speed is L·T⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a metre and a second are not interchangeable. (4)
Group member previews
Preview
Definition 21.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Speed is L·T⁻¹ (item 3-10.2). The catalogued speed kind's dimension equals length divided by time — a checked computation in the dimension group. Uses the dimension map.

Lean code for Theorem21.1.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.speed_dim :
  PropertyKindCalculus.Iso80000.Part3.speed.dim LTMCTDimensionBase =
    PropertyKindCalculus.Dim.length / PropertyKindCalculus.Dim.time
    theorem PropertyKindCalculus.Iso80000.Part3.speed_dim :
  PropertyKindCalculus.Iso80000.Part3.speed.dim
      LTMCTDimensionBase =
    PropertyKindCalculus.Dim.length /
      PropertyKindCalculus.Dim.time
    Speed is length over time (`L·T⁻¹`), ISO 80000-3 item 3-10.2.
Proof for Theorem 21.1.3
uses 0

Proved as speed_dim : speed.dim = Dim.length / Dim.time, discharged by Dim.speed_eq. The catalogue also records curvature_dim_length = -1 (item 3-2, L⁻¹), frequency_dim_time = -1 (item 3-17.1, T⁻¹), and acceleration_dim_time = -2 (item 3-11, L·T⁻²).

Theorem21.1.4
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — area is L² , volume is L³ , speed is L·T⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a metre and a second are not interchangeable. (4)
Group member previews
Preview
Definition 21.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

The metre is a well-formed unit (item 3-1.1). Length is a ratio-scale kind, so it bears a unit (Dybkær §13.3.5); the metre is one such chosen reference.

Lean code for Theorem21.1.4●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.metre_wellFormed :
  PropertyKindCalculus.Iso80000.Part3.metre.WellFormed
    theorem PropertyKindCalculus.Iso80000.Part3.metre_wellFormed :
  PropertyKindCalculus.Iso80000.Part3.metre.WellFormed
    The metre is a well-formed unit (length is ratio-scale, so it bears a unit).
Proof for Theorem 21.1.4
uses 0

Proved as metre_wellFormed : metre.WellFormed via KindOfProperty.rational_bears_unit.

Theorem21.1.5
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — area is L² , volume is L³ , speed is L·T⁻¹ — are checked computations rather than annotations. Each unit is a metrological unit of its kind; commensurability is a type-level fact, so a metre and a second are not interchangeable. (4)
Group member previews
Preview
Definition 21.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

A metre and a second are not commensurable. Length and duration are distinct kinds, so their units cannot be compared by ratio — a type-level fact, not a runtime check. Uses metrological units.

Lean code for Theorem21.1.5●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part3.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part3.metre_second_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part3.metre.Commensurable
      PropertyKindCalculus.Iso80000.Part3.second
    theorem PropertyKindCalculus.Iso80000.Part3.metre_second_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part3.metre.Commensurable
      PropertyKindCalculus.Iso80000.Part3.second
    The metre and the second are **not** commensurable — length and duration are
distinct kinds (a type-level fact).
Proof for Theorem 21.1.5
uses 0

Proved as metre_second_not_commensurable : ¬ metre.Commensurable second by unfolding Commensurable to the underlying kinds and decide (length's kind id differs from duration's).