6. The Proved Spine
This chapter records what PropertyKindCalculus already establishes, sorry-free, in its
Mathlib-free core. Every node here links to a real declaration with
(lean := "PropertyKindCalculus.…"), so its proved status in the dependency graph is
read directly from the checked library rather than asserted in prose.
The point to keep in view: each of these is a law or an operation, not a class
membership. A description-logic reasoner (OWL2/SROIQ) can record that width
specializes length; it cannot state, let alone prove, that specialization is
transitive or that operator availability is monotone in scale. Those are the
entries below. The systems those properties characterize — and the part–whole and
four-category structure they carry — are the foundations chapter's subject.
- 6.1. Scale — the operator-based division of ⟨property⟩ (Dybkær Ch. 12)
- 6.2. Kind-of-property and kind-of-quantity (Dybkær Ch. 6, 13)
- 6.3. Specialization and mutual comparability (OML / Dybkær §6)
- 6.4. Examination — principle, method, procedure (Dybkær Ch. 7, 14)
- 6.5. Property value and value scale (Dybkær Ch. 9, 16, 10, 17)
- 6.6. Metrological units (Dybkær Ch. 18, §13.3.3)