A Property Kind Calculus for Measurement Metrology

29.1. Quantity-kinds of ISO 80000-11 — one dimension, 115 kinds🔗

Definition29.1.1
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , but here every kind maps to the same value, dimension one. The distinguishing datum is moved entirely onto the examination principle — the measurement principle, this work's terse descriptor of the defining ratio, paired with the transport-phenomena context (the clause). Each kind still bears values and a coherent unit ( 1 for all); commensurability is a type-level fact, so two characteristic numbers with the same unit symbol 1 are still not interchangeable. (2)
Group member previews
Preview
Definition 29.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. "11-4.1"), the principal quantity symbol (e.g. Re), and the coherent SI unit symbol (1 for every characteristic number). The citation travels with the kind as data, so the source of each definition can be rendered or audited downstream.

Lean code for Definition29.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 29.1.1
uses 0

Realized as structure CataloguedKind over a DimensionedKind, with cite rendering e.g. ISO 80000-11, Second edition, 2019-10 item 11-4.1. The catalogue lists all 115 items in item order across clauses 4 … 9; catalogue_length : catalogue.length = 115 checks the count.

Definition29.1.2
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , but here every kind maps to the same value, dimension one. The distinguishing datum is moved entirely onto the examination principle — the measurement principle, this work's terse descriptor of the defining ratio, paired with the transport-phenomena context (the clause). Each kind still bears values and a coherent unit ( 1 for all); commensurability is a type-level fact, so two characteristic numbers with the same unit symbol 1 are still not interchangeable. (2)
Group member previews
Preview
Definition 29.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 6.4.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N

A characteristic number is a ratio-scale quantity-kind of dimension one, individuated by its examination principle — the measurement principle, formed as context: defining-ratio. The context is one of ISO 80000-11's six clauses (momentum transfer, heat transfer, mass transfer, constants of matter, magnetohydrodynamics, miscellaneous); it is part of the principle because the same ratio name recurs across clauses as a different kind.

Lean code for Definition29.1.2●1 definition
  • defdefined in PropertyKindCalculus/Iso80000/Part11.lean
    complete
    def PropertyKindCalculus.Iso80000.Part11.charNum
  (ctx : PropertyKindCalculus.Iso80000.Part11.Context)
  (id principle : String) :
  PropertyKindCalculus.DimensionedKind LTMCTDimensionBase
    def PropertyKindCalculus.Iso80000.Part11.charNum
  (ctx :
    PropertyKindCalculus.Iso80000.Part11.Context)
  (id principle : String) :
  PropertyKindCalculus.DimensionedKind
    LTMCTDimensionBase
    A **characteristic number**: a ratio-scale {dimensioned kind} of **dimension one**,
named by `id` and individuated by its {examination principle} — the measurement principle,
formed as `context: defining-ratio`. The dimension is one for every characteristic number;
the principle is what tells them apart.
Proof for Definition 29.1.2
uses 0

charNum ctx id principle := { kind := { id, scale := .ratio, examPrinciple := some (ctx.id ++ ": " ++ principle) }, dim := Dim.one }, with the clause Context an enumeration (momentum, heat, mass, constants, mhd, misc). Every kind in the part is built by this one constructor.

Theorem29.1.3
Group: Each catalogued kind reuses the dimension functor dim over PhysLib's Dimension , but here every kind maps to the same value, dimension one. The distinguishing datum is moved entirely onto the examination principle — the measurement principle, this work's terse descriptor of the defining ratio, paired with the transport-phenomena context (the clause). Each kind still bears values and a coherent unit ( 1 for all); commensurability is a type-level fact, so two characteristic numbers with the same unit symbol 1 are still not interchangeable. (2)
Group member previews
Preview
Definition 29.1.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
EffortsmallTagsproved

Every characteristic number is dimension one — the widest collapse in the series. All 115 catalogued kinds share the dimensionless dimension; the dimension functor collapses the entire part to one point. What distinguishes them is the measurement principle, never the dimension. Uses the dimension map.

Lean code for Theorem29.1.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Iso80000/Part11.lean
    complete
    theorem PropertyKindCalculus.Iso80000.Part11.catalogue_all_dim_one
  (c : PropertyKindCalculus.Iso80000.CataloguedKind) :
  c ∈ PropertyKindCalculus.Iso80000.Part11.catalogue →
    c.qk.dim LTMCTDimensionBase = 1
    theorem PropertyKindCalculus.Iso80000.Part11.catalogue_all_dim_one
  (c :
    PropertyKindCalculus.Iso80000.CataloguedKind) :
  c ∈
      PropertyKindCalculus.Iso80000.Part11.catalogue →
    c.qk.dim LTMCTDimensionBase = 1
    **The entire ISO 80000-11 catalogue lives at dimension one.** All 115 characteristic
numbers share the dimensionless dimension; what distinguishes them is the measurement
principle, never the dimension.
Proof for Theorem 29.1.3
uses 0

catalogue_all_dim_one : ∀ c ∈ catalogue, c.qk.dim = 1, by fin_cases over the catalogue then reflexivity (each entry is a charNum application, whose dim is Dim.one by construction — charNum_dim_one). Axiom-free.