LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Derivative rules for differentiable matrix-valued curves, and skewness of $R^{T} R^{'}$ for a curve in $S O (3)$

Statement

Let $I \subseteq R$ be an interval with at least two points, let $t_{0} \in I$ and let $A, B : I \to M_{3} (R)$ be differentiable at $t_{0}$ , meaning (The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations) that every entry function $t \mapsto A (t)_{i j}$ and $t \mapsto B (t)_{i j}$ is differentiable at $t_{0}$ in the sense of The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set; write $A^{'} (t_{0})$ for the matrix with entries $A^{'} (t_{0})_{i j} : = (t \mapsto A (t)_{i j})^{'} (t_{0})$ , and similarly for $B$ .

$A + B$ and $A^{T}$ are differentiable at $t_{0}$ , with $(A + B)^{'} (t_{0}) = A^{'} (t_{0}) + B^{'} (t_{0})$ and $(A^{T})^{'} (t_{0}) = (A^{'} (t_{0}))^{T}$ .
$A B$ is differentiable at $t_{0}$ , with $(A B)^{'} (t_{0}) = A^{'} (t_{0}) B (t_{0}) + A (t_{0}) B^{'} (t_{0})$ .
If $A (t) \in S O (3)$ for every $t \in I$ (The orthogonal group $O (3)$ and the rotation group $S O (3)$ ), then the matrix $A (t_{0})^{T} A^{'} (t_{0})$ is skew-symmetric, i.e. $(A^{T} A^{'})^{T} = - A^{T} A^{'}$ at $t_{0}$ , and likewise $A^{'} (t_{0}) A (t_{0})^{T}$ is skew-symmetric. In particular the trace of each of these two matrices vanishes.

Facts & Assumptions

Given: An interval $I \subseteq R$ with at least two points, a point $t_{0} \in I$ , and maps $A, B : I \to M_{3} (R)$ differentiable at $t_{0}$ in the entrywise sense of the statement.

[L1]

If $f, g : I \to R$ are differentiable at $t_{0}$ and $α \in R$ , then $f + g$ , $α f$ and $f g$ are differentiable at $t_{0}$ with $(f + g)^{'} (t_{0}) = f^{'} (t_{0}) + g^{'} (t_{0})$ , $(α f)^{'} (t_{0}) = α f^{'} (t_{0})$ and $(f g)^{'} (t_{0}) = f^{'} (t_{0}) g (t_{0}) + f (t_{0}) g^{'} (t_{0})$ Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ .

[L2]

$M_{3} (R)$ is the function space of entries indexed by ${0, 1, 2} \times {0, 1, 2}$ with pointwise sum, so $(A + B)_{i j} = A_{i j} + B_{i j}$ ; the transpose is $(A^{T})_{i j} = A_{j i}$ ; and the product is $(A B)_{i j} = \sum_{k = 0}^{2} A_{i k} B_{k j}$ The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations, The transpose $A^{T}$ of a matrix, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes.

[L3]

Transposition is involutive and reverses products: $(A^{T})^{T} = A$ and $(A B)^{T} = B^{T} A^{T}$ Transpose is linear and involutive, and $(A B)^{T} = B^{T} A^{T}$ .

[L4]

For $R \in S O (3)$ one has $R^{T} R = I_{3}$ , $\det R = 1$ , $R$ invertible with $R^{- 1} = R^{T}$ , and also $R R^{T} = I_{3}$ The orthogonal group $O (3)$ and the rotation group $S O (3)$ , $S O (3)$ is a subgroup of the general linear group, with $R^{- 1} = R^{T}$ .

[L5]

A constant function $I \to R$ is differentiable at every point of $I$ with derivative $0$ : its difference quotient at any limit point of $I$ is the constant function $0$ , whose limit is $0$ The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set.

[L6]

The identity matrix $I_{3}$ has entries $1$ for equal indices and $0$ otherwise, and the matrix all of whose entries are $0$ is the zero matrix Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations.

Proof

technique · direct

1.1givenL1L2

For all $i, j$ the entry $(A + B)_{i j} = A_{i j} + B_{i j}$ is differentiable at $t_{0}$ with derivative $A_{i j}^{'} (t_{0}) + B_{i j}^{'} (t_{0})$ by [L1] and [L2]; these are the entries of $A^{'} (t_{0}) + B^{'} (t_{0})$ , so $A + B$ is differentiable with the asserted derivative.

1.2givenL1L2

For all $i, j$ the entry $(A^{T})_{i j} = A_{j i}$ is differentiable at $t_{0}$ with derivative $A_{j i}^{'} (t_{0})$ , which is the $(i, j)$ entry of $(A^{'} (t_{0}))^{T}$ ; so $A^{T}$ is differentiable with the asserted derivative.

1.3givenL1L2

For all $i, j$ the entry $(A B)_{i j} = \sum_{k = 0}^{2} A_{i k} B_{k j}$ is a finite sum of products of functions differentiable at $t_{0}$ , hence differentiable at $t_{0}$ with derivative $\sum_{k = 0}^{2} (A_{i k}^{'} B_{k j} + A_{i k} B_{k j}^{'})$ by two applications of [L1]; this sum is the $(i, j)$ entry of $A^{'} (t_{0}) B (t_{0}) + A (t_{0}) B^{'} (t_{0})$ by [L2]. Hence $A B$ is differentiable at $t_{0}$ with $(A B)^{'} = A^{'} B + A B^{'}$ .

2.1step 1.21.3givenL4L5L6

Assume $A (t) \in S O (3)$ for all $t \in I$ . By steps 1.2 and 1.3 the map $t \mapsto A (t)^{T} A (t)$ is differentiable at $t_{0}$ , with derivative $(A^{'})^{T} A + A^{T} A^{'}$ at $t_{0}$ . By [L4] this map is the constant map $t \mapsto I_{3}$ , and every entry of this constant entry function is constant, so by [L5] and [L2] its derivative at $t_{0}$ is the zero matrix [L6]. Hence $(A^{'})^{T} A + A^{T} A^{'} = 0$ at $t_{0}$ .

2.2step 1.32.1L3L4algebra

By [L4] and [L3] the map $t \mapsto A (t) A (t)^{T}$ is also the constant map $t \mapsto I_{3}$ , so step 1.3 gives $A^{'} A^{T} + A (A^{'})^{T} = 0$ at $t_{0}$ , and transposing with [L3] gives $(A^{'} A^{T})^{T} = - A^{'} A^{T}$ .

3.1step 2.1L3algebra

Transposing the identity of step 2.1 and using [L3] gives $A^{T} A^{'} + (A^{T} A^{'})^{T} = 0$ , hence $(A^{T} A^{'})^{T} = - A^{T} A^{'}$ , so $A^{T} A^{'}$ is skew-symmetric.

4.1step 3.12.2L2algebra∎

A skew-symmetric matrix has zero diagonal, hence trace $0$ : the $(i, i)$ entry satisfies $M_{i i} = - M_{i i}$ by step 3.1 applied entrywise, so $2 M_{i i} = 0$ in $R$ ; this applies to the two matrices of steps 3.1 and 2.2.

Derivative rules for differentiable matrix-valued curves, and skewness of $R^{T} R^{'}$ for a curve in $S O (3)$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Derivative rules for differentiable matrix-valued curves, and skewness of RTR′RTR′ for a curve in SO(3)SO(3)

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

Derivative rules for differentiable matrix-valued curves, and skewness of $R^{T} R^{'}$ for a curve in $S O (3)$