A Property Kind Calculus for Measurement Metrology

6.5. Property value and value scale (Dybkær Ch. 9, 16, 10, 17)🔗

Definition6.5.1
Group: A property value (§9.15) is an inherent feature of a property used in comparing it with other properties of the same kind-of-property; it is a member of a value scale (§10.14), the ordered set of possible, mutually comparable values of a kind. A quantity value (§16.10) is the special case carried as a numerical value times a reference — Dybkær's "reference quantity multiplied by a number". The laws below — that comparability of values is an equivalence, that a value scale holds only mutually comparable values, that a value's scale type fixes which operations are defined — quantify over relations, operations, and a scale's members; a description logic can record an instance of the link but can neither state nor prove the laws. (3)
Group member previews
Preview
Theorem 6.5.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 4
Reverse dependency previews
Preview
Theorem 6.5.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A property value (§9.15) bundles its kind-of-property, a numeral (the numerical value, §16.10), and the reference the numeral is taken against — a metrological unit for a quantity value, a designation for a nominal one. A value is a quantity value (§16.10) iff its kind has magnitude, and two values are comparable iff they are of the same kind.

Lean code for Definition6.5.1●1 definition
  • structure(3 fields)defined in PropertyKindCalculus/PropertyValue.lean
    complete
    structure PropertyKindCalculus.PropertyValue : Type
    structure PropertyKindCalculus.PropertyValue : Type
    **§9.15 property value** — an inherent feature of a property used in comparing
it with other properties of the *same* kind-of-property. Carried as a kind
together with its representation (§9.15 Note 2): a numeral and the reference the
numeral is taken against.

    Fields

    kind : PropertyKindCalculus.KindOfProperty
    §9.15 — the kind-of-property this value belongs to; a value is comparable
only with values of the same kind. 
    numeral : Int
    §16.10 — the numerical value (numeral). For a quantity value the magnitude
is this number times the `reference`; for a nominal value (§12.4) it is a bare
type-number / label. 
    reference : String
    §16.10 — the reference the numeral is taken against: a metrological unit id
for a quantity value (§18.12), or a category/designation id for a nominal one.
Proof for Definition 6.5.1
uses 0

A structure with DecidableEq. scale, IsQuantityValue, and Comparable are definitional projections over the kind field.

Theorem6.5.2
Group: A property value (§9.15) is an inherent feature of a property used in comparing it with other properties of the same kind-of-property; it is a member of a value scale (§10.14), the ordered set of possible, mutually comparable values of a kind. A quantity value (§16.10) is the special case carried as a numerical value times a reference — Dybkær's "reference quantity multiplied by a number". The laws below — that comparability of values is an equivalence, that a value scale holds only mutually comparable values, that a value's scale type fixes which operations are defined — quantify over relations, operations, and a scale's members; a description logic can record an instance of the link but can neither state nor prove the laws. (3)
Group member previews
Preview
Definition 6.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
OwnerNicolas RouquetteTagsproved

Comparability of values is an equivalence. Two property values are comparable iff they are of the same kind (§9.15); the relation is reflexive, symmetric, and transitive. Comparable values are moreover governed by the same scale type, so the same operators are defined on both (scale_eq_of_comparable). Transitivity is exactly the algebraic law a description logic cannot state.

Lean code for Theorem6.5.2●1 theorem
  • theoremdefined in PropertyKindCalculus/PropertyValue.lean
    complete
    theorem PropertyKindCalculus.PropertyValue.Comparable.trans
  {u v w : PropertyKindCalculus.PropertyValue} (h₁ : u.Comparable v)
  (h₂ : v.Comparable w) : u.Comparable w
    theorem PropertyKindCalculus.PropertyValue.Comparable.trans
  {u v w :
    PropertyKindCalculus.PropertyValue}
  (h₁ : u.Comparable v)
  (h₂ : v.Comparable w) : u.Comparable w
    Comparability is transitive — the law a description logic cannot state.
Proof for Theorem 6.5.2
uses 0

Comparability unfolds to equality of the kind field, so reflexivity, symmetry, and transitivity are those of Eq; scale_eq_of_comparable is congrArg on the scale projection.

Definition6.5.3
Group: A property value (§9.15) is an inherent feature of a property used in comparing it with other properties of the same kind-of-property; it is a member of a value scale (§10.14), the ordered set of possible, mutually comparable values of a kind. A quantity value (§16.10) is the special case carried as a numerical value times a reference — Dybkær's "reference quantity multiplied by a number". The laws below — that comparability of values is an equivalence, that a value scale holds only mutually comparable values, that a value's scale type fixes which operations are defined — quantify over relations, operations, and a scale's members; a description logic can record an instance of the link but can neither state nor prove the laws. (3)
Group member previews
Preview
Definition 6.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

A property value scale (§10.14) is the ordered set of possible, mutually comparable values of one kind. It carries that kind and a provenance — true (consistent with the property's definition, §10.16.1) or examined (obtained by an examination procedure, §10.16.2). Its scaleType is the kind's scale, the datum Table 17.4 uses to gate which manipulations a scale admits, and KindOfProperty.valueScale gives the canonical true scale of a kind (§9.15 ↔ §10.14).

Lean code for Definition6.5.3●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/ValueScale.lean
    complete
    structure PropertyKindCalculus.ValueScale : Type
    structure PropertyKindCalculus.ValueScale : Type
    **§10.14 property value scale** — the ordered set of possible, mutually
comparable property values of one kind. Carried as that kind together with its
provenance (§10.16).

    Fields

    kind : PropertyKindCalculus.KindOfProperty
    §10.14 — the kind-of-property whose values this scale orders. 
    provenance : PropertyKindCalculus.ScaleProvenance
    §10.16 — whether this is a true or an examined property-value scale.
Proof for Definition 6.5.3
uses 0

A structure carrying kind and a ScaleProvenance; Admits v is v.kind = s.kind, and KindOfProperty.valueScale builds the canonical true scale.

Theorem6.5.4
Group: A property value (§9.15) is an inherent feature of a property used in comparing it with other properties of the same kind-of-property; it is a member of a value scale (§10.14), the ordered set of possible, mutually comparable values of a kind. A quantity value (§16.10) is the special case carried as a numerical value times a reference — Dybkær's "reference quantity multiplied by a number". The laws below — that comparability of values is an equivalence, that a value scale holds only mutually comparable values, that a value's scale type fixes which operations are defined — quantify over relations, operations, and a scale's members; a description logic can record an instance of the link but can neither state nor prove the laws. (3)
Group member previews
Preview
Definition 6.5.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Theorem 6.1.3
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
OwnerNicolas RouquettePriorityhighTagscapstoneproved

A value scale holds only mutually comparable values. Any two values a value scale admits are of the scale's kind, hence comparable (§10.14) — the defining property of a value scale, quantified over its members. The scale type further licenses operations monotonically (allows_mono_of_le): a richer value scale supports every manipulation a poorer one does (Table 17.4), inherited from operator monotonicity.

Lean code for Theorem6.5.4●1 theorem
  • theoremdefined in PropertyKindCalculus/ValueScale.lean
    complete
    theorem PropertyKindCalculus.ValueScale.comparable_of_mem
  {s : PropertyKindCalculus.ValueScale}
  {v w : PropertyKindCalculus.PropertyValue} (hv : s.Admits v)
  (hw : s.Admits w) : v.Comparable w
    theorem PropertyKindCalculus.ValueScale.comparable_of_mem
  {s : PropertyKindCalculus.ValueScale}
  {v w :
    PropertyKindCalculus.PropertyValue}
  (hv : s.Admits v) (hw : s.Admits w) :
  v.Comparable w
    **§10.14 — a value scale holds only mutually comparable values.** Any two
values a scale admits are of the scale's kind, and so are comparable. This is the
defining property of a value scale, and it quantifies over the scale's members.
Proof for Theorem 6.5.4
uses 0

Membership unfolds to equality with the scale's kind, so two members' kinds are equal by trans/symm; operator monotonicity is the scale-layer allows_mono re-exported through scaleType.