A Property Kind Calculus for Measurement Metrology

22.1. Quantity-kinds and units of ISO 80000-4🔗

Definition22.1.1
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — force is M·L·T⁻² , energy M·L²·T⁻² , pressure M·L⁻¹·T⁻² , power M·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 kilogram and a newton are not interchangeable. (2)
Group member previews
Preview
Theorem 22.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. "4-9.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 rather than kept in a comment.

Lean code for Definition22.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 22.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. ISO 80000-4, Second edition, 2019-08 item 4-9.1. The catalogue lists all 54 items in item order — mass (4-1), momentum (4-8), force (4-9.1), torque (4-12.2), pressure (4-14.1), power (4-27), action (4-32), … — each paired with its coherent SI unit symbol.

Theorem22.1.2
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — force is M·L·T⁻² , energy M·L²·T⁻² , pressure M·L⁻¹·T⁻² , power M·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 kilogram and a newton are not interchangeable. (2)
Group member previews
Preview
Definition 22.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Force is M·L·T⁻² (item 4-9.1). The catalogued force kind carries time-exponent minus 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 Theorem22.1.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part4.force_dim_time :
  (PropertyKindCalculus.Iso80000.Part4.force.dim
        LTMCTDimensionBase).time =
    -2
    theorem PropertyKindCalculus.Iso80000.Part4.force_dim_time :
  (PropertyKindCalculus.Iso80000.Part4.force.dim
        LTMCTDimensionBase).time =
    -2
    Force is `M·L·T⁻²`: its time-exponent is `-2` (ISO 80000-4 item 4-9.1).
Proof for Theorem 22.1.2
uses 0

Proved as force_dim_time : force.dim.time = -2 in the Iso80000 library, discharged by norm_num over the PhysLib dimension lemmas. The companions energy_dim_length = 2 (item 4-28), pressure_dim_length = -1 (item 4-14.1), and power_dim_time = -3 (item 4-27) record the rest of the mechanical algebra.

Theorem22.1.3
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , so the standard's dimensional facts — force is M·L·T⁻² , energy M·L²·T⁻² , pressure M·L⁻¹·T⁻² , power M·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 kilogram and a newton are not interchangeable. (2)
Group member previews
Preview
Definition 22.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

A kilogram and a newton are not commensurable. Mass and force 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 Theorem22.1.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part4.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part4.kilogram_newton_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part4.kilogram.Commensurable
      PropertyKindCalculus.Iso80000.Part4.newton
    theorem PropertyKindCalculus.Iso80000.Part4.kilogram_newton_not_commensurable :
  ¬PropertyKindCalculus.Iso80000.Part4.kilogram.Commensurable
      PropertyKindCalculus.Iso80000.Part4.newton
    The kilogram and the newton are **not** commensurable — mass and force are distinct
kinds (a type-level fact).
Proof for Theorem 22.1.3
uses 0

Proved as kilogram_newton_not_commensurable : ¬ kilogram.Commensurable newton by unfolding Commensurable to the underlying kinds and decide. The kilogram and the newton are each WellFormed (mass and force are ratio-scale).