Function THE-ZERO-SCALAR-FOR-DIMENSION

• Defined in theory: Scalar-quantities
• Source code: scalar-quantities.lisp

Slots on this function:

Documentation:

The zero element for scalars of physical-dimension ?dimension. The real number 0 is the zero scalar-quantity for quantities of identity-dimension (i.e., dimensionless scalars). We make the distinction between 0 meters and 0 seconds, for instance, to maintain our compatibility requirements for operators such as addition (i.e. a length quantity + a length quantity always equals another length quantity). In practice, the distinction between zero quantities may not be important to any models, but there inclusion frees us from special cases for composition of quantities of different dimensions.

Instance-Of: Function

Arity: 2

Domain: Physical-dimension

Range: Scalar-quantity, Zero-quantity

Equivalence Axioms:

(<=> (The-Zero-Scalar-For-Dimension ?Dimension)
     (And (Physical-Dimension ?Dimension)
          (Scalar-Quantity ?Zero-Scalar)
          (Zero-Quantity ?Zero-Scalar)
          (Identity-Element-For 
              ?Zero-Scalar
              +
              (Scalar-Quantities-Of-Dimension ?Dimension))))

Axioms:

(= 0 (The-Zero-Scalar-For-Dimension Identity-Dimension))

Other Related Axioms:

(Forall (?D)
        (=> (Physical-Dimension ?D)
            (Abelian-Group (Scalar-Quantities-Of-Dimension ?D)
                           +
                           (The-Zero-Scalar-For-Dimension ?D))))

(Abelian-Group 
    (Kappa (?X)
           (And (Scalar-Quantity ?X)
                (Forall (?Dim)
                        (=> (Physical-Dimension ?Dim)
                            (/= (The-Zero-Scalar-For-Dimension ?Dim)
                                ?X)))))
    *
    1)

(=> (And (Scalar-Quantity ?X) (Recip ?X ?Y))
    (And (Scalar-Quantity ?Y)
         (Forall (?Dim)
                 (=> (/= ?X (The-Zero-Scalar-For-Dimension ?Dim))
                     (= (* ?X ?Y) Identity-Scalar)))))

(=> (The-Zero-Scalar-For-Dimension $X $Y) (Zero-Quantity $Y))

(=> (The-Zero-Scalar-For-Dimension $X $Y) (Scalar-Quantity $Y))

(=> (The-Zero-Scalar-For-Dimension $X $Y) (Physical-Dimension $X))

(=> (= (The-Zero-Scalar-For-Dimension ?Dimension) ?Zero-Scalar)
    (Identity-Element-For ?Zero-Scalar
                          +
                          (Scalar-Quantities-Of-Dimension ?Dimension)))

(=> (= (The-Zero-Scalar-For-Dimension ?Dimension) ?Zero-Scalar)
    (Zero-Quantity ?Zero-Scalar))

(=> (= (The-Zero-Scalar-For-Dimension ?Dimension) ?Zero-Scalar)
    (Scalar-Quantity ?Zero-Scalar))

(=> (= (The-Zero-Scalar-For-Dimension ?Dimension) ?Zero-Scalar)
    (Physical-Dimension ?Dimension))