3. Why a calculus, not a taxonomy🔗

PropertyKindCalculus continues two lines of machine-checkable metrology modeling — the descriptive one, which runs from QUDV through an OML vocabulary to SysML v2, and the mechanized one, which indexes quantities by dimension inside a proof assistant — and inherits its problem statement from exactly where each of them stops.

1. 3.1. From QUDV to an OML metrology vocabulary
2. 3.2. What a description logic cannot express
3. 3.3. SysML v2: a quantity model organized by value representation
4. 3.4. Mechanization: what a dimension index still cannot separate
5. 3.5. How the calculus maps into Lean