21.8. Why it matters: classification and metrological consistency at the quantity level🔗

Formalizing a remark's mathematics is not decoration. It earns its keep by turning the quantity-kind into a working classifier and by moving metrological checking down to the quantity level, where the type system enforces it.

Classifying quantities. The surface-area formula does not return a bare real number: its output is, by construction, a magnitude of the one catalogued kind area. Any quantity a downstream model computes this way — the area of a field, a footprint, a cross-section — is automatically classified as the same kind, dimension L², unit the square metre. The kind is the genus under which every such quantity falls, and the defining relation is what places it there. So formalizing the remark gives users a principled answer to "what is this quantity?" — it is a value of area, because the relation that produced it is area's defining relation.

Verifying metrological consistency. Because the kind carries its dimension and its own scalar unit, the consistency checks happen at the quantity level and cannot be skipped. Two areas combine — addition is defined on the area carrier — but an area and a length are different types, so adding them does not type-check: the dimensionless numeric conflation a spreadsheet would silently allow is rejected. An area is not measurable in metres, because the square metre and the metre are not commensurable, a fact of the types rather than a runtime guard. And the dimensional invariant L² travels with every value of the kind. The remark's mathematics, the kind, and these consistency guarantees are thus one chain: the relation anchors the kind, the kind classifies the quantity, and the classification is the metrological check.

These claims are exercised as checked facts in the DimensionExamples library: a surface area built from the analytic element and classified as an area quantity, the L² invariant, the area-plus-area combination, and the rejected area-versus-length and square-metre-versus-metre conflations.

This is the verified instantiation requirement (R12): a classification is a certificate that a quantity satisfies its kind's defining relation, not a bare tag. For area, the defining relation is the surface element above, and it yields two concrete certificate forms.