LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

The product rule for quaternion and matrix curves, multiplicativity of the quaternion norm, and the conjugation formula $q φ (v) \overset{ˉ}{q} = φ ((a^{2} - ∥ u ∥^{2}) v + 2 ⟨ u, v ⟩ u + 2 a (u \times v))$

Statement

Let $I \subseteq R$ be a nondegenerate open interval, let $H$ be the quaternions, and let $φ : R^{3} \to Im H$ be the identification of The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts.

Product form and product rule. For $p = s + φ (u)$ and $q = t + φ (w)$ with $s, t \in R$ and $u, w \in R^{3}$ one has $p q = (s t - ⟨ u, w ⟩_{2}) + φ (s w + t u + u \times w)$ . If moreover $p, q : I \to H$ are of class $C^{1}$ (componentwise, $C^{k}$ Euclidean maps and diffeomorphisms), then $p q : I \to H$ is $C^{1}$ and $(p q)^{'} = p^{'} q + p q^{'}$ . Likewise, if $A, B : I \to M_{3} (R)$ are of class $C^{1}$ , then $A B$ is $C^{1}$ and $(A B)^{'} = A^{'} B + A B^{'}$ .
Conjugation and norm. For all $p, q \in H$ one has $\overline{p q} = \overset{ˉ}{q} \overset{ˉ}{p}$ and $N (p q) = N (p) N (q)$ , and $Re (p \overset{ˉ}{q}) = ⟨ p, q ⟩_{2}$ for $Re (x) : = x_{0}$ and the Euclidean inner product of The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ . For a $C^{1}$ curve $q : I \to H$ , the curves $\overset{ˉ}{q}$ and $N \circ q$ are $C^{1}$ with ${\overline{q}}^{'} = \overline{q^{'}}$ and

$(N \circ q)^{'} = 2 Re (q^{'} \overset{ˉ}{q}) = 2 ⟨ q^{'}, q ⟩_{2} .$

Conjugation formula. If $q = a + φ (u)$ with $a \in R$ and $u \in R^{3}$ , and $v \in R^{3}$ , then

$q φ (v) \overset{ˉ}{q} = φ ((a^{2} - ∥ u ∥_{2}^{2}) v + 2 ⟨ u, v ⟩_{2} u + 2 a (u \times v));$

in particular $q φ (v) \overset{ˉ}{q}$ is imaginary for every $q \in H$ , that is, its real part is $0$ . 4. Axis-angle form. If $N (q) = 1$ and $q = \cos (θ / 2) + φ (\hat{n}) \sin (θ / 2)$ with $θ \in R$ and $\hat{n} \in R^{3}$ , $∥ \hat{n} ∥_{2} = 1$ , then for every $v \in R^{3}$

$ρ (q) (φ (v)) = φ (\cos θ v + (1 - \cos θ) ⟨ \hat{n}, v ⟩_{2} \hat{n} + \sin θ (\hat{n} \times v)) .$

Facts & Assumptions

Given: The interval $I$ , the identification $φ$ of The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts, curves and vectors as in the clauses, and $q = a + φ (u) \in H$ with $a \in R$ , $u \in R^{3}$ .

[F1]

Quaternion multiplication is given by the explicit bilinear formula of The quaternions $H$ : real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$ ; writing $x = s + φ (w)$ and $y = t + φ (z)$ with $s, t \in R$ and $w, z \in R^{3}$ one has $x y = (s t - ⟨ w, z ⟩_{2}) + φ (s z + t w + w \times z)$ . The conjugate is $\overset{ˉ}{x} = s - φ (w)$ , the real norm is $N (x) = s^{2} + ∥ w ∥_{2}^{2}$ , and $\hat{N (x)} = x \overset{ˉ}{x} = \overset{ˉ}{x} x$ ; for $x \neq 0$ , $x^{- 1} = \hat{N (x)^{- 1}} \overset{ˉ}{x}$ . Every embedded real scalar $\hat{r}$ commutes with every quaternion (The quaternions $H$ : real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$ , $H$ is a division ring that is not commutative, hence not a field: $q^{- 1} = \overset{ˉ}{q} / N (q)$ for $q \neq 0$ , while $i j = k$ and $j i = - k$ ).

[F2]

For spatial vectors only, write $w_{j} : = w (j - 1)$ for $j = 1, 2, 3$ , so $(w_{1}, w_{2}, w_{3}) = (w (0), w (1), w (2))$ and $φ (w) = w_{1} i + w_{2} j + w_{3} k$ ; quaternion coordinates retain their indices $0, 1, 2, 3$ . The Euclidean inner product is $⟨ w, z ⟩_{2} = \sum_{j = 1}^{3} w_{j} z_{j}$ with $∥ w ∥_{2}^{2} = ⟨ w, w ⟩_{2}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ), and the cross product is given by $u \times v = (u_{2} v_{3} - u_{3} v_{2}, u_{3} v_{1} - u_{1} v_{3}, u_{1} v_{2} - u_{2} v_{1})$ with $⟨ u \times v, w ⟩_{2} = \det [u v w]$ , so that $(u \times v) \cdot u = (u \times v) \cdot v = 0$ (The cross product in $R^{3}$ , The cross product is bilinear, alternating, and orthogonal to both factors).

[F3]

A curve $f : I \to R^{n}$ is differentiable if and only if all its components are, and then $f^{'}$ is the componentwise derivative; sums and scalar multiples are differentiated componentwise (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral), and for real functions $(f g)^{'} = f^{'} g + f g^{'}$ (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$ ). A curve is of class $C^{1}$ when all components have continuous first derivatives ( $C^{k}$ Euclidean maps and diffeomorphisms).

[F4]

In this proof, for $A \in M_{3} (R)$ write $A_{i j} : = A (i - 1, j - 1)$ for $i, j = 1, 2, 3$ , relabeling the supplier indices $0, 1, 2$ . The entries of a matrix product are $(A B)_{i j} = \sum_{k = 1}^{3} A_{i k} B_{k j}$ (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes).

[F5]

For all real $x, y$ : $\sin (x + y) = \sin x \cos y + \cos x \sin y$ , $\cos (x + y) = \cos x \cos y - \sin x \sin y$ , and $\sin^{2} x + \cos^{2} x = 1$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[F6]

For unit $q \in S^{3}$ one has $q^{- 1} = \overset{ˉ}{q}$ and $ρ (q) = c_{q} ∣_{Im H}$ is $c_{q} (x) = q x \overset{ˉ}{q}$ (The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts).

Proof

technique · direct; finite coordinate expansions for the algebraic identities, then the product rule

1.1F1F2algebra

The multiplication formula of [F1] is bilinear over $R$ with integer coefficients, and in the form $x = s + φ (w)$ , $y = t + φ (z)$ it reads $x y = (s t - ⟨ w, z ⟩_{2}) + φ (s z + t w + w \times z)$ : the scalar part is $s t - (x_{1} y_{1} + x_{2} y_{2} + x_{3} y_{3}) = s t - ⟨ w, z ⟩_{2}$ and the three vector coordinates are $s z_{j} + t w_{j} + (w \times z)_{j}$ by the coordinate formula of the cross product in [F2].

1.2F1F2F3algebra

From [F1] the scalar part of $p \overset{ˉ}{q}$ is $\sum_{j = 0}^{3} p_{j} q_{j} = ⟨ p, q ⟩_{2}$ , which is the displayed identity $Re (p \overset{ˉ}{q}) = ⟨ p, q ⟩_{2}$ . If $q : I \to H$ is $C^{1}$ with components $q_{0}, \dots, q_{3}$ , then $\overset{ˉ}{q}$ has components $q_{0}, - q_{1}, - q_{2}, - q_{3}$ , which are $C^{1}$ with derivatives $q_{0}^{'}, - q_{1}^{'}, - q_{2}^{'}, - q_{3}^{'}$ , so $\overset{ˉ}{q}$ is $C^{1}$ and ${\overline{q}}^{'} = \overline{q^{'}}$ by [F3].

2.1step 1.1F1algebra

Both maps $(p, q) \mapsto \overline{p q}$ and $(p, q) \mapsto \overset{ˉ}{q} \overset{ˉ}{p}$ from $H \times H$ to $H$ are $R$ -bilinear; on the sixteen pairs of basis elements $1, i, j, k$ they agree — for instance $\overline{i j} = \overset{ˉ}{k} = - k$ and $\overset{ˉ}{j} \overset{ˉ}{i} = (- j) (- i) = j i = - k$ , and the remaining pairs are the same computation with signs — hence they agree on all of $H$ . Using the real embedding in [F1], $\hat{N (p q)} = (p q) \overline{(p q)} = p q \overset{ˉ}{q} \overset{ˉ}{p} = p \hat{N (q)} \overset{ˉ}{p} = \hat{N (q)} p \overset{ˉ}{p} = \hat{N (q)} \hat{N (p)} = \hat{N (p) N (q)}$ . The embedded scalar commutes with $p, \overset{ˉ}{p}$ by [F1], and $r \mapsto \hat{r}$ is injective by its first coordinate, so $N (p q) = N (p) N (q)$ in $R$ .

2.2step 1.1F1F2algebra

Write $q = a + φ (u)$ , $\overset{ˉ}{q} = a - φ (u)$ . By [step 1.1], $q φ (v) = - ⟨ u, v ⟩_{2} + φ (a v + u \times v)$ , so with $x : = - ⟨ u, v ⟩_{2} + φ (a v + u \times v)$ and $y : = a - φ (u)$ the product formula of [step 1.1] gives $q φ (v) \overset{ˉ}{q} = x y = (- ⟨ u, v ⟩_{2} a - ⟨ a v + u \times v, - u ⟩_{2}) + φ (⟨ u, v ⟩_{2} u + a (a v + u \times v) - (a v + u \times v) \times u)$ . The scalar part is $- a ⟨ u, v ⟩_{2} + (a ⟨ v, u ⟩_{2} + (u \times v) \cdot u) = 0$ , because $(u \times v) \cdot u = 0$ by [F2]. In the vector part, $- a (v \times u) = a (u \times v)$ . Writing $u = (u_{1}, u_{2}, u_{3})$ and $v = (v_{1}, v_{2}, v_{3})$ , the coordinate formula [F2] gives $(u \times v) \times u = ((u_{2}^{2} + u_{3}^{2}) v_{1} - u_{1} u_{2} v_{2} - u_{1} u_{3} v_{3}, (u_{1}^{2} + u_{3}^{2}) v_{2} - u_{1} u_{2} v_{1} - u_{2} u_{3} v_{3}, (u_{1}^{2} + u_{2}^{2}) v_{3} - u_{1} u_{3} v_{1} - u_{2} u_{3} v_{2}) = ∥ u ∥_{2}^{2} v - ⟨ u, v ⟩_{2} u$ . Substitution makes the vector part $(a^{2} - ∥ u ∥_{2}^{2}) v + 2 ⟨ u, v ⟩_{2} u + 2 a (u \times v)$ . This proves clause 3.

2.3step 1.1step 1.2F1F2F3F4algebra

Let $p, q : I \to H$ be $C^{1}$ . Each component of $p q$ is, by [step 1.1], a finite sum of terms $\pm p_{i} q_{j}$ ; each such term is differentiable with derivative $\pm (p_{i}^{'} q_{j} + p_{i} q_{j}^{'})$ by the real product rule in [F3], and derivatives of sums are sums of derivatives; the resulting derivative components are continuous because $p_{i}, q_{j}, p_{i}^{'}, q_{j}^{'}$ are continuous. Hence $p q$ is $C^{1}$ and $(p q)^{'} = p^{'} q + p q^{'}$ . For $C^{1}$ curves $A, B : I \to M_{3} (R)$ the same argument applies to the entries $(A B)_{i j} = \sum_{k} A_{i k} B_{k j}$ of [F4], giving $(A B)^{'} = A^{'} B + A B^{'}$ . If $q : I \to H$ is $C^{1}$ , the real-valued coordinate formula $N (q) = \sum_{j = 0}^{3} q_{j}^{2}$ and the real product rule give $(N \circ q)^{'} = 2 \sum_{j = 0}^{3} q_{j}^{'} q_{j} = 2 ⟨ q^{'}, q ⟩_{2} = 2 Re (q^{'} \overset{ˉ}{q})$ by [step 1.2]; thus $N \circ q$ is $C^{1}$ . The conjugate curve is $C^{1}$ by [step 1.2].

3.1step 2.2F5F6algebra∎

Under the hypotheses of clause 4, $N (q) = 1$ gives $a^{2} + ∥ φ (\hat{n}) \sin (θ / 2) ∥_{2}^{2} = 1$ and $q = a + φ (\hat{n}) \sin (θ / 2)$ with $a = \cos (θ / 2)$ ; by [F6] and [step 2.2], $ρ (q) (φ (v)) = q φ (v) \overset{ˉ}{q} = φ ((\cos^{2} (θ / 2) - \sin^{2} (θ / 2)) v + 2 \sin^{2} (θ / 2) ⟨ \hat{n}, v ⟩_{2} \hat{n} + 2 \cos (θ / 2) \sin (θ / 2) (\hat{n} \times v))$ . The addition formula of [F5] with $x = y = θ / 2$ gives $\cos θ = \cos^{2} (θ / 2) - \sin^{2} (θ / 2)$ and $\sin θ = 2 \sin (θ / 2) \cos (θ / 2)$ ; and $\sin^{2} (θ / 2) + \cos^{2} (θ / 2) = 1$ gives $2 \sin^{2} (θ / 2) = 1 - \cos θ$ . Substituting these three identities proves clause 4.

Remarks

Clause 3 is stated for arbitrary $q$ and is a purely algebraic identity; only in clause 4 and in the definition of $ρ$ is the unit condition used, through $q^{- 1} = \overset{ˉ}{q}$ . No division by $∥ u ∥_{2}$ or by the vector part of $q$ occurs anywhere, so $q = \pm 1$ is included.
The identity of clause 4 is the Rodrigues axis-angle formula in quaternion form: for $N (q) = 1$ , the linear map $ρ (q)$ fixes $φ (\hat{n})$ and rotates the plane ${\hat{n}}^{⊥}$ by the angle $θ$ . This is a computation about the map $ρ$ ; no statement about any physical rotation, its rate, or a choice of orientation is made by the lemma itself.
The multiplicativity $N (p q) = N (p) N (q)$ is used in the following lemma to estimate the quaternion angular-velocity equation, and the product rule is used to differentiate curves of rotations and of unit quaternions. Both are recorded here once in the form in which they are consumed.

The product rule for quaternion and matrix curves, multiplicativity of the quaternion norm, and the conjugation formula $q φ (v) \overset{ˉ}{q} = φ ((a^{2} - ∥ u ∥^{2}) v + 2 ⟨ u, v ⟩ u + 2 a (u \times v))$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The product rule for quaternion and matrix curves, multiplicativity of the quaternion norm, and the conjugation formula q φ(v) qˉ=φ((a2−∥u∥2)v+2⟨u,v⟩u+2a (u×v))qφ(v)qˉ​=φ((a2−∥u∥2)v+2⟨u,v⟩u+2a(u×v))

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

The product rule for quaternion and matrix curves, multiplicativity of the quaternion norm, and the conjugation formula $q φ (v) \overset{ˉ}{q} = φ ((a^{2} - ∥ u ∥^{2}) v + 2 ⟨ u, v ⟩ u + 2 a (u \times v))$