2.8. Verified classification: kind-laws that instantiate at the quantity level (R12)🔗

R12 — A classification is a certificate, not an assertion; kind-laws instantiate at the quantity level. By default a kind is a tag: Quantity k R records the kind but the magnitude is arbitrary, so a value can be labelled with a kind it has not earned. R12 upgrades a classification to a certificate — a proof that a quantity satisfies its kind's defining relation (the formalized ISO 80000 Remark) to quantities of the kinds it is built from. A length built as speed × time is certified by construction; a bare ⟨999⟩ cannot be certified against those factors. The kind becomes a refinement (a tag plus its earned proof).

The reason this strengthens the calculus is instantiation. Every kind-law is stated as a carrier-parametric universal over quantities with the kind-relation as a premise, so it instantiates to a quantity-level fact by ordinary application — the inter-kind generalization of R10's carrier-parametric laws — and any property of a kind's defining relation transports to every quantity certified under it (every certified surface area is ≥ 0, because the area element is). The pattern comes in three algebraic shapes — product (area = length · length, energy = force · length), quotient (speed = length / duration, plane angle = arc / radius), and reciprocal (frequency = 1 / period, curvature = 1 / radius) — each a kind-law family in the core; analysis-shaped relations such as area as a surface integral ∬ √g du dv follow the same discipline in the layer where their mathematics lives. These are exercised directly on ISO 80000-3's own Remarks (see the ISO 80000-3 chapter), where, for instance, the plane angle is computed to be dimension one because it is a ratio of two lengths. R12 unifies the two halves of the standards work: the formalized remark is the defining relation, and classification is the witnessed instantiation of it.