9.1. The dedicated kind (Dybkær Ch. 20)
-
PropertyKindCalculus.Component[complete]
A component (§20) is the pertinent component of the sort of system a dedicated kind is about — water in a soil sample, glucose in plasma. Specified abstractly by identity, exactly mirroring the sort carrier.
Lean code for Definition9.1.1●1 definition
Associated Lean declarations
-
PropertyKindCalculus.Component[complete]
-
PropertyKindCalculus.Component[complete]
-
structuredefined in PropertyKindCalculus/DedicatedKind.leancomplete
structure PropertyKindCalculus.Component : Type
structure PropertyKindCalculus.Component : Type
**§20 component** — a pertinent component of the sort of system that a dedicated kind-of-property is about (e.g. *water* in a *soil* sample, *glucose* in *plasma*). Specified abstractly by identity, mirroring `SortOfSystem`.
Fields
id : String
Terminological identity of the component (mirrors the OML `id`).
A one-field structure with DecidableEq; nothing to prove.
-
PropertyKindCalculus.DedicatedKind[complete]
A dedicated kind-of-property (§20) bundles a sort of system, a component, and a kind-of-property. Its systematicTerm renders the three as System — Component ; kind, and it is a dedicated kind-of-quantity iff its underlying kind has magnitude (§13.3.1). dedicatedTo builds one from a bare kind.
Lean code for Definition9.1.2●1 definition
Associated Lean declarations
-
PropertyKindCalculus.DedicatedKind[complete]
-
PropertyKindCalculus.DedicatedKind[complete]
-
structuredefined in PropertyKindCalculus/DedicatedKind.leancomplete
structure PropertyKindCalculus.DedicatedKind : Type
structure PropertyKindCalculus.DedicatedKind : Type
**§20 dedicated kind-of-property** — "kind-of-property with given sort of system and any pertinent component." Its three projections are the IUPAC/IFCC `System — Component ; kind-of-property` triple, the `System` slot naming the sort.
Fields
sort : PropertyKindCalculus.SortOfSystem
The sort of system the dedicated kind is about — the definition's "given sort of system". The *particular* system is not stored here: it is the object index of the `IndividualQuantity` that instantiates this catalogue entry.
component : PropertyKindCalculus.Component
The pertinent component (§20).
kind : PropertyKindCalculus.KindOfProperty
The underlying generic kind-of-property (Ch. 6).
A three-field structure with DecidableEq. systematicTerm is string interpolation of the three ids; IsQuantity is the underlying kind's IsQuantity.
Dedicating a kind through an object: the object contributes exactly its sort, via the model's Sorted claim. This is the arrow from the individual layer to the catalogue — an individual quantity carries the particular in its type, and dedicatedFor says which catalogue entry that particular's readings instantiate. In the terms of the foundations chapter's ontological square, it is Lowe's dispositional route to exemplification: up the instantiated by edge, then across the top.
Lean code for Definition9.1.3●1 definition
Associated Lean declarations
-
defdefined in PropertyKindCalculus/DedicatedKind.leancomplete
def PropertyKindCalculus.KindOfProperty.dedicatedFor.{u} {O : Type u} [PropertyKindCalculus.Sorted O] (k : PropertyKindCalculus.KindOfProperty) (o : O) (component : PropertyKindCalculus.Component) : PropertyKindCalculus.DedicatedKind
def PropertyKindCalculus.KindOfProperty.dedicatedFor.{u} {O : Type u} [PropertyKindCalculus.Sorted O] (k : PropertyKindCalculus.KindOfProperty) (o : O) (component : PropertyKindCalculus.Component) : PropertyKindCalculus.DedicatedKind
Dedicate a kind through an **object**: the object contributes exactly its sort. This is the instantiation square closing — the individual layer carries the particular, the dedicated kind its sort — and `Sorted` is the model's claim about which sort that is. In square terms, Lowe's dispositional route to exemplification: up the *instantiated by* edge, then across the top.
dedicatedTo applied to Sorted.sortOf o.
Two objects of one sort dedicate to one kind. The catalogue entry cannot tell two rovers apart, and is not supposed to: individuation is the object index's job, where combining quantities across the two is a compile-time type error. This is the load-bearing half of the corrected §20 reading — dedication to the sort, individuation by the object.
Lean code for Theorem9.1.4●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/DedicatedKind.leancomplete
theorem PropertyKindCalculus.KindOfProperty.dedicatedFor_congr.{u} {O : Type u} [PropertyKindCalculus.Sorted O] {k : PropertyKindCalculus.KindOfProperty} {o₁ o₂ : O} (h : PropertyKindCalculus.Sorted.sortOf o₁ = PropertyKindCalculus.Sorted.sortOf o₂) (component : PropertyKindCalculus.Component) : k.dedicatedFor o₁ component = k.dedicatedFor o₂ component
theorem PropertyKindCalculus.KindOfProperty.dedicatedFor_congr.{u} {O : Type u} [PropertyKindCalculus.Sorted O] {k : PropertyKindCalculus.KindOfProperty} {o₁ o₂ : O} (h : PropertyKindCalculus.Sorted.sortOf o₁ = PropertyKindCalculus.Sorted.sortOf o₂) (component : PropertyKindCalculus.Component) : k.dedicatedFor o₁ component = k.dedicatedFor o₂ component
**Two objects of one sort dedicate to one kind.** The catalogue entry cannot tell two rovers apart, and is not supposed to: individuation is the object index's job, where combining quantities across the two is a type error.
Congruence: the two dedications differ only in the sort argument, and the hypothesis equates the sorts.
Same sort and component, a different kind-of-property: a distinct dedicated kind. This is the principled volumetric-versus-gravimetric distinctness. Both water contents are "Soil — Water", but volume fraction and mass fraction are different kinds-of-property, so the dedicated kinds differ — with the sort and component held identical, and without appeal to any hand-chosen identity string. This is exactly the discrimination an OWL2 reasoner cannot phrase.
Lean code for Theorem9.1.5●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/DedicatedKind.leancomplete
theorem PropertyKindCalculus.DedicatedKind.distinct_of_kind {d₁ d₂ : PropertyKindCalculus.DedicatedKind} (h : d₁.kind ≠ d₂.kind) : d₁ ≠ d₂
theorem PropertyKindCalculus.DedicatedKind.distinct_of_kind {d₁ d₂ : PropertyKindCalculus.DedicatedKind} (h : d₁.kind ≠ d₂.kind) : d₁ ≠ d₂
Two dedicated kinds that **agree on sort and component** but differ in the underlying kind-of-property are distinct. This is the *principled* form of the soil-moisture distinctness. Volumetric and gravimetric water content are the **same measurement target** — soil — water — examined as two different kinds-of-property (*volume fraction* vs *mass fraction*). They are distinct dedicated kinds **because the kinds-of-property differ**, not because of any hand-chosen identity string.
Assume the two dedicated kinds are equal; then their kind projections are equal by congruence, contradicting the hypothesis (intro he; apply h; rw [he]). The companion laws distinct_of_sort and distinct_of_component are the same one-line argument on the other two projections.
Same sort and kind, a different component: a distinct dedicated kind. The water content and the air content of soil share their sort of system and their kind-of-property, differing only in the component — and that alone makes them distinct dedicated kinds.
Lean code for Theorem9.1.6●1 theorem
Associated Lean declarations
-
theoremdefined in PropertyKindCalculus/DedicatedKind.leancomplete
theorem PropertyKindCalculus.DedicatedKind.distinct_of_component {d₁ d₂ : PropertyKindCalculus.DedicatedKind} (h : d₁.component ≠ d₂.component) : d₁ ≠ d₂
theorem PropertyKindCalculus.DedicatedKind.distinct_of_component {d₁ d₂ : PropertyKindCalculus.DedicatedKind} (h : d₁.component ≠ d₂.component) : d₁ ≠ d₂
Dedicated kinds with the same sort and kind-of-property but a different component are distinct (e.g. the water content vs. the air content of the same sort of soil sample).
Congruence on the component projection, exactly as for distinct_of_kind.