Class DYAD


Slots on this class:

Documentation:
The class of second order tensors (aka tensors). Given an orthornormal basis a dyad can be decomposed into scalar components. These components can be represented as a square matrix. The matrix is not unique but it a 'view' of the tensor for a particular basis.
Instance-Of: Class
Subclass-Of: Constant-quantity, Tensor-quantity


Slots on instances of this class:

Tensor-Order: 2

Equivalence Axioms:

(<=> (Dyad ?D)
     (And (Constant-Quantity ?D)
          (Tensor-Quantity ?D)
          (= (Tensor-Order ?D) 2)
          (Forall (?B ?I ?J)
                  (=> (And (Orthonormal-Basis ?B)
                           (= (Basis.Dimension ?B)
                              (Spatial.Dimension ?D))
                           (Positive-Integer ?I)
                           (=< ?I (Spatial.Dimension ?D))
                           (Positive-Integer ?J)
                           (=< ?J (Spatial.Dimension ?D)))
                      (And (Defined (Dyad-Component ?D ?I ?J ?B))
                           (= (Quantity.Dimension (Dyad-Component ?D
                                                                  ?I
                                                                  ?J
                                                                  ?B))
                              (Quantity.Dimension ?D)))))
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (= (Quantity.Dimension ?U)
                              (Quantity.Dimension ?D)))
                      (Numeric-Tensor (Magnitude ?D ?U))))))


Axioms:

(Forall (?U)
        (=> (And (Unit-Of-Measure ?U)
                 (= (Quantity.Dimension ?U) (Quantity.Dimension ?D)))
            (Numeric-Tensor (Magnitude ?D ?U))))

(Forall (?B ?I ?J)
        (=> (And (Orthonormal-Basis ?B)
                 (= (Basis.Dimension ?B) (Spatial.Dimension ?D))
                 (Positive-Integer ?I)
                 (=< ?I (Spatial.Dimension ?D))
                 (Positive-Integer ?J)
                 (=< ?J (Spatial.Dimension ?D)))
            (And (Defined (Dyad-Component ?D ?I ?J ?B))
                 (= (Quantity.Dimension (Dyad-Component ?D ?I ?J ?B))
                    (Quantity.Dimension ?D)))))

(Tensor-Quantity ?D)

(Constant-Quantity ?D)


Other Related Axioms:

(<= (Tensor-Order $X 2) (Dyad $X))

(<=> (Dyad ?D)
     (And (Constant-Quantity ?D)
          (Tensor-Quantity ?D)
          (= (Tensor-Order ?D) 2)
          (Forall (?B ?I ?J)
                  (=> (And (Orthonormal-Basis ?B)
                           (= (Basis.Dimension ?B)
                              (Spatial.Dimension ?D))
                           (Positive-Integer ?I)
                           (=< ?I (Spatial.Dimension ?D))
                           (Positive-Integer ?J)
                           (=< ?J (Spatial.Dimension ?D)))
                      (And (Defined (Dyad-Component ?D ?I ?J ?B))
                           (= (Quantity.Dimension (Dyad-Component ?D
                                                                  ?I
                                                                  ?J
                                                                  ?B))
                              (Quantity.Dimension ?D)))))
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (= (Quantity.Dimension ?U)
                              (Quantity.Dimension ?D)))
                      (Numeric-Tensor (Magnitude ?D ?U))))))

(Nth-Domain Dyad-Component 1 Dyad)

(=> (= (Dyad-Component ?T ?I ?J ?Basis) ?S) (Dyad ?T))

(Nth-Domain The-Dyad 3 Dyad)

(=> (= (The-Dyad ?M ?B) ?T) (Dyad ?T))

(=> (And (Dyad ?X) (Dyad ?Y))
    (=> (+ ?X ?Y ?Z)
        (And (Dyad ?Z)
             (Forall (?B ?I ?J)
                     (=> (And (Orthonormal-Basis ?B)
                              (= (Spatial.Dimension ?X)
                                 (Basis.Dimension ?B))
                              (Positive-Integer ?I)
                              (Positive-Integer ?J)
                              (=< ?I (Spatial.Dimension ?X))
                              (=< ?J (Spatial.Dimension ?X)))
                         (= (Dyad-Component ?Z ?I ?J ?B)
                            (+ (Dyad-Component ?X ?I ?J ?B)
                               (Dyad-Component ?Y ?I ?J ?B))))))))

(=> (And (Vector-Quantity ?V1) (Dyad ?T1))
    (<=> (Dot ?V1 ?T1 ?V)
         (And (Vector-Quantity ?V)
              (Forall (?B)
                      (= ?T
                         (The-Vector-Quantity (* (Tensor-To-Matrix ?V1
                                                                   ?B)
                                                 (Tensor-To-Matrix ?T1
                                                                   ?B))
                                              ?B)))
              (Forall 
                  (?B ?I ?J)
                  (=> (= (Basis.Dimension ?B)
                         (Spatial.Dimension ?V1))
                      (= ?T
                         (Summation 
                             (Lambda 
                                 (?I)
                                 (* (Basis.Vec ?B ?I)
                                    (Summation 
                                        (Lambda (?J)
                                                (* (Vector-Component 
                                                       ?V1
                                                       ?J
                                                       ?B)
                                                   (Dyad-Component ?T1
                                                                   ?J
                                                                   ?I
                                                                   ?B)))
                                        1
                                        (Spatial.Dimension ?V1))))
                             1
                             (Spatial.Dimension ?V1))))))))

(=> (And (Dyad ?T1) (Vector-Quantity ?V1))
    (<=> (Dot ?T1 ?V1 ?V)
         (And (Vector-Quantity ?V)
              (Forall 
                  (?B)
                  (= ?T
                     (The-Vector-Quantity 
                         (Transpose (* (Tensor-To-Matrix ?T1 ?B)
                                       (Transpose (Tensor-To-Matrix 
                                                      ?V1
                                                      ?B))))
                         ?B)))
              (Forall 
                  (?B ?I ?J)
                  (=> (= (Basis.Dimension ?B)
                         (Spatial.Dimension ?V1))
                      (= ?T
                         (Summation 
                             (Lambda 
                                 (?I)
                                 (* (Basis.Vec ?B ?I)
                                    (Summation 
                                        (Lambda (?J)
                                                (* (Dyad-Component ?T1
                                                                   ?I
                                                                   ?J
                                                                   ?B)
                                                   (Vector-Component 
                                                       ?V1
                                                       ?J
                                                       ?B)))
                                        1
                                        (Spatial.Dimension ?V1))))
                             1
                             (Spatial.Dimension ?V1))))))))

(=> (And (Dyad ?T1) (Dyad ?T2))
    (<=> (Dot ?T1 ?T2 ?T)
         (And (Dyad ?T)
              (Forall (?B)
                      (= ?T
                         (The-Dyad (* (Tensor-To-Matrix ?T1 ?B)
                                      (Tensor-To-Matrix ?T2 ?B))
                                   ?B)))
              (Forall 
                  (?B ?I ?J)
                  (=> (= (Basis.Dimension ?B)
                         (Spatial.Dimension ?T1))
                      (= ?T
                         (Summation 
                             (Lambda 
                                 (?I)
                                 (Summation 
                                     (Lambda (?J)
                                             (* (* (Basis.Vec ?B ?I)
                                                   (Basis.Vec ?B ?J))
                                                (* (Dyad-Component ?T1
                                                                   ?I
                                                                   ?J
                                                                   ?B)
                                                   (Dyad-Component ?T2
                                                                   ?J
                                                                   ?I
                                                                   ?B))))
                                     1
                                     (Spatial.Dimension ?T1)))
                             1
                             (Spatial.Dimension ?T1))))))))

(Nth-Domain The-Zero-Dyad-Of-Type 3 Dyad)

(=> (= (The-Zero-Dyad-Of-Type ?Spatdim ?Physdim) ?V0)
    (Forall (?V)
            (=> (Dyad ?V)
                (= (Dot ?V ?V0)
                   (The-Zero-Scalar-For-Dimension ?Physdim)))))

(<- (Dyad-Of-Dimensions ?Physim ?Spatdim)
    (If (And (Physical-Dimension ?Physim)
             (Positive-Integer ?Spatdim))
        (Kappa (?Vq)
               (And (Dyad ?Vq)
                    (= (Spatial.Dimension ?Vq) ?Spatdim)
                    (= (Quantity.Dimension ?Vq) ?Physim)))))