det_gamma_identity

The determinant identity $\det \mathbf{\Gamma }=\det {\mathbf{J}}_{{\nu }_e}^{\oplus }$

Why this identity matters

The coordinated transform $\mathbf{\Gamma }$ is the load-bearing change of coordinates of the whole control architecture: it maps the generalized velocities $[{\mathbf{v}}_b;{\mathbf{\omega }}_b;\dot{\mathbf{q}}]$ to the coordinated velocities $[{\mathbf{v}}_c;{\mathbf{\omega }}_b;{\mathbf{\nu }}_e^{\oplus }]$, and every reduced equation of motion is a congruence through it. The controller must invert it every step, and the singularity-handling layer watches ${\sigma }_{\min }(\mathbf{\Gamma })$ to know when that inversion is about to blow up.

The house equation sheet (~/Code/Inspection/GNC/equations/current_sota.md) states, at eq 2.6, that the closed-form inverse “exists iff ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ is nonsingular — $\mathbf{\Gamma }$ and ${\mathbf{J}}_{{\nu }_e}^{\oplus }$ go singular together, lower-right block”. The determinant identity is the sharp algebraic fact behind that sentence: not merely that the two matrices lose rank together, but that their determinants are equal, always, at every configuration. All the singular behavior of the $12\times 12$ transform is carried by its $6\times 6$ lower-right block. That is why watching the small block suffices — and it is the first thesis fact we push through a proof kernel.

So, what do we actually have to prove? Bear with me — the whole thing turns out to be a story about zeros in the right places.

Sources and provenance

• Block structure of $\mathbf{\Gamma }$: (~/Code/Inspection/GNC/equations/current_sota.md) eq 2.4, which transcribes eq 19 of Giordano, Ott & Albu-Schäffer, “Coordinated Control of Spacecraft’s Attitude and End-Effector for Space Robots” (IEEE RA-L 2019), bibkey giordano2019coordinated. Neither published typo of that paper (eq 31 sign, eq 34d block order) touches eq 19.
• Circumcentroidal Jacobian ${\mathbf{J}}_{{\nu }_e}^{\oplus }$: same sheet, eq 2.2 (Giordano eq 14).
• Implementation cross-check: Inspection/GNC/breve_controller.py:527-528 slices Gamma[0:3,0:3] = R_cb, Gamma[6:12,3:6] = G_omega_b, Gamma[6:12,6:] = J_plus — the code’s block layout matches eq 2.4.
• Block-triangular determinant: Horn & Johnson, Matrix Analysis, 2nd ed., §0.9.4 (partitioned matrices). We prove it from the Leibniz expansion below, so the document stands alone. Its formal counterparts are the Mathlib lemmas Matrix.det_fromBlocks_zero₂₁ and Matrix.det_fromBlocks_zero₁₂.
• Machine pre-check: exact rational SymPy verification at (~/Code/tasks/streams/leanpunov/scratch/check_det_gamma.py) — five trials over $\mathbb{Q}$ plus a counterfactual with $\det \mathbf{R}\ne 1$, all passing 2026-07-05.

A notation note before we start. The source sheet writes the cross-product operator as $[\mathbf{p}{]}^{\wedge }$; per house convention this document writes ${\mathbf{p}}^{\times }$ for the same $3\times 3$ skew-symmetric matrix.

The precise statement

Throughout, the arm is nonredundant: $n=6$ joints, so that $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 12}$ is square and its determinant is defined. (For $n\ne 6$ the transform is $12\times (6+n)$ and the identity is not even well-posed — the sheet’s §3 makes the same restriction before inverting.)

From eq 2.4, the transform is

$$\mathbf{\Gamma }=\left[\begin{array}{ccc}{\mathbf{R}}_{cb}& -{\mathbf{R}}_{cb}{\mathbf{p}}_{bc}^{\times }& {\mathbf{R}}_{cb}{\bar{\mathbf{J}}}_v\\ 0& \mathbf{E}& 0\\ 0& {\mathbf{G}}_{{\omega }_b}& {\mathbf{J}}_{{\nu }_e}^{\oplus }\end{array}\right]$$

with block rows and columns of sizes $3,3,6$. Here ${\mathbf{R}}_{cb}\in SO(3)$ is the rotation from the base frame to the CoM frame, $\mathbf{E}$ is the $3\times 3$ identity, ${\mathbf{p}}_{bc}\in {\mathbb{R}}^3$ the base-to-CoM vector, ${\bar{\mathbf{J}}}_v\in {\mathbb{R}}^{3\times 6}$ the mass-averaged linear Jacobian, ${\mathbf{G}}_{{\omega }_b}\in {\mathbb{R}}^{6\times 3}$ the base-angular coupling map, and ${\mathbf{J}}_{{\nu }_e}^{\oplus }\in {\mathbb{R}}^{6\times 6}$ the circumcentroidal Jacobian.

Theorem (determinant of the coordinated transform). For every configuration, $\det \mathbf{\Gamma }=\det {\mathbf{J}}_{{\nu }_e}^{\oplus }$.

Notice what the theorem does not need: nothing about the contents of the top-right blocks $-{\mathbf{R}}_{cb}{\mathbf{p}}_{bc}^{\times }$ and ${\mathbf{R}}_{cb}{\bar{\mathbf{J}}}_v$, and nothing about ${\mathbf{G}}_{{\omega }_b}$. The only facts that matter are the two zero blocks in the first column, the zero block to the right of $\mathbf{E}$, and $\det {\mathbf{R}}_{cb}=1$. This is what makes the identity robust: it survives any modeling change that preserves the block shape.

Scratch work — where the proof comes from

We want $\det \mathbf{\Gamma }$ to collapse onto the lower-right block. Working backward: if a square matrix has the shape

$$\mathbf{M}=\left[\begin{array}{cc}\mathbf{A}& \mathbf{B}\\ 0& \mathbf{D}\end{array}\right]$$

with $\mathbf{A}$ and $\mathbf{D}$ square, then $\det \mathbf{M}=\det \mathbf{A}\det \mathbf{D}$ — the block-triangular determinant fact. Can we see $\mathbf{\Gamma }$ that way? Yes, twice over:

1. Group rows and columns as $3+9$. The first block column of $\mathbf{\Gamma }$ is zero below ${\mathbf{R}}_{cb}$, so $\mathbf{\Gamma }=\left[\begin{array}{cc}{\mathbf{R}}_{cb}& \mathbf{T}\\ 0& \mathbf{L}\end{array}\right]$ where $\mathbf{T}\in {\mathbb{R}}^{3\times 9}$ collects both top-right blocks and $\mathbf{L}\in {\mathbb{R}}^{9\times 9}$ is the lower-right $2\times 2$ block grid.
2. Inside $\mathbf{L}=\left[\begin{array}{cc}\mathbf{E}& 0\\ {\mathbf{G}}_{{\omega }_b}& {\mathbf{J}}_{{\nu }_e}^{\oplus }\end{array}\right]$ the upper-right block is zero — the transposed variant of the same fact applies.

Then $\det \mathbf{\Gamma }=\det {\mathbf{R}}_{cb}\cdot \det \mathbf{E}\cdot \det {\mathbf{J}}_{{\nu }_e}^{\oplus }$, and the first two factors are $1$. The technique is a direct proof; all the content sits in the block-triangular lemma, so we prove that first, from the definition of the determinant, with no invertibility assumption anywhere.

Proof

Lemma (block-triangular determinant). Let $\mathbf{A}\in {\mathbb{R}}^{m\times m}$, $\mathbf{D}\in {\mathbb{R}}^{k\times k}$, and $\mathbf{B}\in {\mathbb{R}}^{m\times k}$, and set $\mathbf{M}=\left[\begin{array}{cc}\mathbf{A}& \mathbf{B}\\ 0& \mathbf{D}\end{array}\right]$. Then $\det \mathbf{M}=\det \mathbf{A}\det \mathbf{D}$, and the same holds for $\left[\begin{array}{cc}\mathbf{A}& 0\\ \mathbf{C}& \mathbf{D}\end{array}\right]$ by transposition.

Proof of the lemma. By the Leibniz expansion, the determinant of the $(m+k)\times (m+k)$ matrix $\mathbf{M}$ is the sum over all permutations $\sigma$ of $\{1,\dots ,m+k\}$ of the signed products $\mathrm{sgn}(\sigma ){\prod }_i{M}_{i\sigma (i)}$. Consider any permutation whose product is nonzero. For every row index $i>m$, the entry $M_{i\sigma (i)}$ lies in the bottom block row, where only the $\mathbf{D}$ columns are nonzero; hence $\sigma (i)>m$ for all $i>m$. Since $\sigma$ is a bijection and maps the $k$-element set $\{m+1,\dots ,m+k\}$ into itself, it maps that set onto itself, and therefore also maps $\{1,\dots ,m\}$ onto itself. Thus every contributing permutation splits as a pair $({\sigma }_1,{\sigma }_2)$, where ${\sigma }_1$ permutes the first $m$ indices and ${\sigma }_2$ the last $k$, with $\mathrm{sgn}(\sigma )=\mathrm{sgn}({\sigma }_1)\mathrm{sgn}({\sigma }_2)$ because the two blocks of transpositions do not interact. The sum factors accordingly:

$$\det \mathbf{M}=(\sum _{{\sigma }_1}\mathrm{sgn}({\sigma }_1)\prod _{i\le m}{A}_{i{\sigma }_1(i)})(\sum _{{\sigma }_2}\mathrm{sgn}({\sigma }_2)\prod _{j\le k}{D}_{j{\sigma }_2(j)})$$

which is precisely $\det \mathbf{A}\det \mathbf{D}$. For the lower-triangular variant, apply the result to ${\mathbf{M}}^{\top }$ and use $\det {\mathbf{M}}^{\top }=\det \mathbf{M}$. This completes the lemma. $\square$

Proof of the theorem. Group the rows and columns of $\mathbf{\Gamma }$ as $3+9$. Since the second and third block rows of eq 2.4 both carry $0$ in the first block column, the matrix has the shape of the lemma with $\mathbf{A}={\mathbf{R}}_{cb}$ and $\mathbf{D}=\mathbf{L}$, where the top-right $\mathbf{T}=[-{\mathbf{R}}_{cb}{\mathbf{p}}_{bc}^{\times }{\mathbf{R}}_{cb}{\bar{\mathbf{J}}}_v]$ plays the role of $\mathbf{B}$ and is not constrained in any way. By the lemma,

$$\det \mathbf{\Gamma }=\det {\mathbf{R}}_{cb}\cdot \det \mathbf{L}$$

Next, the $9\times 9$ block $\mathbf{L}$ carries $0$ in its upper-right position, so the lower-triangular variant of the lemma gives

$$\det \mathbf{L}=\det \mathbf{E}\cdot \det {\mathbf{J}}_{{\nu }_e}^{\oplus }$$

Since $\mathbf{E}$ is the identity, its determinant is $1$. Since ${\mathbf{R}}_{cb}$ is a rotation matrix — an element of $SO(3)$, the special orthogonal group, whose defining conditions are ${\mathbf{R}}^{\top }\mathbf{R}=\mathbf{E}$ and $\det \mathbf{R}=+1$ — its determinant is $1$ as well. Chaining the three equalities,

$$\det \mathbf{\Gamma }=1\cdot 1\cdot \det {\mathbf{J}}_{{\nu }_e}^{\oplus }=\det {\mathbf{J}}_{{\nu }_e}^{\oplus }$$

as desired. $\square$

Post-proof analysis

The moral. The transform $\mathbf{\Gamma }$ adds no singularities of its own. Its first two block coordinates — CoM translation re-expressed by a rotation, base angular velocity passed through untouched — are volume-preserving; every loss of rank, and indeed the entire determinant, is inherited from the circumcentroidal Jacobian. The controller’s practice of monitoring the small block is not an approximation but an identity.

What the identity does not say. Equal determinants do not mean equal conditioning: ${\sigma }_{\min }(\mathbf{\Gamma })$ and ${\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })$ are distinct quantities, and the sheet’s §6 reports their empirical Spearman rank correlation ($\ge 0.9969$) rather than an equality — singular values do not factor across block-triangular structure the way determinants do. The determinant identity pins the singular set exactly; the conditioning correlation remains an empirical (now well-understood) observation.

Could it be simpler? One could instead factor $\mathbf{\Gamma }$ into elementary block matrices, but that route needs invertibility hypotheses the Leibniz argument avoids. The permutation-splitting proof is the minimal one, and it is exactly the proof Mathlib’s Matrix.det_fromBlocks_zero₂₁ formalizes — the paper proof and the machine proof are the same proof.

Generality. Nothing above used real numbers: the argument holds over any commutative ring, with any block sizes, and with $\det {\mathbf{R}}_{cb}=1$ as the only hypothesis on the diagonal blocks besides $\mathbf{E}$ being the identity. The Lean statement is proved at that generality and then instantiated to the thesis shape ($3,3,6$ over $\mathbb{R}$).

The machine seal

Two machine checks accompany this derivation:

1. SymPy pre-check (house rule — fast, exact, falsifiable): (~/Code/tasks/streams/leanpunov/scratch/check_det_gamma.py) builds the full $12\times 12$ eq 2.4 structure with exact rational entries, a genuine rational rotation for ${\mathbf{R}}_{cb}$ (composed Pythagorean-triple rotations, $\det =1$ exactly), and the eq 2.2 form of ${\mathbf{G}}_{{\omega }_b}$. Five trials give $\det \mathbf{\Gamma }=\det {\mathbf{J}}_{{\nu }_e}^{\oplus }$ exactly over $\mathbb{Q}$; a counterfactual with $\mathbf{R}$ scaled so $\det =8$ shifts the result by exactly that factor, confirming the check has teeth.
2. Lean 4 seal (the external kernel check): DetGamma.lean in this directory states the theorem over an arbitrary commutative ring exactly as in the Generality note and proves it with Matrix.det_fromBlocks_zero₂₁, Matrix.det_fromBlocks_zero₁₂, Matrix.det_one, plus the $\det \mathbf{R}=1$ hypothesis; a corollary instantiates the thesis shape. The #print axioms output is recorded on the stream note (~/Code/tasks/streams/leanpunov.md).