TheoremStatement: 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.

Existence, uniqueness and sign ambiguity of the quaternion lift of a $C^{1}$ rotation path

Statement

Let $I \subseteq R$ be a nondegenerate open interval, let $R : I \to S O (3)$ be of class $C^{1}$ (The orthogonal group $O (3)$ and the rotation group $S O (3)$ ) with body angular velocity $ω_{R}$ in the sense of The body angular velocity of a $C^{1}$ rotation path: $Ω = R^{T} R^{'}$ is skew, $Ω z = ω \times z$ determines a unique continuous $ω$ , and $R^{'} = R Ω$ , let $t_{0} \in I$ , and let $q_{0} \in S^{3}$ satisfy $ρ (q_{0}) = R (t_{0})$ , with $ρ$ and $S^{3}$ as in The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts. Then:

There is exactly one $C^{1}$ quaternion lift $q : I \to S^{3}$ of $R$ with $q (t_{0}) = q_{0}$ , namely the unique solution on $I$ of the initial value problem

$q^{'} (t) = \frac{1}{2} q (t) φ (ω_{R} (t)), q (t_{0}) = q_{0} .$

Every $C^{1}$ lift $\tilde{q} : I \to S^{3}$ of $R$ satisfies $\tilde{q} = q$ or $\tilde{q} = - q$ ; in particular $- q$ is the lift with initial value $- q_{0}$ , and $ρ \circ q = ρ \circ (- q) = R$ .

Facts & Assumptions

Given: The $C^{1}$ rotation path $R$ , its body angular velocity $ω_{R}$ , the times $t_{0} \in I$ , and the unit quaternion $q_{0}$ with $ρ (q_{0}) = R (t_{0})$ .

[F1]

$ρ (q_{0}) \in S O (3)$ for $q_{0} \in S^{3}$ ; the assignment $q \mapsto ρ (q)$ restricts to a surjective homomorphism $S^{3} \to S O (3)$ whose kernel is ${1, - 1}$ , and $ρ (- q) = ρ (q)$ ; in particular $ρ (1)$ is the identity (The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts, Definition and Remarks).

[F2]

For $q, q^{'} \in S^{3}$ one has $q q^{'} \in S^{3}$ , $(q q^{'})^{- 1} = q^{' - 1} q^{- 1}$ , and $q^{- 1} = \overset{ˉ}{q}$ because $\hat{N (q)} = q \overset{ˉ}{q} = \overset{ˉ}{q} q = 1_{H}$ ; the product of two $C^{1}$ quaternion curves is again $C^{1}$ . The unit and inverse assertions use $N (q q^{'}) = N (q) N (q^{'})$ , $x^{- 1} = \hat{N (x)^{- 1}} \overset{ˉ}{x}$ , and $S^{3} = {x : N (x) = 1}$ (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))$ clauses 1-2, 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$ , The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts).

[F3]

The body angular velocity $ω_{R} : I \to R^{3}$ is continuous and uniquely characterized by $R^{'} (t) = R (t) Ω_{ω_{R} (t)}$ , where $Ω_{ω}$ is the matrix $z \mapsto ω \times z$ (The body angular velocity of a $C^{1}$ rotation path: $Ω = R^{T} R^{'}$ is skew, $Ω z = ω \times z$ determines a unique continuous $ω$ , and $R^{'} = R Ω$ clauses 2-3).

[F4]

For continuous $ω : I \to R^{3}$ , $C^{1}$ $q : I \to H$ with $q^{'} = \frac{1}{2} q φ (ω (t))$ and $q (t_{0}) \in S^{3}$ : $q (I) \subseteq S^{3}$ , and $R = ρ \circ q$ is $C^{1}$ with $R^{'} = R Ω_{ω}$ ; moreover the initial value problem $q^{'} = \frac{1}{2} q φ (ω (t))$ , $q (t_{0}) = q_{0}$ with $q_{0} \in S^{3}$ has exactly one solution on $I$ (The quaternion lift of a prescribed continuous angular velocity: $q^{'} = \frac{1}{2} q φ (ω (t))$ keeps $S^{3}$ invariant, its rotation path has body angular velocity $ω$ , and the initial value problem has a unique solution on the whole interval clauses 1-2).

[F5]

A linear initial value problem $S^{'} = S Ω (t)$ on $M_{3} (R) ≅ R^{9}$ with continuous coefficient $Ω : I \to M_{3} (R)$ satisfies the Picard-Lindelöf hypotheses: being linear in the state variable with the continuous matrix coefficient $Ω (t)$ , the field is continuous and locally Lipschitz in the state variable, locally uniformly in time (Local Lipschitz continuity in the state variable, locally uniform in time and parameters, First-order systems, initial value problems, and solutions on intervals, The vector space $M_{m \times n} (F) : = F^{m \times n}$ of $m$ by $n$ matrices over a field, with entrywise operations); hence any two solutions through the same data agree on every common interval containing the initial time, and there is a unique maximal solution (Picard-Lindelöf local existence and uniqueness for first-order systems, Every Picard–Lindelöf initial value problem has one maximal solution on an open interval).

[F6]

If $f : A \to R$ is continuous on $A \subseteq R$ and $I \subseteq A$ is an interval, then the image $f [I]$ is order-convex: for $a, b \in f [I]$ with $a \leq b$ the whole segment $[a, b]$ lies in $f [I]$ (The image of an interval under a continuous real function is order-convex, hence an interval, and the image of a closed bounded interval is a closed bounded interval clause 1).

Proof

technique · direct; solve the quaternion equation through the lift lemma, then identify the rotation path through uniqueness for the linear matrix equation

1.1F3F4

The body angular velocity $ω_{R}$ is continuous by [F3], so [F4] applies with $ω = ω_{R}$ , $t_{0}$ and $q_{0} \in S^{3}$ : there is exactly one curve $q : I \to S^{3}$ of class $C^{1}$ with $q^{'} = \frac{1}{2} q φ (ω_{R} (t))$ on $I$ and $q (t_{0}) = q_{0}$ .

2.1step 1.1F3F4F5

Both $S : = R$ and $S : = ρ \circ q$ are $C^{1}$ curves $I \to M_{3} (R)$ solving the same linear initial value problem $S^{'} = S Ω_{ω_{R} (t)}$ , $S (t_{0}) = R (t_{0})$ : for $R$ this is the characterization in [F3], and for $ρ \circ q$ it is clause 1 of [F4] applied to the solution of step 1.1. By [F5] the coefficient is continuous and the equation satisfies the Picard-Lindelöf hypotheses, so two solutions through the same data agree on every common interval containing $t_{0}$ ; the interval $I$ is such a common interval, hence $ρ \circ q = R$ . Thus $q$ is a lift of $R$ with $q (t_{0}) = q_{0}$ .

3.1step 1.1step 2.1F1F2F6algebra∎

Let $\tilde{q} : I \to S^{3}$ be any $C^{1}$ lift of $R$ and put $h : = \tilde{q} q^{- 1} = \tilde{q} \overset{ˉ}{q} : I \to H$ , a product of two $C^{1}$ curves and hence $C^{1}$ by [F2]. By [F2], $h$ takes values in $S^{3}$ ; by the homomorphism property and kernel of [F1], $ρ (h) = ρ (\tilde{q}) ρ (q^{- 1}) = ρ (\tilde{q}) ρ (q)^{- 1} = R R^{- 1}$ , and this identity element of $S O (3)$ is $ρ (1)$ ; hence $h \in {1, - 1}$ for every $t \in I$ . The real part $Re \circ h : I \to R$ is continuous and takes its values in ${1, - 1}$ ; by [F6] applied to the interval $I$ its image is order-convex, so it cannot contain both $1$ and $- 1$ (the whole segment between them would lie in a two-point set), and $h$ is constant. At $t_{0}$ , $h (t_{0}) = \tilde{q} (t_{0}) q_{0}^{- 1}$ is $1$ when $\tilde{q} (t_{0}) = q_{0}$ and $- 1$ when $\tilde{q} (t_{0}) = - q_{0}$ ; thus the constant value gives $\tilde{q} = q$ in the first case and $\tilde{q} = - q$ in the second. Since $h (t_{0}) \in {1, - 1}$ , these are the only cases, so every lift is one of $q, - q$ . Finally, $- q$ is a $C^{1}$ curve into $S^{3}$ with initial value $- q_{0}$ and $ρ (- q) = ρ (q) = R$ by [F1]. This proves the uniqueness with each prescribed initial sign in clause 1 and the full assertion of clause 2.

Remarks

The two lifts $q$ and $- q$ solve the same differential equation with opposite initial data and define the same rotation path; the sign is therefore not determined by $R$ . Selecting one sign requires an initial choice, and no construction on this page selects a preferred sign.
The statement is conditional on the countable-choice hypothesis of the published covering example ex-su-two-to-so-three-as-a-covering-homomorphism recorded in The quaternion rotation map $ρ$ : conjugation on the imaginary quaternions, the unit sphere $S^{3}$ , and quaternion lifts, which is used through the covering and kernel facts of [F1] — that is, through the identification of $S^{3}$ with $S U (2)$ and the kernel ${1, - 1}$ . It is not used in the differential-equation part of the proof, which is choice-free.
Nothing in the statement asserts that the covering $S^{3} \to S O (3)$ is nontrivial, that a closed rotation loop has a closed lift, or that any global continuous sign selection exists; those questions are treated on the companion examples page.

Existence, uniqueness and sign ambiguity of the quaternion lift of a $C^{1}$ rotation path

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Existence, uniqueness and sign ambiguity of the quaternion lift of a C1C1 rotation path

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Existence, uniqueness and sign ambiguity of the quaternion lift of a $C^{1}$ rotation path