Property Kind Calculus

About this technology

Overview

PropertyKindCalculus (PKC) is a formally verified metrology kernel implemented in the Lean 4 interactive theorem prover. It formalizes Ren Dybkr's An Ontology on Property for Physical, Chemical, and Biological Systems (2009) and David Flater's full tracking of kinds of quantities (NIST Technical Note 1943, Appendix C), and is the first artifact in which the quantity calculus - dimension arithmetic, the kind interaction algebra, scale-gated operations, extensivity, units, and their algebraic laws - is machine-checked, rather than only the taxonomy around itPKC continues a line of machine-checkable metrology modeling: OMG SysML QUDV (NTR 49755), then an OML/OWL2 metrology vocabulary grounded in Dybkr and the VIM (NTR 51720). That line established the taxonomy but reached the structural limit of description logic - dimension arithmetic alone had to be pushed into SPARQL, where it is brittle. PKC moves the model into dependent type theory, where kinds are first-class types, kind-incompatible arithmetic is a compile-time error, classification is a proof obligation, and every law is a theorem checked by the Lean kernel. The motivating defect it removes is the collapse of all dimension-one quantities - volumetric versus gravimetric water content, permittivity, reflectivity - under any dimension-only system, the exact silent-failure class in soil-moisture retrieval.The software is organized as seven Lake libraries so the core is exportable on its own: a Mathlib-free, toolchain-only ontological spine; a PhysLib-backed dimension/coherence layer in which dim is a forgetful homomorphism; a standards layer encoding eleven of the thirteen ISO/IEC 80000 parts item by item (700+ quantity-kinds, with the standards' Remarks formalized as defining relations); a TorchLean-backed instance of an executable/specification refinement bridge at IEEE-754 binary32; worked-example libraries; and a typed external-cross-reference layer. Thirteen metrology requirements are stated up front; twelve are discharged as machine-checked theorems and one (numeric unitconversion round-trip) is on the roadmap. The whole package builds with no unfinished proofs; the core is axiom-free.A Verso design blueprint renders to HTML and a paginated PDF in which each proved claim is linked to the declaration that discharges it - a self-verifying specification, suitable as the rigorous, auditable basis for any model whose correctness depends on getting physical quantities right. Downstream, PKC is the metrology foundation for verified soilmoisture retrieval; more broadly it serves any model that combines physical quantities and must not silently confuse them