2.3. Soundness bridges (R7, R8, R16, R17)🔗

R7 — Dimension certifies coherence; it does not decide legality. Every kind has a dimension, but dimension is a consistency check, not the authorization: matching dimensions are necessary yet never sufficient — which is exactly what lets R4 reject Torque + Energy. Formally the dimension map \dim : \mathrm{Kind} \to \mathrm{Dimension} is a forgetful functor and a homomorphism: \mathrm{KMul}\ k_1\ k_2\ k_3 \;\Longrightarrow\; \dim k_3 = \dim k_1 \cdot \dim k_2.

In plain engineering terms: \dim is a deliberately lossy, one-way translation from the rich kind layer down to the coarse SI-dimension layer. It keeps only the base-quantity exponents (length, mass, time, …) and forgets everything else, so many distinct kinds collapse onto the same dimension and there is no way back — that is what "forgetful" names. Calling it a homomorphism says the translation respects multiplication: the dimension of a product equals the product of the dimensions (the exponents add), so the kind layer and the dimension layer can never disagree about what multiplying means. It is the discipline of ordinary dimensional analysis, stated and proved as a law rather than performed by hand.

R8 — Units are chosen values of a kind; conversion is a faithful round-trip. A unit is a distinguished value of a kind (a metre is a chosen length), and a measured quantity is a number times a unit. Converting a quantity from one unit to another of the same kind and back is the identity — conversion is multiplication by a ratio, defined only within a kind. There is no conversion between units of different kinds; that too is a type error, not a runtime check.

R16 — Unit references are faithful. R8 states the capability; R16 and R17 are its proof obligations, split so each can be discharged exactly. R16 covers the reference side: commensurability of unit references is an equivalence relation, and the VIM's number-and-reference form of a quantity value round-trips — decompose a value into its number and its unit reference and recompose, and nothing is lost. Faithfulness here is what makes a recorded measurement citable: the reference is part of the value's identity, not a display convention.

R17 — Unit conversion between commensurable units is a faithful round-trip. The conversion side of R8's claim, made exact: converting between commensurable units is multiplication by an exact, reciprocal power-of-radix factor — SI decimal or IEC binary — so converting there and back is the identity on the nose, not up to floating-point error. The exactness is the point: a conversion factor that is a power of the radix commutes with the carrier's rounding, which is what lets the round-trip law hold at Float and not only at \mathbb{R}. R20's frame functoriality (toFrameVector_id, toFrameVector_comp) is this requirement's frame twin: what R17 proves for the unit axis, R20 proves for the frame axis.