The magnitude of a constant-quantity is a numeric value for the quantity given in terms of some unit-of-measure. For example, the magnitude of the quantity 2 kilometers in the unit-of-measure meter is the real number 2000. The unit-of-measure and quantity must be of the same physical-dimension, and the resulting value is a dimensionless-quantity. The type of the resulting quantity is dependent on the type of the original quantity. The magnitude of a scalar-quantity is a real-number, and the magnitude of a vector-quantity is a numeric-vector. In general, then, the magnitude function converts a quantity with dimension into a normal mathematical object.Units of measure are scalar quantities, and magnitude is defined in terms of scalar multiplication. The magnitude of a quantity in a given unit times that unit is equal to the original quantity. This holds for all kinds of tensors, including real-numbers and vectors. For scalar quantities, one can think of the magnitude as the ratio of a quantity to the unit quantity. See the definition of the multiplication operator * for the various sorts of quantities. The properties of * that hold for all physical-quantities are defined in this theory.
There is no magnitude for a function-quantity. Instead, the value of a function-quantity on some input is a quantity which may in turn be a constant-quantity for which the magnitude function is defined. See the definition of value-at.
(Nth-Domain Magnitude 3 Dimensionless-Quantity)
(Nth-Domain Magnitude 2 Unit-Of-Measure)
(Nth-Domain Magnitude 1 Constant-Quantity)
(Forall (?Q ?Unit ?Mag)
(=> (And (Constant-Quantity ?Q)
(Unit-Of-Measure ?Unit)
(Dimensionless-Quantity ?Mag)
(Defined (* ?Mag ?Q)))
(= (Magnitude (* ?Mag ?Q) ?Unit)
(* ?Mag (Magnitude ?Q ?Unit)))))
(<=> (Magnitude ?Q ?Unit ?Mag)
(And (Constant-Quantity ?Q)
(Unit-Of-Measure ?Unit)
(Dimensionless-Quantity ?Mag)
(Compatible-Quantities ?Q ?Unit)
(Defined (* ?Mag ?Unit))
(= (* ?Mag ?Unit) ?Q)))