2.6. Value representation: vectors and scalar units (R11)🔗

R11 — Units are scalar; a vector quantity is a numerical array times one scalar unit. Following ISO 80000-2 §18 (scalars, vectors and tensors), a vector (or tensor) quantity is written as a numerical vector multiplied by a single unit, and "all units are scalars" — not as a collection of per-coordinate quantity values each carrying its own number × unit; the quantity itself is independent of the coordinate system while its numerical components are not. This is exactly the R10 carrier taken at a numerical-array type: a vector quantity is Quantity (k : KindOfProperty) (Fin n → R) — one kind k, the numbers an n-vector in the carrier R, and one scalar MetrologicalUnit of the kind for the whole vector — and the additivity laws transfer to the vector carrier by the same parametric proof used for scalars (the pointwise Carrier (Fin n → R)). It is the ISO 80000-2 §18 numerical-array reading of value representation, and it aligns with the VIM's "a quantity is scalar; a vector/tensor is a composite of scalar quantities" — the priority SysML v2 inverts (see Why a calculus, not a taxonomy). The structural apparatus is a separate axis, specified as R20 below.

One consequence of the numerical-array reading needs stating here because it is a gate rather than a capability. A carrier supplying Mul is not thereby supplying the multiplication of magnitudes: Lean's Mul (Fin n → R) is pointwise, so the componentwise product of two position vectors would elaborate through Quantity.mul as a correctly kinded, correctly dimensioned area that is no physical quantity at all. ScalarCarrier is the carrier-side gate that refuses it — the missing half of the doctrine QuantityClassification already stated, that a kind's scale says an operation is meaningful while a carrier's tier says the representation can compute it. It is a marker class, and deliberately so: the same \iota \to R is a scalar carrier when its indices are independent samples (the batch carriers) and not when they are components, and no property of the type decides which. The operations §18 does license on a vector quantity — the scalar and vector products — are not pointwise and belong to R20.