A Property Kind Calculus for Measurement Metrology

6.4. Examination — principle, method, procedure (Dybkær Ch. 7, 14)🔗

Definition6.4.1
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.2
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 0
Used by 17
Reverse dependency previews
Preview
Definition 6.4.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The examination chain has three layers — an examination principle (§7.5 / VIM4 2CD 2.4), a method based on a principle (VIM4 2CD 2.5), and a procedure based on a method (VIM4 2CD 2.7) — gathered into one carrier ExaminationItem so that refinement is a homogeneous relation. The forgetful projection basePrinciple sends any item down to the principle it rests on.

Lean code for Definition6.4.1●1 definition
  • structure(1 field)defined in PropertyKindCalculus/Examination.lean
    complete
    structure PropertyKindCalculus.ExaminationPrinciple : Type
    structure PropertyKindCalculus.ExaminationPrinciple :
  Type
    **§7.5 examination principle** (VIM4 2CD 2.4) — the phenomenon serving as the
basis of an examination. Carries a terminological `id` (OML-style).

    Fields

    id : String
    Terminological identity of the examination principle (OML-style).
Proof for Definition 6.4.1
uses 0

Three small structures with DecidableEq, united by an ExaminationItem inductive; basePrinciple is the projection to the principle layer.

Definition6.4.2
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 1✓L∃∀N

An examination method (Dybkær Ch. 7 / VIM4 2CD 2.5) is a generic description of an examination, based on an examination principle.

Lean code for Definition6.4.2●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/Examination.lean
    complete
    structure PropertyKindCalculus.ExaminationMethod : Type
    structure PropertyKindCalculus.ExaminationMethod :
  Type
    **Examination method** (Dybkær Ch. 7; VIM4 2CD 2.5) — a generic description of
an examination, *based on* an `ExaminationPrinciple`.

    Fields

    id : String
    Terminological identity of the examination method. 
    principle : PropertyKindCalculus.ExaminationPrinciple
    The principle this method is based on.
Proof for Definition 6.4.2
uses 0

A structure carrying an identifier and the ExaminationPrinciple it is based on.

Definition6.4.3
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N

An examination procedure (Dybkær Ch. 7 / VIM4 2CD 2.7) is a detailed description, based on an examination method; its principle is the method's principle.

Lean code for Definition6.4.3●1 definition
  • structure(2 fields)defined in PropertyKindCalculus/Examination.lean
    complete
    structure PropertyKindCalculus.ExaminationProcedure : Type
    structure PropertyKindCalculus.ExaminationProcedure :
  Type
    **Examination procedure** (Dybkær Ch. 7; VIM4 2CD 2.7) — a detailed
description, *based on* an `ExaminationMethod`.

    Fields

    id : String
    Terminological identity of the examination procedure. 
    method : PropertyKindCalculus.ExaminationMethod
    The method this procedure is based on.
Proof for Definition 6.4.3
uses 0

A structure carrying an identifier and the ExaminationMethod it is based on.

Definition6.4.4
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1
Used by 2
Reverse dependency previews
Preview
Theorem 6.4.5
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Refinement Refines is the reflexive–transitive closure of the "based-on" edges (a procedure is based on its method, a method on its principle): procedure ⊑ method ⊑ principle. It mirrors specialization over kinds — the same closure construction, one level down at the defining aspect.

Lean code for Definition6.4.4●1 definition
  • inductive(2 constructors, Prop, 2 parameters)defined in PropertyKindCalculus/Examination.lean
    complete
    inductive PropertyKindCalculus.Refines :
  PropertyKindCalculus.ExaminationItem →
    PropertyKindCalculus.ExaminationItem → Prop
    inductive PropertyKindCalculus.Refines :
  PropertyKindCalculus.ExaminationItem →
    PropertyKindCalculus.ExaminationItem →
      Prop
    **Refinement** of examinations: the reflexive–transitive closure of
`BasedOn`. A more specific examination *refines* a more generic one
(procedure ⊑ method ⊑ principle). Mirrors `Specializes` over kinds.

    Constructors

    PropertyKindCalculus.Refines.refl
  (a : PropertyKindCalculus.ExaminationItem) :
  PropertyKindCalculus.Refines a a
    Reflexivity of the closure: every examination refines itself. 
    PropertyKindCalculus.Refines.step
  {a b c : PropertyKindCalculus.ExaminationItem} :
  PropertyKindCalculus.BasedOn a b →
    PropertyKindCalculus.Refines b c →
      PropertyKindCalculus.Refines a c
    Prepend a based-on edge `BasedOn a b` to a refinement `b ⊑ c`.
Proof for Definition 6.4.4
uses 0

An inductive with refl and step constructors over a BasedOn edge relation; of_basedOn lifts a single edge.

Theorem6.4.5
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
OwnerNicolas RouquetteTagsproved

Refinement is a preorder. It is reflexive (the refl constructor) and transitive (Refines.trans) on the examination chain — the same algebraic law proved for specialization, which an OWL2 reasoner can neither state nor prove.

Lean code for Theorem6.4.5●1 theorem
  • theoremdefined in PropertyKindCalculus/Examination.lean
    complete
    theorem PropertyKindCalculus.Refines.trans
  {a b c : PropertyKindCalculus.ExaminationItem}
  (h₁ : PropertyKindCalculus.Refines a b)
  (h₂ : PropertyKindCalculus.Refines b c) :
  PropertyKindCalculus.Refines a c
    theorem PropertyKindCalculus.Refines.trans
  {a b c :
    PropertyKindCalculus.ExaminationItem}
  (h₁ : PropertyKindCalculus.Refines a b)
  (h₂ :
    PropertyKindCalculus.Refines b c) :
  PropertyKindCalculus.Refines a c
    Refinement is transitive (a preorder, together with `refl`).
Proof for Theorem 6.4.5
uses 0

Transitivity is by induction on the first derivation, exactly as for Specializes: refl returns the second derivation, step re-applies the constructor under the inductive hypothesis.

Theorem6.4.6
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.1
Loading preview
Group member preview content is loaded from the rendered-fragment cache.
uses 1used by 0✓L∃∀N
OwnerNicolas RouquettePriorityhighTagscapstoneproved

Refinement preserves the principle. Every examination in one refinement chain rests on the same base principle: \mathrm{Refines}\ a\ b \;\Longrightarrow\; \mathrm{basePrinciple}\ a = \mathrm{basePrinciple}\ b. The forgetful projection to the principle layer is invariant along refinement — the examination-layer analogue of \dim being a homomorphism, and one provable here in the Mathlib-free core without PhysLib. Builds on refinement.

Lean code for Theorem6.4.6●1 theorem
  • theoremdefined in PropertyKindCalculus/Examination.lean
    complete
    theorem PropertyKindCalculus.Refines.basePrinciple_eq
  {a b : PropertyKindCalculus.ExaminationItem}
  (h : PropertyKindCalculus.Refines a b) :
  a.basePrinciple = b.basePrinciple
    theorem PropertyKindCalculus.Refines.basePrinciple_eq
  {a b :
    PropertyKindCalculus.ExaminationItem}
  (h : PropertyKindCalculus.Refines a b) :
  a.basePrinciple = b.basePrinciple
    **Coherence — refinement preserves the principle.** Every examination in one
refinement chain rests on the *same* principle: a procedure, the method it is
based on, and the principle under that all share one base principle. The
forgetful projection `basePrinciple` is invariant along `Refines` — the
examination analogue of `dim` being a homomorphism, and a law no description
logic can phrase.
Proof for Theorem 6.4.6
uses 0

By induction on the refinement derivation: each BasedOn edge preserves the base principle (cases … <;> rfl), and the inductive step chains the resulting equalities.

Theorem6.4.7
Group: A kind-of-property is a "common defining aspect" (§6.19). One such defining aspect is how the property is examined : its examination principle (§7.5, VIM4 2CD 2.4) — the phenomenon serving as the basis — a method based on that principle (VIM4 2CD 2.5), and a procedure based on that method (VIM4 2CD 2.7). These refine one another and individuate kinds that scale and dimension alone cannot tell apart: width and height are both rational lengths, separated only by the principle under which each is examined. A description logic can record a link to a defining aspect; it cannot state that refinement is a preorder, nor that refinement preserves the principle. (6)
Group member previews
Preview
Definition 6.4.1
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 1✓L∃∀N
OwnerNicolas RouquetteTagsproved

The examination principle is a defining aspect. Two kinds examined by different principles are distinct kinds — independently of scale and dimension. This is what keeps width and height distinct while both remain rational lengths, mutually comparable under their shared super-kind Length.

Lean code for Theorem6.4.7●1 theorem
  • theoremdefined in PropertyKindCalculus/Examination.lean
    complete
    theorem PropertyKindCalculus.KindOfProperty.distinct_of_examPrinciple
  {k₁ k₂ : PropertyKindCalculus.KindOfProperty}
  (h : k₁.examPrinciple ≠ k₂.examPrinciple) : k₁ ≠ k₂
    theorem PropertyKindCalculus.KindOfProperty.distinct_of_examPrinciple
  {k₁ k₂ :
    PropertyKindCalculus.KindOfProperty}
  (h :
    k₁.examPrinciple ≠ k₂.examPrinciple) :
  k₁ ≠ k₂
    **§7.5 — the examination principle is a defining aspect.** Two kinds examined
by different principles are *distinct kinds* — independently of scale and (later)
dimension. This is what individuates otherwise-comparable kinds such as width and
height: same scale, same dimension, different examination principle, hence
different kinds.
Proof for Theorem 6.4.7
uses 0

The kinds differ in their examPrinciple field, so they are unequal by congruence: substitute the assumed kind-equality and derive a contradiction from the field inequality.