deruiter2021attitude

Attitude Representations and Identities (course notes)

Author: Anton H. J. de Ruiter · Year: 2021 (compile; revised 2022) · Venue: unpublished course notes, 8 pp. — no title page; authorship confirmed by the note owner 2026-07-09 Raw: md · pdf

Summary

A compact, self-contained development of attitude representation from first principles: vectrix resolution of physical vectors, the rotation matrix as the natural attitude representation, $SO(3)$ group properties (including the $\lambda =1$ eigenvalue via $\det [C-I]=0$), Euler rotations $C_a(\varphi )$ with a full proof of Euler’s theorem, the unit quaternion from the double-angle substitution, Poisson’s kinematics $\dot{C}=-{\omega }^{\times }C$, and — the notes’ distinctive content — the $S(p)$ / $\Gamma (p)$ machinery for arbitrary differentiable maps $C(p)\in SO(3)$ with the attitude-parameterization identities (16)–(21). Identity (20) is stated without proof; its proof (and the general $n$-parameter theory) is the subject of deruiter2014general. Every derivation is whiteboard-re-derivable; this is the substrate document for the SO(3) formalization arc (ctrllib Phase-4 recon).

Key Claims

• Rotation matrix as natural representation. Columns of $C_{bI}$ are the ${\mathcal{F}}_I$ basis vectors resolved in ${\mathcal{F}}_b$; every $C\in SO(3)$ is a rotational transformation (constructive proof via $c_3=c_1^{\times }{c}_2$ and the $\det [X]=x_1^{\top }{x}_2^{\times }{x}_3$ identity).
• Euler’s theorem (proved). Every $C\in SO(3)$ equals $C_a(\varphi )=\cos \varphi I+(1-\cos \varphi )a{a}^{\top }-\sin \varphi a^{\times }$ for some unit axis $a$, angle $\varphi$; proof by reduction to $R^{\top }CR=C_{e_1}(\varphi )$ using the $\lambda =1$ eigenvector.
• Kinematic-singularity definition. For any 3-parameter attitude set $p$: $\omega =S(p)\dot{p}$, and the singularity set is exactly where $S(p)$ loses invertibility — $|\dot{p}|\to \infty$ near it even for small $\omega$ (§1.6). For $n>3$ the constraint $\Phi (p)=0$ yields the stacked $[S^{\top }{\Xi }^{\top }{]}^{\top }$ system and its inverse block $\Gamma (p)$ with $S\Gamma =I$, $\Xi \Gamma =0$.
• Parameterization identities. $\frac{\partial }{\partial p^{\top }}[C(p)v]\Gamma (p)=[C(p)v{]}^{\times }$ (16) and the transpose form (18); reader-highlighted in the source. Final identity $(\dot{S}-\partial \omega /\partial p^{\top })\Gamma =-{\omega }^{\times }$ (20) unproven here — proved in the 2014 JAM paper.

Method

Direct matrix algebra throughout: no exterior calculus, no Lie-group formalism — everything reduces to $e_i$ manipulations, the cross-product-matrix identities $a^{\times }{b}^{\times }=b{a}^{\top }-(a^{\top }b)I$, $(Ca{)}^{\times }=C{a}^{\times }{C}^{\top }$, and constructive frame completions. This makes the content unusually close to what a Lean/Mathlib formalization would state and prove directly on Matrix (Fin 3) (Fin 3) ℝ.

Regime note. Generic rigid-body attitude; no manipulator dynamics — but §1.6 explicitly covers $C(p)$ with $p$ = joint angles of an $n$-link manipulator (the end-effector orientation map), which is the free-flying arm’s rotational kinematics verbatim.

Relevance to thesis

The boss’s own foundational notes — the theorem inventory for the robotics-notes formalization arc starts here (smallest self-contained document, everything provable with elementary Mathlib matrix machinery). Defines vectrix notation (§1.2), the provenance anchor for the vectrix research task. The $S(p)$-invertibility singularity definition connects to the project’s ${\sigma }_{\min }$ conditioning machinery (kinematic_singularity); the quaternion material grounds the attitude-error conventions of unit_quaternion.

Connections

Topics: Unit Quaternion · Kinematic Singularity · Exponential Coordinates Sources: giordano2019coordinated (consumes the quaternion error machinery) · deruiter2014general (the published proofs of the identity family)

Key Equations / Quotes

Euler rotation and the unit quaternion (source eqs 5, 7):

$C_a(\varphi )=\cos \varphi I+(1-\cos \varphi )a{a}^{\top }-\sin \varphi a^{\times }C=({\eta }^2-{ϵ}^{\top }ϵ)I+2ϵ{ϵ}^{\top }-2\eta {ϵ}^{\times }$

Kinematics for a parameterization $p$ (source eqs 9, 13):

$\omega =S(p)\dot{p}\dot{p}=\Gamma (p)\omega$

The unproven final identity (source eq 20, proved in deruiter2014general):

$\left(\dot{S}(p)-\frac{\partial \omega }{\partial p^{\top }}\right)\Gamma (p)=-{\omega }^{\times }$

Open Questions

• Which of eqs (5)–(21) exist in Mathlib already (e.g. Matrix.orthogonalGroup, quaternion API) vs need building? — the Phase-4 statement-shape recon answers this row by row.
• The source’s reader highlights (17)/(18)/(19) mark the identities the boss teaches from — confirm these are the recon’s first-priority targets.