Slots on this function:

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.

Arity: 3


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