A Property Kind Calculus for Metrology: proving quantity and unit laws in Lean, from ISO/IEC 80000 to measurement uncertainty🔗

Measurement begins with a judgment that two properties are mutually comparable — that it is meaningful to ask which of them is the greater, or by how much. Dybkær's ontology on property  (Dybkær, 2004)René Dybkær, 2004. An Ontology on Property for Physical, Chemical, and Biological Systems. PhD Thesis, University of Copenhagen takes that judgment as primitive and names what underwrites it: a kind-of-property is the "common defining aspect of mutually comparable properties" (§6.19). That is the first commitment, comparability: which properties are mutually comparable is something a model states, not a coincidence a reader may infer. Nearly everything else about a quantity hangs on it — the scale, which fixes whether =,<,+,\times are so much as defined between two values; the unit, which is one chosen value of one kind and of no other; and whether the values of the parts of a system bear on the value of the whole.

What a dimension contributes is real, and bounded. It records the SI base-quantity exponents of a kind and nothing else, and it records them homomorphically: the exponents of a product add. That is enough for dimensional analysis to do its work — to reject a length added to a time, to catch the formula that returned a rate where a total was wanted, to constrain the form of a law before its coefficients are known — by arithmetic alone, with no knowledge of what the quantities are quantities of. It is a genuine invariant, and worth keeping.

What a dimension cannot do is separate two kinds it sends to the same point, and the map that sends them is many-to-one by construction. Torque and energy both carry \mathrm{M\,L^2\,T^{-2}}, so no dimension check tells them apart. The limiting case is the quantities of dimension one  (Dybkær, 2004)René Dybkær (2004). “Units for quantities of dimension one”. Metrologia. 41(1)., the ones usually called dimensionless: every ratio of like quantities lands on the single point 1. Volumetric and gravimetric water content, relative permittivity, reflectivity, and all 115 characteristic numbers of ISO 80000-11 — Reynolds, Mach, and Prandtl among them — arrive there together. Inside that fiber dimensional analysis has no discriminating power left at all: it sees one type, a real number, for the whole family, and every substitution of one member for another is dimensionally correct. A language that checks dimensions therefore checks a necessary condition and reports it as a sufficient one — and what it admits, a gravimetric water content where a volumetric one was meant or a reflectivity where a permittivity was, does not halt the computation. It changes the number the computation returns.

A kind is a kind of something, and the second commitment, the bearer, concerns what that something is. Lowe's four-category ontology  (Lowe, 2005)E. J. Lowe (December 2005). “The Four-Category Ontology: A Metaphysical Foundation for Natural Science”. Oxford University Press. . supplies the categorial frame Dybkær's vocabulary implies but never names. Two cuts make the four categories — universal against particular, and substantial, a thing, against non-substantial, a way a thing is — and every term of measurement lands in exactly one of the quadrants they produce. Here is Lowe's square (his Fig. 7.1), with the calculus's identifier for each corner set beneath his own term and its mechanism on each edge:

The four corners, taken in the order the square draws them, top row first (the numbers are Lowe's):

• (3) Kinds — the substantial universal. A sort of system: soil, a reference cell, an antenna. What a thing is, said once for all things of that sort.

• (4) Attributes — the non-substantial universal. A kind-of-property, the comparability commitment above: volumetric water content in general, torque in general.

• (1) Substances — the substantial particular. The system at hand: this soil column, under this footprint, at this hour. Particular systems are the objects of measurement — whatever a measured value is a value of — and object is the word the rest of this document uses for a substance.

• (2) Modes — the non-substantial particular. An individual quantity: the volumetric water content of that column. Neither the general kind nor a bare number.

And the three relations, which are why this is a square and not a list of four boxes:

• Instantiation runs down the sides, universal to particular: a sort of system is instantiated by the systems of that sort, a kind-of-property by the individual quantities of that kind. Both edges are declared by a model; neither is inferred.

• Characterization runs across each row, left to right, substantial to non-substantial: below, a system is characterized by the individual quantities it bears; above, a sort of system is characterized by the kinds-of-property that apply to it — the edge along which a kind may be dedicated to a sort, water content of soil rather than water content at large. A dimension has no counterpart for either.

• Exemplification is the diagonal, and it is derived rather than primitive: an object exemplifies an attribute by going either way around the square, so the calculus needs no construct joining an object directly to a kind.

Two consequences are load-bearing. First, an individual quantity is a mode — the length of this pencil, not length in general — so a magnitude detached from what it characterizes is a number rather than a quantity, and the general kind is never the same entity as the individual measurement. Second, characterization is not parthood: properties characterize objects, they do not compose them. Dybkær says as much in his own voice, refusing a partitive reading of the object–property relation on the ground that a duplicate object cannot be produced by putting an object's properties together (§2.23.3).

Keeping those relations apart raises the third commitment, composition — the one an unstated convention damages most: what a carving of a system into parts does to a value. Marmodoro's distinction is that "physical structure unites; while metaphysical structure unifies", and that "wholes are not always unities"; a physical structure brings no principle of counting with it: "Alternative carvings of the world deliver alternative numbers of entities"  (Marmodoro, 2018)Anna Marmodoro, 2018. “Whole, but not One”. In Ontology, Modality, and Mind: Themes from the Metaphysics of E. J. Lowe (Oxford University Press).. A description of a whole into parts is one carving among many, and no arithmetic follows from having made it. That the masses of the parts sum to the mass of the whole while the volumes of mixed liquids do not is a claim about the kind — refutable by a measurement, and therefore worth proving rather than assuming.

Each of the three is a claim about the world rather than a convention adopted for convenience: a model states it, and a measurement can refute it.

• Comparability. Which properties share a kind-of-property, and may therefore be compared, added, or given a common unit. Put torque and energy under one kind — their dimensions raise no objection — and the model licenses a sum that denotes nothing.

• Bearer. What each kind is a kind of: the sort of system it is dedicated to, and the object an individual quantity characterizes. Leave it unstated and one system's water content stands in for another's without complaint.

• Composition. What a carving of a system into parts does to a value — which kinds aggregate over that carving, and by what law. Assume additivity everywhere and the volumes of mixed liquids refute the model.

A metrology taxonomy answers a different question. It records which kinds exist, with their dimensions and defining relations — a list of entries, and no list forbids the sum, dedicates the kind, or fixes the aggregation law. What has to be added is the calculus that operates on those kinds: dimension arithmetic, the algebra of which kinds interact and to what, operations gated by scale, aggregation laws quantified over every carving; parametricity enough that one model definition survives the several numeric carriers a quantity must inhabit; and a logic in which each such law is proved rather than documented.

We present PropertyKindCalculus (PKC) 0.113.0, a machine-checked formalization, in the Lean 4 proof assistant, of Dybkær's seminal contribution to metrology — read through Lowe's square — and of several recent developments in this field (Flater  (Flater, 2018)David Flater (2018). “Architecture for software-assisted quantity calculus”. Computer Standards & Interfaces. 56., Willink  (Willink, 2005)Robin Willink (2005). “A procedure for the evaluation of measurement uncertainty based on moments”. Metrologia. 42(5)., and Degenhardt  (Degenhardt et al., 2025)Johannes Degenhardt, Rainer Tutsch, Xiukun Hu, and Gaoliang Dai (2025). “A practically oriented, efficient alternative to the Monte Carlo method for measurement uncertainty estimation”. Metrologia. 62(2).). PKC makes a kind a first-class type, kind-incompatible arithmetic a compile-time error, and classification a proof obligation. Of twenty-eight metrology requirements, twenty say something that is either true or false of the calculus — that two kinds of the same dimension stay distinct, that converting a value to another unit and back returns it unchanged — and every one of those is proved as a theorem the Lean kernel checks. The other eight ask a different question: not whether something is true, but whether the language can express it at all — that a general kind and an individual quantity are different sorts of thing, that a unit is one chosen value of one kind. Each of those is met by a definition that compiles, and a type error is what its failure would look like. The standard is the test: all eleven quantity-and-unit parts of ISO/IEC 80000, item by item, 700+ kinds with checked dimensions and proved defining relations. Because a PKC model is carrier-polymorphic and its measurement uncertainty is an additive descriptor, one model definition serves proof, calculation, sensitivity analysis, and uncertainty quantification: what changes between the four is the carrier the model is instantiated at, never the model. That is the design principle we abbreviate write once, correctly; go fast, automatically. Measurement uncertainty, its propagation, and the coverage of the resulting interval are thereby machine-checked, while accuracy against nature — which needs a true value the kernel never has — remains an empirical matter; the boundary is exact, not rhetorical. The result is a modeling discipline whose specification documents — rendered from the checked sources — are verifiable rather than merely descriptive.

PKC is a library, and where it stands among the libraries it requires is worth drawing before anything is proved about it. A domain model written in the calculus traces its trust down through PhysLib, for dimensions and units, and cslib, for the labelled transition systems in which the capstone chapter states its bisimulation — the two peers on Mathlib — and through TorchLean, with FloatLib under it, for the tensor carriers and the executable float word, to Mathlib and then to the Lean kernel with its three classical axioms, the one band that is believed rather than derived, checked, or enumerated:

This blueprint is the design map for that formalization: every theorem node names the declaration that discharges it and reports that declaration's checked status, with the headline results tagged capstone. The dependency graph and a status summary come at the end.

What can the calculus do — what guarantee does a model earn by being written in it, stated as a theorem whose hypotheses the build discharges? Three capstone theorems answer that question, and they are the subject of the capstone chapter: the seal of a module — once its gates are declared, no other raw datum reaches its outputs; the seal of the computation — the same guarantee for the code at every carrier, with every kind change under an occurrence the source states; and dimensional homogeneity — dimension is a homomorphism along every path of a well-formed model. That chapter was written blueprint-first: the properties were architected and their proofs sketched there before the declarations were written, and every node now links the declaration that discharges it.

The whole blueprint is also available as a single paginated document: download the PDF.

The generated API reference for the checked sources is published alongside it: browse the API documentation. Declarations carrying @[pkc_math] render their defining equation as typeset mathematics there, next to the Lean source it was derived from.

Acknowledgment. The task "ROSE-L Soil Moisture Retrieval Using the SMAP and NISAR Algorithm", along with this research, was carried out at the Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.