A Property Kind Calculus for Measurement Metrology

6.6. Metrological units (Dybkær Ch. 18, §13.3.3)🔗

Definition6.6.1
Group: A metrological unit (§18.12) is one quantity of a kind chosen as the reference : "with which any other quantity of the same kind can be compared" (VIM4 2CD 1.12). It belongs to a unitary kind-of-quantity (§13.3.3), whose magnitudes are "a reference quantity multiplied by a number" — the differential (§13.3.4) and rational (§13.3.5) kinds. The two laws specified here are ones a description logic can record an instance of but neither state nor prove: that commensurability — being "of the same kind", the only relation along which a value converts — is an equivalence relation (a relation that is reflexive, symmetric, and transitive, so it partitions units into convertible classes); and that the number-and-reference form is a faithful round-trip. This is the symbolic (numeral-and-reference) layer; the real-valued Quantity k with conversion ratios and the dimension-1 disambiguation are the planned PhysLib refinement, stated in the Units and the Dimension-1 Problem chapter. (3)
Group member previews
Preview
Theorem 6.6.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 2
Statement dependency previews
Preview
Definition 6.2.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 22
Reverse dependency previews
Preview
Theorem 6.6.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A metrological unit (§18.12) carries the kind it references and a terminological symbol (the unit id, e.g. "m", "kg"). A kind bears a unit (BearsUnit, §13.3.3) iff its scale is at least differential, and a unit is well-formed iff its kind bears one; measure u n builds the property value "n × symbol".

Lean code for Definition6.6.1●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/Unit.lean
    complete
    structure PropertyKindCalculus.MetrologicalUnit : Type
    structure PropertyKindCalculus.MetrologicalUnit :
  Type
    **§18.12 metrological unit** — one quantity of a kind chosen as the reference,
"with which any other quantity of the same kind can be compared". Carried as the
kind it references together with its terminological `symbol` (the §18.12 unit id,
e.g. `"m"`, `"kg"`). Like `KindOfProperty`, it is an open value so applications
declare units as `def`s.

    Fields

    kind : PropertyKindCalculus.KindOfProperty
    §18.12 / §13.3.3 — the kind whose quantities this unit references. A
well-formed unit's kind must bear a unit (`WellFormed`). 
    symbol : String
    §18.12 — the terminological identity of the unit (the unit id, e.g. `"m"`).
Proof for Definition 6.6.1
uses 0

A structure with DecidableEq. BearsUnit is scale.AllowsDifference, WellFormed is kind.BearsUnit, and measure fills the value's numeral and reference fields from n and the unit's symbol.

Theorem6.6.2
Group: A metrological unit (§18.12) is one quantity of a kind chosen as the reference : "with which any other quantity of the same kind can be compared" (VIM4 2CD 1.12). It belongs to a unitary kind-of-quantity (§13.3.3), whose magnitudes are "a reference quantity multiplied by a number" — the differential (§13.3.4) and rational (§13.3.5) kinds. The two laws specified here are ones a description logic can record an instance of but neither state nor prove: that commensurability — being "of the same kind", the only relation along which a value converts — is an equivalence relation (a relation that is reflexive, symmetric, and transitive, so it partitions units into convertible classes); and that the number-and-reference form is a faithful round-trip. This is the symbolic (numeral-and-reference) layer; the real-valued Quantity k with conversion ratios and the dimension-1 disambiguation are the planned PhysLib refinement, stated in the Units and the Dimension-1 Problem chapter. (3)
Group member previews
Preview
Definition 6.6.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N
OwnerNicolas RouquetteTagsproved

Commensurability is an equivalence. Two units are commensurable iff they reference the same kind (§9.13.4); the relation is reflexive, symmetric, and transitive. A metre and a centimetre are commensurable; a metre and a kilogram are not — incommensurability across kinds is a fact of the types, not a runtime check. Transitivity is exactly the law a description logic cannot state.

Lean code for Theorem6.6.2●1 theorem
  • theoremdefined in PropertyKindCalculus/Unit.lean
    complete
    theorem PropertyKindCalculus.MetrologicalUnit.Commensurable.trans
  {u₁ u₂ u₃ : PropertyKindCalculus.MetrologicalUnit}
  (h₁ : u₁.Commensurable u₂) (h₂ : u₂.Commensurable u₃) :
  u₁.Commensurable u₃
    theorem PropertyKindCalculus.MetrologicalUnit.Commensurable.trans
  {u₁ u₂ u₃ :
    PropertyKindCalculus.MetrologicalUnit}
  (h₁ : u₁.Commensurable u₂)
  (h₂ : u₂.Commensurable u₃) :
  u₁.Commensurable u₃
    Commensurability is transitive — the law a description logic cannot state.
Proof for Theorem 6.6.2
uses 0

Commensurability unfolds to equality of the kind field, so reflexivity, symmetry, and transitivity are those of Eq.

Theorem6.6.3
Group: A metrological unit (§18.12) is one quantity of a kind chosen as the reference : "with which any other quantity of the same kind can be compared" (VIM4 2CD 1.12). It belongs to a unitary kind-of-quantity (§13.3.3), whose magnitudes are "a reference quantity multiplied by a number" — the differential (§13.3.4) and rational (§13.3.5) kinds. The two laws specified here are ones a description logic can record an instance of but neither state nor prove: that commensurability — being "of the same kind", the only relation along which a value converts — is an equivalence relation (a relation that is reflexive, symmetric, and transitive, so it partitions units into convertible classes); and that the number-and-reference form is a faithful round-trip. This is the symbolic (numeral-and-reference) layer; the real-valued Quantity k with conversion ratios and the dimension-1 disambiguation are the planned PhysLib refinement, stated in the Units and the Dimension-1 Problem chapter. (3)
Group member previews
Preview
Definition 6.6.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
OwnerNicolas RouquetteTagsproved

Only a unitary kind bears a unit. A nominal kind has no magnitude, and — the distinctive §9.13.4 fact — an ordinal kind, though rankable, has no reference-times-number magnitude either, so neither bears a metrological unit (not_wellFormed_of_nominal, not_wellFormed_of_ordinal). Conversely a rational kind does (rational_bears_unit), and bearing a unit implies being a kind-of-quantity (bearsUnit_isQuantity). This gate is invisible to a dimension-and-scale-only view that treats every magnitude alike. Uses the metrological unit.

Lean code for Theorem6.6.3●1 theorem
  • theoremdefined in PropertyKindCalculus/Unit.lean
    complete
    theorem PropertyKindCalculus.MetrologicalUnit.not_wellFormed_of_ordinal
  {u : PropertyKindCalculus.MetrologicalUnit} (h : u.kind.IsOrdinal) :
  ¬u.WellFormed
    theorem PropertyKindCalculus.MetrologicalUnit.not_wellFormed_of_ordinal
  {u :
    PropertyKindCalculus.MetrologicalUnit}
  (h : u.kind.IsOrdinal) : ¬u.WellFormed
    A metrological unit of an ordinal kind is ill-formed (§9.13.4).
Proof for Theorem 6.6.3
uses 0

BearsUnit is scale.AllowsDifference, which is False at nominal and ordinal; substitute the scale from IsNominal/IsOrdinal and the goal is ¬ False. The rational case and bearsUnit_isQuantity are the same four-way case split on the scale.

Theorem6.6.4
Group: A metrological unit (§18.12) is one quantity of a kind chosen as the reference : "with which any other quantity of the same kind can be compared" (VIM4 2CD 1.12). It belongs to a unitary kind-of-quantity (§13.3.3), whose magnitudes are "a reference quantity multiplied by a number" — the differential (§13.3.4) and rational (§13.3.5) kinds. The two laws specified here are ones a description logic can record an instance of but neither state nor prove: that commensurability — being "of the same kind", the only relation along which a value converts — is an equivalence relation (a relation that is reflexive, symmetric, and transitive, so it partitions units into convertible classes); and that the number-and-reference form is a faithful round-trip. This is the symbolic (numeral-and-reference) layer; the real-valued Quantity k with conversion ratios and the dimension-1 disambiguation are the planned PhysLib refinement, stated in the Units and the Dimension-1 Problem chapter. (3)
Group member previews
Preview
Definition 6.6.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
Statement uses 3
Statement dependency previews
Preview
Definition 6.5.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
used by 0✓L∃∀N
OwnerNicolas RouquettePriorityhighTagscapstoneproved

The number-and-reference form is a faithful round-trip (§13.3.3). Measuring a quantity in a unit yields a numeral, and re-applying the unit to that numeral recovers the value: \mathrm{numeral}\,(\mathrm{measure}\ u\ n) = n \qquad\text{and}\qquad \mathrm{measure}\ u\ (\mathrm{numeral}\ v) = v \;\text{ when } v \text{ is measured in } u. So quantity / unit = number and number × unit = quantity invert one another — the §13.3.3 "reference quantity multiplied by a number", checked as a law. Measuring in a well-formed unit moreover yields a quantity value (measure_isQuantityValue), and values measured in commensurable units are comparable. Builds on the metrological unit.

Lean code for Theorem6.6.4●1 theorem
  • theoremdefined in PropertyKindCalculus/Unit.lean
    complete
    theorem PropertyKindCalculus.MetrologicalUnit.measure_eq_of_measures
  {u : PropertyKindCalculus.MetrologicalUnit}
  {v : PropertyKindCalculus.PropertyValue} (h : u.Measures v) :
  u.measure v.numeral = v
    theorem PropertyKindCalculus.MetrologicalUnit.measure_eq_of_measures
  {u :
    PropertyKindCalculus.MetrologicalUnit}
  {v : PropertyKindCalculus.PropertyValue}
  (h : u.Measures v) :
  u.measure v.numeral = v
    **`number × unit = quantity`** — re-applying a unit to the numeral of a value
measured in it recovers the value exactly. Together with `measure_numeral` this is
the §13.3.3 number-and-reference *round-trip*: the unit is a faithful reference.
Proof for Theorem 6.6.4
uses 0

measure_numeral is rfl. For the converse, destructure "measured in u" into the kind- and reference-equalities, unfold measure, and rewrite the unit's kind and symbol back to the value's fields; structure eta closes the goal.