1. What PropertyKindCalculus provides
This project addresses twenty-eight requirements about formalizing metrology — the science of measurement — and discharges most of them as machine-checked theorems rather than prose. A substantial part of the library is grounded directly on the published ISO and IEC 80000 metrology standards — eleven of the thirteen parts (every part but the two general ones, 1 General and 2 Mathematics), catalogued item by item. The table below is generated directly from the formalized catalogues, so its per-part counts and total stay in step with the Lean source:
Part | Title | Quantity kinds |
|---|---|---|
ISO 80000-3 | Space and time | 42 |
ISO 80000-4 | Mechanics | 54 |
ISO 80000-5 | Thermodynamics | 54 |
IEC 80000-6 | Electromagnetism | 85 |
ISO 80000-7 | Light and radiation | 66 |
ISO 80000-8 | Acoustics | 18 |
ISO 80000-9 | Physical chemistry and molecular physics | 62 |
ISO 80000-10 | Atomic and nuclear physics | 125 |
ISO 80000-11 | Characteristic numbers | 115 |
ISO 80000-12 | Condensed matter physics | 60 |
IEC 80000-13 | Information science and technology | 42 |
Total |
| 723 |