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)))