Class ORTHONORMAL-BASIS

• Defined in theory: Tensor-quantities
• Source code: tensor-quantities.lisp

Slots on this class:

Documentation:

A set of n vector-quantities in an n-dimensional vector space which form an ortho-normal basis, the n vector-quantities are linearly independent and the scalar product of any two is the identity-scalar.

Instance-Of: Class

Domain-Of: Basis.dimension

---

Slots on instances of this class:

Basis.Dimension:

Slot-Cardinality: 1

Axioms:

(Forall (?N1 ?N2)
        (=> (And (Positive-Integer ?N1)
                 (Positive-Integer ?N2)
                 (=< ?N1 (Basis.Dimension ?B))
                 (=< ?N2 (Basis.Dimension ?B)))
            (=> (= ?N1 ?N2)
                (= (Dot (Basis.Vec ?B ?N1) (Basis.Vec ?B ?N2)) 1))
            (=> (/= ?N1 ?N2)
                (= (Dot (Basis.Vec ?B ?N1) (Basis.Vec ?B ?N2)) 0))))

(Forall (?N)
        (=> (And (Positive-Integer ?N) (=< ?N (Basis.Dimension ?B)))
            (Defined (Basis.Vec ?B ?N))))

Other Related Axioms:

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

(<=> (Vector-Quantity ?V)
     (And (Constant-Quantity ?V)
          (Tensor-Quantity ?V)
          (= (Tensor-Order ?V) 1)
          (Forall (?B ?I)
                  (=> (And (Orthonormal-Basis ?B)
                           (= (Basis.Dimension ?B)
                              (Spatial.Dimension ?V))
                           (Positive-Integer ?I)
                           (=< ?I (Spatial.Dimension ?V)))
                      (And (Defined (Vector-Component ?V ?I ?B))
                           (= (Quantity.Dimension (Vector-Component ?V
                                                                    ?I
                                                                    ?B))
                              (Quantity.Dimension ?V)))))
          (Forall (?U)
                  (=> (And (Unit-Of-Measure ?U)
                           (= (Quantity.Dimension ?U)
                              (Quantity.Dimension ?V)))
                      (Numeric-Tensor (Magnitude ?V ?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)))))

(<=> (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 Basis.Vec 1 Orthonormal-Basis)

(=> (Basis.Dimension $X $Y) (Orthonormal-Basis $X))

(Nth-Domain Tensor-To-Matrix 2 Orthonormal-Basis)

(=> (= (Tensor-To-Matrix ?T ?Basis) ?M) (Orthonormal-Basis ?Basis))

(Nth-Domain Vector-Component 3 Orthonormal-Basis)

(=> (= (Vector-Component ?V ?I ?B) ?S) (Orthonormal-Basis ?B))

(Nth-Domain Dyad-Component 4 Orthonormal-Basis)

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

(Nth-Domain The-Vector-Quantity 2 Orthonormal-Basis)

(=> (= (The-Vector-Quantity ?M ?B) ?V) (Orthonormal-Basis ?B))

(Nth-Domain The-Dyad 2 Orthonormal-Basis)

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

(=> (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 ?X) (Vector-Quantity ?Y))
    (=> (+ ?X ?Y ?Z)
        (And (Vector-Quantity ?Z)
             (Forall (?B ?I)
                     (=> (And (Orthonormal-Basis ?B)
                              (= (Spatial.Dimension ?X)
                                 (Basis.Dimension ?B))
                              (Positive-Integer ?I)
                              (=< ?I (Spatial.Dimension ?X)))
                         (= (Vector-Component ?Z ?I ?B)
                            (+ (Vector-Component ?X ?I ?B)
                               (Vector-Component ?Y ?I ?B))))))))