3.4. Mechanization: what a dimension index still cannot separate🔗

The other line is mechanization, and its strongest prior result is a formalization of the ISQ and the SI in a proof assistant  (Foster and Wolff, 2023)Simon Foster and Burkhart Wolff (2023). “Automated Reasoning for Physical Quantities, Units, and Measurements in Isabelle/HOL”. 27th International Conference on Engineering of Complex Computer Systems (ICECCS). .: a quantity carries its dimension as a type index, so dimensionally incoherent arithmetic is rejected by the type checker rather than deferred to a run-time check.

That is a real calculus, and it is one this work carries too — as \dim, the forgetful functor of point 5 of the next subsection, whose job is to certify. What it is not is a kind layer. Indexing on the dimension collapses the fibers of \dim: volumetric and gravimetric water content, relative permittivity and reflectivity, torque and energy each share an index and are therefore one type, so the distinction a kind-of-property exists to draw cannot be stated there, let alone enforced. Neither do the axes that hang off a kind rather than off a dimension follow from it — the scale that decides which operators are defined, the interaction algebra, the dedicated kind, the aggregation laws. Dimensional coherence remains necessary; it was never sufficient.