A Property Kind Calculus for Measurement Metrology

10.2. Verified classification and instantiable kind-laws (R12)🔗

A quantity Quantity k R records its kind k as a tag: the magnitude is an arbitrary R, so a value can be labelled with a kind it has not earned (⟨999⟩ type-checks as an area). R12 upgrades a classification from an assertion to a certificate: a quantity is classified under a kind by a proof that it satisfies the kind's defining relation — the formalized ISO 80000 Remark — to quantities of the kinds it is built from. The kind becomes a refinement (a tag plus its earned proof), not a label.

The payoff is instantiation. Every kind-law is stated as a carrier-parametric universal over quantities with the kind-relation as a premise; "instantiating it at the quantity level" is then ordinary application, and any property of a kind's defining relation transports to every quantity certified under it. This is the inter-kind generalization of the carrier-parametric laws of R10.

Definition10.2.1
Group: The canonical pattern is the product , which covers a large fraction of the ISQ (area = length · length, volume = area · length, energy = force · length). The general machinery lives in the Mathlib-free core; the dimensional refinement ( k.dim = k₁.dim · k₂.dim ) lives in the dimension layer, and analysis-shaped relations (area as a surface integral) in the Mathlib-backed layer. (4)
Group member previews
Preview
Definition 10.2.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 2
Reverse dependency previews
Preview
Theorem 10.1.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A product kind-law ProductKind k₁ k₂ k records that k is the product kind of k₁ and k₂. In the core it carries the scale precondition — all three are ratio-scale, since only ratio quantities multiply (Dybkær §13.3.5); the dimension layer refines it with the dimensional equation k.\dim = k_1.\dim \cdot k_2.\dim.

Lean code for Definition10.2.1●1 definition
  • structure(3 fields)defined in PropertyKindCalculus/QuantityClassification.lean
    complete
    structure PropertyKindCalculus.ProductKind
  (k₁ k₂ k : PropertyKindCalculus.KindOfProperty) : Prop
    structure PropertyKindCalculus.ProductKind
  (k₁ k₂ k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    **A kind-level product law.** `k` is the *product kind* of `k₁` and `k₂`: all three
are ratio-scale (Dybkær §13.3.5 — only ratio quantities multiply), the precondition for
forming a product quantity. The Dimension layer strengthens this with the dimensional
equation `k.dim = k₁.dim * k₂.dim`; in the core it carries the scale precondition.

    Fields

    ratio₁ : k₁.IsRational
    The first factor is ratio-scale. 
    ratio₂ : k₂.IsRational
    The second factor is ratio-scale. 
    ratioProduct : k.IsRational
    The product is ratio-scale.
Proof for Definition 10.2.1
uses 0

Realized as structure ProductKind with three IsRational fields. A concrete law such as area = length · length is the value ⟨rfl, rfl, rfl⟩.

Definition10.2.2
Group: The canonical pattern is the product , which covers a large fraction of the ISQ (area = length · length, volume = area · length, energy = force · length). The general machinery lives in the Mathlib-free core; the dimensional refinement ( k.dim = k₁.dim · k₂.dim ) lives in the dimension layer, and analysis-shaped relations (area as a surface integral) in the Mathlib-backed layer. (4)
Group member previews
Preview
Definition 10.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

The certificate q.IsProduct h a b states that q (of kind k) is the product of a (of k₁) and b (of k₂): its magnitude is the product of theirs. A proof of this certifies q's classification, rather than asserting it. It is a separate proposition, so Quantity stays a clean tag and certificates are carried only when needed. The smart constructor Quantity.mul yields a quantity whose certificate holds by construction.

Lean code for Definition10.2.2●1 definition
  • defdefined in PropertyKindCalculus/QuantityClassification.lean
    complete
    def PropertyKindCalculus.Quantity.IsProduct {R : Type} [Mul R]
  [PropertyKindCalculus.ScalarCarrier R]
  {k₁ k₂ k : PropertyKindCalculus.KindOfProperty}
  (_h : PropertyKindCalculus.ProductKind k₁ k₂ k)
  (q : PropertyKindCalculus.Quantity k R)
  (a : PropertyKindCalculus.Quantity k₁ R)
  (b : PropertyKindCalculus.Quantity k₂ R) : Prop
    def PropertyKindCalculus.Quantity.IsProduct
  {R : Type} [Mul R]
  [PropertyKindCalculus.ScalarCarrier R]
  {k₁ k₂ k :
    PropertyKindCalculus.KindOfProperty}
  (_h :
    PropertyKindCalculus.ProductKind k₁ k₂
      k)
  (q : PropertyKindCalculus.Quantity k R)
  (a : PropertyKindCalculus.Quantity k₁ R)
  (b :
    PropertyKindCalculus.Quantity k₂ R) :
  Prop
    **The certificate.** `q` (of kind `k`) is the product of `a` (of `k₁`) and `b` (of
`k₂`): its magnitude is the product of theirs. A proof of this *certifies* `q`'s
classification as `k`, rather than merely asserting it. Kept a separate `Prop` so
`Quantity` stays a clean tag and certificates are carried only when needed.
Proof for Definition 10.2.2
uses 0

Quantity.IsProduct h q a b := q.magnitude = a.magnitude * b.magnitude over a carrier with multiplication; Quantity.mul h a b := ⟨a.magnitude * b.magnitude⟩, and mul_isProduct is rfl.

Theorem10.2.3
Group: The canonical pattern is the product , which covers a large fraction of the ISQ (area = length · length, volume = area · length, energy = force · length). The general machinery lives in the Mathlib-free core; the dimensional refinement ( k.dim = k₁.dim · k₂.dim ) lives in the dimension layer, and analysis-shaped relations (area as a surface integral) in the Mathlib-backed layer. (4)
Group member previews
Preview
Definition 10.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 0✓L∃∀N
EffortsmallTagsproved

A kind-law that instantiates at the quantity level. A quantity certified as the product of a and b is unique — and any certified product equals the smart-constructed one (eq_mul_of_isProduct, canonicity). Supplying concrete quantities gives the quantity-level fact by application. Axiom-free.

Lean code for Theorem10.2.3●1 theorem
  • theoremdefined in PropertyKindCalculus/QuantityClassification.lean
    complete
    theorem PropertyKindCalculus.Quantity.isProduct_unique {R : Type} [Mul R]
  [PropertyKindCalculus.ScalarCarrier R]
  {k₁ k₂ k : PropertyKindCalculus.KindOfProperty}
  (h : PropertyKindCalculus.ProductKind k₁ k₂ k)
  {q q' : PropertyKindCalculus.Quantity k R}
  {a : PropertyKindCalculus.Quantity k₁ R}
  {b : PropertyKindCalculus.Quantity k₂ R}
  (hq : PropertyKindCalculus.Quantity.IsProduct h q a b)
  (hq' : PropertyKindCalculus.Quantity.IsProduct h q' a b) : q = q'
    theorem PropertyKindCalculus.Quantity.isProduct_unique
  {R : Type} [Mul R]
  [PropertyKindCalculus.ScalarCarrier R]
  {k₁ k₂ k :
    PropertyKindCalculus.KindOfProperty}
  (h :
    PropertyKindCalculus.ProductKind k₁ k₂
      k)
  {q q' :
    PropertyKindCalculus.Quantity k R}
  {a : PropertyKindCalculus.Quantity k₁ R}
  {b : PropertyKindCalculus.Quantity k₂ R}
  (hq :
    PropertyKindCalculus.Quantity.IsProduct
      h q a b)
  (hq' :
    PropertyKindCalculus.Quantity.IsProduct
      h q' a b) :
  q = q'
    **A kind-law that instantiates at the quantity level.** A quantity certified as the
product of `a` and `b` is unique — supply any concrete `a`, `b` to get the
quantity-level fact by application.
Proof for Theorem 10.2.3
uses 0

isProduct_unique rewrites both magnitudes to a.magnitude * b.magnitude and closes by structure η; eq_mul_of_isProduct is isProduct_unique against mul_isProduct. Both depend on no axioms.

Definition10.2.4
Group: The canonical pattern is the product , which covers a large fraction of the ISQ (area = length · length, volume = area · length, energy = force · length). The general machinery lives in the Mathlib-free core; the dimensional refinement ( k.dim = k₁.dim · k₂.dim ) lives in the dimension layer, and analysis-shaped relations (area as a surface integral) in the Mathlib-backed layer. (4)
Group member previews
Preview
Definition 10.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 9
Reverse dependency previews
Preview
Theorem 23.5.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A quotient kind-law QuotientKind k₁ k₂ k records that k is the quotient kind k = k₁ / k₂ (speed = length / duration; plane angle = arc / radius, where the lengths cancel). Like the product, it carries the ratio-scale precondition in the core and is refined by k.dim = k₁.dim / k₂.dim in the dimension layer. Its certificate Quantity.IsQuotient and smart constructor Quantity.div mirror the product family exactly, over the core Div class.

Lean code for Definition10.2.4●1 definition
  • structure(3 fields)defined in PropertyKindCalculus/QuantityClassification.lean
    complete
    structure PropertyKindCalculus.QuotientKind
  (k₁ k₂ k : PropertyKindCalculus.KindOfProperty) : Prop
    structure PropertyKindCalculus.QuotientKind
  (k₁ k₂ k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    **A kind-level quotient law.** `k` is the *quotient kind* of `k₁` by `k₂`
(`k = k₁ / k₂`): all three are ratio-scale (the precondition for dividing quantities,
Dybkær §13.3.5). The Dimension layer strengthens this with `k.dim = k₁.dim / k₂.dim`.

    Fields

    ratio₁ : k₁.IsRational
    The dividend is ratio-scale. 
    ratio₂ : k₂.IsRational
    The divisor is ratio-scale. 
    ratioQuotient : k.IsRational
    The quotient is ratio-scale.
Proof for Definition 10.2.4
uses 0

structure QuotientKind with three IsRational fields; Quantity.div h a b := ⟨a.magnitude / b.magnitude⟩, div_isQuotient is rfl, and isQuotient_unique / eq_div_of_isQuotient are the product family's proofs transcribed. Axiom-free.

Definition10.2.5
Group: The canonical pattern is the product , which covers a large fraction of the ISQ (area = length · length, volume = area · length, energy = force · length). The general machinery lives in the Mathlib-free core; the dimensional refinement ( k.dim = k₁.dim · k₂.dim ) lives in the dimension layer, and analysis-shaped relations (area as a surface integral) in the Mathlib-backed layer. (4)
Group member previews
Preview
Definition 10.2.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0used by 1✓L∃∀N

A reciprocal kind-law ReciprocalKind k₁ k records that k = 1 / k₁ (frequency = 1 / period; curvature = 1 / radius; repetency = 1 / wavelength) — the unary special case, over the core Inv class, refined by k.dim = (k₁.dim)⁻¹. All three families (product, quotient, reciprocal) stay Mathlib-free, using only toolchain-level arithmetic classes.

Lean code for Definition10.2.5●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/QuantityClassification.lean
    complete
    structure PropertyKindCalculus.ReciprocalKind
  (k₁ k : PropertyKindCalculus.KindOfProperty) : Prop
    structure PropertyKindCalculus.ReciprocalKind
  (k₁ k :
    PropertyKindCalculus.KindOfProperty) :
  Prop
    **A kind-level reciprocal law.** `k` is the *reciprocal kind* of `k₁`
(`k = 1 / k₁`): both ratio-scale (the precondition for inverting a quantity). The
Dimension layer strengthens this with `k.dim = (k₁.dim)⁻¹`.

    Fields

    ratio₁ : k₁.IsRational
    The base kind is ratio-scale. 
    ratioReciprocal : k.IsRational
    The reciprocal is ratio-scale.
Proof for Definition 10.2.5
uses 0

structure ReciprocalKind with two IsRational fields; Quantity.recip h a := ⟨a.magnitude⁻¹⟩, recip_isReciprocal is rfl, with isReciprocal_unique / eq_recip_of_isReciprocal as before. Axiom-free.