A Property Kind Calculus for Measurement Metrology

3.5. How the calculus maps into Lean🔗

Two things in particular resist a DL encoding: the interaction algebra (which kind \times which kind = which kind, a partial relation with arithmetic side-conditions, not a role chain), and the difference between instantiation and subtyping (that a radius is a length, versus that this pencil's length is an instance of the length kind — conflated by punning in OWL). In Lean both map cleanly, and the mapping is the design:

  1. Kinds are type-level parameters. Quantity (k : KindOfProperty) (R : Type) — a kind indexes a type, not a value of one universal Quantity class, and a unit RealUnit k is a distinguished quantity of that same kind (the Units chapter), so "a metre" and "a unit of gravimetric water content" inhabit different types. This is the move OWL cannot make.

  2. Specialization (⊑) induces coercions between types. It lives on that parameter: Quantity Radius R → Quantity Length R is sound — a radius is a length — and the reverse is not. Up-casting to a parent kind is an explicit, visible loss of information.

  3. Instantiation is term-of-type, not subtyping. The length of a pencil is a term pencil : Quantity Length ℝ := .attest "read off the ruler" 5.2 — a value of that type, related to its kind by typing/instantiation, never by subtyping (and, being a mint, one of the boundary sites the audit enumerates). The general/individual distinction is the type/term distinction.

  4. The kind algebra is a partial typed algebra, not a group. PhysLib's Dimension is a total CommGroup — multiply, divide, invert anything. Kinds are not: Torque × Angle = Work is meaningful; Torque + Energy must be blocked even though the dimensions match; FuelConsumption × Rainfall is an error (Flater's own example). The meaningful products are encoded as a relation surfaced through typeclass resolution — Flater's "map kinds onto classes + operator overloading," lifted into Lean's elaborator.

  5. Dimension is a soundness functor, not the primary type. In QUDV and most quantity libraries dimension is the primary classifier: two quantities interoperate exactly when their dimensions agree — which is precisely the move that collapses every dimension-one quantity into one indistinguishable type. PropertyKindCalculus inverts the dependency: the kind is the primary type-level index, and dimension is recovered as a forgetful functor \dim : \mathrm{Kind} \to \mathrm{Dimension}. Its job is certification, not decision — the coherence theorem KMul k₁ k₂ k₃ → dim k₃ = dim k₁ · dim k₂ proves every product the kind algebra admits is dimensionally consistent — but dim never decides whether an operation is allowed; the kind relation does. Agreeing dimensions are necessary, not sufficient.

  6. Specialization (⊑) is a preorder — a lattice, not a tree. Flater stresses this (citing Formal Concept Analysis): a kind can specialize several parents. Unit-1 subtyping (Flater §6) is then just the dimension-1 slice of that kind lattice — and nothing forces it to be uniform: units of plane angle, for one, could carry their own subtyping reflecting the different measurement principles by which they are realized.

  7. The numeric carrier is a type parameter, bounded by a typeclass (R10). A scalar quantity is Quantity (k : KindOfProperty) (R : Type) with the arithmetic on R supplied by a Carrier typeclass — the kind fixes what is measured, R fixes in what numbers. Everything above R (kind discrimination, scale gating, the dimension functor, the interaction algebra, extensivity) is written once, against the typeclass, and is reused verbatim at every R (the additivity laws, for one, are proved a single time over any lawful carrier and hold at ℝ and Int with no per-carrier proof). This is the architecture TorchLean already runs: models are written against a Context α typeclass (arithmetic + transcendentals

    • comparison) and instantiated at α := ℝ for the spec, α := FP32 for the finite rounding model, and α := IEEE32Exec for the executable IEEE-754 kernel — the same source elaborated at three carriers. The kind layer here is the missing index above that carrier: TorchLean makes a tensor polymorphic in its scalar type; PropertyKindCalculus makes the scalar polymorphic in its kind, and the two indices compose. Crucially the carriers are bridged by refinement theorems (toReal (op_exec x) = round (op_real (toReal x))), so a law proved at \mathbb{R} is not stranded in the proof world — it descends to the float that runs. A description logic has no type parameters and no typeclasses, so this whole axis is unavailable to it; here it is the ordinary discipline of parametric polymorphism.

The trigger was concrete. PhysLib's Dimension makes all dimension-one quantities equal, so it cannot distinguish volumetric (\mathrm{L^3/L^3}) from gravimetric (\mathrm{M/M}) soil moisture, nor either from permittivity, reflectivity, or emissivity. Every dangerous soil-moisture confusion is dimension one. Indexing quantities and units by kind is what restores the distinction — this is the dimension-1 disambiguation capstone in the Units chapter.