A Property Kind Calculus for Measurement Metrology

6.2. Kind-of-property and kind-of-quantity (Dybkær Ch. 6, 13)🔗

Definition6.2.1
Group: A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). (5)
Group member previews
Preview
Theorem 6.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 17
Reverse dependency previews
Preview
Theorem 6.2.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A kind-of-property (§6.19) bundles a terminological id, a scale (from the scale types), and an optional examination principle. A kind is a kind-of-quantity (§13.3.1) iff its scale has magnitude (is at least ordinal).

Lean code for Definition6.2.1●1 definition
  • structure(3 fields)defined in PropertyKindCalculus/Kind.lean
    complete
    structure PropertyKindCalculus.KindOfProperty : Type
    structure PropertyKindCalculus.KindOfProperty : Type
    **§6.19 kind-of-property** — common defining aspect of mutually comparable
properties. In four-category terms (Lowe, Fig. 7.1) this is the *Attributes* corner —
the non-substantial universal, instantiated by individual quantities (its modes) and
characterizing sorts of system through the §20 dedicated kinds.

    Fields

    id : String
    Terminological identity (mirrors the OML `id`). 
    scale : PropertyKindCalculus.ScaleType
    The scale type (Ch. 12) — which operations are defined on its instances. 
    examPrinciple : Option String
    **§7.5 examination principle** used as a defining aspect, when present.
Proof for Definition 6.2.1
uses 0

A structure with DecidableEq. IsQuantity, and the scale divisions IsNominal/IsOrdinal/IsDifferential/IsRational (§13.2), are definitional predicates over the scale field.

Theorem6.2.2
Group: A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). (5)
Group member previews
Preview
Definition 6.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
OwnerNicolas RouquetteTagsproved

A nominal kind is, by construction, not a kind-of-quantity: it has no magnitude. Uses kind-of-property.

Lean code for Theorem6.2.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Kind.lean
    complete
    theorem PropertyKindCalculus.KindOfProperty.nominal_not_quantity
  {k : PropertyKindCalculus.KindOfProperty} (h : k.IsNominal) :
  ¬k.IsQuantity
    theorem PropertyKindCalculus.KindOfProperty.nominal_not_quantity
  {k :
    PropertyKindCalculus.KindOfProperty}
  (h : k.IsNominal) : ¬k.IsQuantity
    A nominal kind is, by construction, not a kind-of-quantity (§13.3.1).
Proof for Theorem 6.2.2
uses 0

Unfold IsQuantity, IsNominal, and HasMagnitude; the scale is nominal, so scale ≠ nominal is false.

Theorem6.2.3
Group: A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). (5)
Group member previews
Preview
Definition 6.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
OwnerNicolas RouquetteTagsproved

A rational kind is a kind-of-quantity. Uses kind-of-property.

Lean code for Theorem6.2.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Kind.lean
    complete
    theorem PropertyKindCalculus.KindOfProperty.rational_isQuantity
  {k : PropertyKindCalculus.KindOfProperty} (h : k.IsRational) :
  k.IsQuantity
    theorem PropertyKindCalculus.KindOfProperty.rational_isQuantity
  {k :
    PropertyKindCalculus.KindOfProperty}
  (h : k.IsRational) : k.IsQuantity
    A rational kind *is* a kind-of-quantity.
Proof for Theorem 6.2.3
uses 0

The scale is ratio, so scale ≠ nominal holds; unfold and simplify.

Definition6.2.4
Group: A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). (5)
Group member previews
Preview
Definition 6.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

A kind is a ratio quantity (VIM4 2CD 1.3) when its scale is ratio: the operators \times, \div are defined, so its quantities have an absolute zero and form ratios.

Lean code for Definition6.2.4●1 definition
  • defdefined in PropertyKindCalculus/Kind.lean
    complete
    def PropertyKindCalculus.KindOfProperty.IsRational
  (k : PropertyKindCalculus.KindOfProperty) : Prop
    def PropertyKindCalculus.KindOfProperty.IsRational
  (k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    §13.2.4 rational kind-of-property (divisible).
Proof for Definition 6.2.4
uses 0

IsRational k := k.scale = .ratio.

Definition6.2.5
Group: A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). (5)
Group member previews
Preview
Definition 6.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

A kind is an interval quantity (VIM4 2CD 1.4) when its scale is interval: the operators +, - are defined (differences are meaningful), but ratios are not.

Lean code for Definition6.2.5●1 definition
  • defdefined in PropertyKindCalculus/Kind.lean
    complete
    def PropertyKindCalculus.KindOfProperty.IsDifferential
  (k : PropertyKindCalculus.KindOfProperty) : Prop
    def PropertyKindCalculus.KindOfProperty.IsDifferential
  (k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    §13.2.3 differential kind-of-property (subtractive, not divisible).
Proof for Definition 6.2.5
uses 0

IsDifferential k := k.scale = .interval.

Definition6.2.6
Group: A kind is the "common defining aspect of mutually comparable properties" (§6.19). It is an open value — applications declare new kinds as def s — and it carries its scale and an optional examination principle (§7.5) used to individuate otherwise-comparable kinds (width vs. height). (5)
Group member previews
Preview
Definition 6.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N

A kind is an ordinal quantity (VIM4 2CD 1.33) when its scale is ordinal: only the order <, > is defined, with neither differences nor ratios.

Lean code for Definition6.2.6●1 definition
  • defdefined in PropertyKindCalculus/Kind.lean
    complete
    def PropertyKindCalculus.KindOfProperty.IsOrdinal
  (k : PropertyKindCalculus.KindOfProperty) : Prop
    def PropertyKindCalculus.KindOfProperty.IsOrdinal
  (k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    §13.2.2 ordinal kind-of-property (rankable, not subtractive).
Proof for Definition 6.2.6
uses 0

IsOrdinal k := k.scale = .ordinal.