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.
(<=> (Magnitude ?Q ?Unit)
(And (Constant-Quantity ?Q)
(Unit-Of-Measure ?Unit)
(Dimensionless-Quantity ?Mag)
(Compatible-Quantities ?Q ?Unit)
(Defined (* ?Mag ?Unit))
(= (* ?Mag ?Unit) ?Q)))
(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)))))
(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) (= (* ?Mag ?Unit) ?Q))
(=> (= (Magnitude ?Q ?Unit) ?Mag) (Defined (* ?Mag ?Unit)))
(=> (= (Magnitude ?Q ?Unit) ?Mag) (Compatible-Quantities ?Q ?Unit))
(=> (= (Magnitude ?Q ?Unit) ?Mag) (Dimensionless-Quantity ?Mag))
(=> (= (Magnitude ?Q ?Unit) ?Mag) (Unit-Of-Measure ?Unit))
(=> (= (Magnitude ?Q ?Unit) ?Mag) (Constant-Quantity ?Q))
(=> (And (Constant-Quantity ?X) (Constant-Quantity ?Y))
(<=> (+ ?X ?Y ?Z)
(And (Constant-Quantity ?Z)
(Forall (?Unit)
(=> (Unit-Of-Measure ?Unit)
(= (+ (Magnitude ?X ?Unit)
(Magnitude ?Y ?Unit))
(Magnitude ?Z ?Unit)))))))
(Forall (@Args)
(<=> (And (Holds ?R @Args)
(=> (Item ?Q (Listof @Args))
(Constant-Quantity ?Q)))
(Forall (?Unit ?Q)
(=> (And (Unit-Of-Measure ?Unit)
(=> (Item ?Q (Listof @Args))
(Compatible-Quantities ?Q ?Unit)))
(Member (Map (Lambda (?Q)
(Magnitude ?Q ?Unit))
(Listof @Args))
?R)))))
(<=> (Relation-Extended-To-Quantities ?R)
(And (Relation ?R)
(Forall (@Args)
(<=> (And (Holds ?R @Args)
(=> (Item ?Q (Listof @Args))
(Constant-Quantity ?Q)))
(Forall (?Unit ?Q)
(=> (And (Unit-Of-Measure ?Unit)
(=> (Item ?Q (Listof @Args))
(Compatible-Quantities
?Q
?Unit)))
(Member (Map (Lambda
(?Q)
(Magnitude ?Q
?Unit))
(Listof @Args))
?R)))))))
(Forall (?Other-Unit)
(=> (And (Unit-Of-Measure ?Other-Unit)
(Compatible-Quantities ?U ?Other-Unit))
(And (Real-Number (Magnitude ?U ?Other-Unit))
(Positive (Magnitude ?U ?Other-Unit)))))
(<=> (Unit-Of-Measure ?U)
(And (Constant-Quantity ?U)
(Forall (?Other-Unit)
(=> (And (Unit-Of-Measure ?Other-Unit)
(Compatible-Quantities ?U ?Other-Unit))
(And (Real-Number (Magnitude ?U ?Other-Unit))
(Positive (Magnitude ?U ?Other-Unit)))))))
(<- (Magnitude-In-System-Of-Units ?Q ?System)
(Magnitude ?Q (Standard-Unit ?System (Quantity.Dimension ?Q))))