The Augmented Inertia Decouples the Self-Motion Coordinate

At a glance

A seven-joint arm on a free-flying base has one degree of freedom the mission never sees: the combined arm-and-base self-motion that leaves the twelve task coordinates frozen. To regulate it one appends a single inertia-weighted row to the wide task map $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 13}$, squaring it up to ${\mathbf{\Gamma }}_a\in {\mathbb{R}}^{13\times 13}$, and reads the dynamics in the new velocity coordinates. This page proves the geometric heart of that construction: the transformed inertia $\hat{\mathbf{M}}={\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1}$ is block-diagonal — the self-motion coordinate $v_n$ carries no kinetic-energy cross-terms with the twelve task coordinates, and its scalar inertia ${\hat{m}}_n={\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}$ is strictly positive. Seven results establish this: the self-motion sits at the last coordinate axis, its coupling column and its coupling row both vanish, every task velocity is inertia-orthogonal to it, and the diagonal scalar is well posed and positive. Lean’s kernel has checked all seven end-to-end on the three standard axioms [propext, Classical.choice, Quot.sound], with no sorry and — this is the point worth stressing — no open assumption: every hypothesis is a definitional given of the congruence transform or the construction of the appended covector, not an un-formalized analysis fact. The results live over an arbitrary commutative ring, using no matrix-inverse machinery; the concrete $13\times 13$ structure enters only through the symbolic and numerical cross-checks.

Links: module index · assumptions ledger · companion the passivity and null-space damping module · related the passivity-transport result · sources giordano2019coordinated, khatib1987unified, ott2008cartesian, nakamura1991advanced · pin test_seven_dof_p1_decoupling.py · derivation [(~/Code/generated_reports/math/derivation_7dof.md)]

Motivation

Giordano’s coordinated-control framing (giordano2019coordinated) certifies a free-flying manipulator by writing the dynamics in twelve task coordinates — the circumcentroidal split of centre-of-mass motion, base attitude, and end-effector pose — and closing the loop there. The framing carries an explicit restriction: “Let us assume a nonredundant manipulator.” A six-joint arm makes the coordinate map $\mathbf{\Gamma }$ square and invertible, and the whole argument runs.

A seven-joint arm breaks that convenience. The task map $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 13}$ now has thirteen columns and only twelve rows: it is wide, its kernel is one-dimensional, and it cannot be inverted. That extra kernel direction is the self-motion of the arm — the combined arm-and-base motion that changes nothing the mission watches. To regulate the self-motion, rather than let it drift, we need a velocity coordinate for it. The companion module (the passivity and null-space damping module) closes a damping loop on that coordinate and proves the closed loop converges; but the damping argument only earns its clean shape if the self-motion is inertially separated from the task in the first place. Supplying that separation, rigorously, is the job of this page.

The separation is not automatic. It is engineered by the choice of the appended row: the dynamically consistent, inertia-weighted covector of Khatib (khatib1987unified). The claim to be proved is the one the ratified derivation [(~/Code/generated_reports/math/derivation_7dof.md)] marks as the hard half of proof obligation P1: with this choice, the transformed inertia matrix block-diagonalizes, so there are no kinetic-energy cross-terms between the self-motion and the twelve task coordinates. Everything here is finite-dimensional linear algebra a reader can re-derive by hand — which is exactly why it is worth pinning down precisely what each step rests on.

The objects

The redundancy is resolved by making the wide map square. The one-dimensional self-motion is spanned by a vector $\hat{\mathbf{k}}\in {\mathbb{R}}^{13}$ in the kernel of $\mathbf{\Gamma }$; from the derivation’s block algebra (§3.2) it reads

$$\hat{\mathbf{k}}=\left[\begin{array}{c}-{\bar{\mathbf{J}}}_v\hat{\mathbf{n}}\\ 0_3\\ \hat{\mathbf{n}}\end{array}\right]\in {\mathbb{R}}^{13}\mathbf{\Gamma }\hat{\mathbf{k}}=0$$

where $\hat{\mathbf{n}}$ is the arm’s own null joint-rate direction, ${\bar{\mathbf{J}}}_v$ the mass-weighted link Jacobian, and the base counter-translates by exactly the mass-weighted arm motion so the centre of mass stays frozen. Append one row to $\mathbf{\Gamma }$ to obtain the square augmented map, and read the dynamics through the induced change of velocity coordinates:

$${\mathbf{\Gamma }}_a=\left[\begin{array}{c}\mathbf{\Gamma }\\ {\mathbf{z}}_a^{\top }\end{array}\right]\in {\mathbb{R}}^{13\times 13}{\mathbf{z}}_a^{\top }=\frac{{\hat{\mathbf{k}}}^{\top }\mathbf{M}}{{\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}}\hat{\mathbf{M}}={\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1}$$

Here $\mathbf{M}$ is the joint-space inertia matrix and ${\mathbf{z}}_a$ is the dynamically consistent (inertia-weighted) generalized inverse of Khatib (khatib1987unified): among all rows that would square up the map, this is the canonical one, because it is what makes the new coordinate inertially orthogonal to the task coordinates — the very fact this page proves. Kinetic energy is invariant under a change of velocity coordinates, so the inertia transforms by congruence, and $\hat{\mathbf{M}}$ carries the hat of that transform.

The abstract data. None of the seven results below needs the concrete $13\times 13$ structure, and none needs a matrix inverse. The module works over an arbitrary commutative ring $R$ with three pieces of data: a matrix $\mathbf{M}$ that is symmetric (${\mathbf{M}}^{\top }=\mathbf{M}$); a pair $(\mathbf{G},\mathbf{P})$ standing for $({\mathbf{\Gamma }}_a,{\mathbf{\Gamma }}_a^{-1})$, of which the only property used is the right-inverse relation $\mathbf{G}\mathbf{P}=1$; and an index $j$ marking the appended self-motion coordinate. Write ${\mathbf{e}}_n:=$ Pi.single j 1 for the corresponding basis vector (a one in slot $j$, zeros elsewhere) and

$$\hat{\mathbf{k}}:=\mathbf{P}{\mathbf{e}}_n$$

for the last column of the inverse (the vector the derivation calls ${\mathbf{c}}_{13}$). The scalar ${\hat{m}}_n:={\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}$ is the denominator of ${\mathbf{z}}_a$ (in Lean, denom). The bridge between the appended covector and the inertia is the single construction fact

$${\hat{m}}_n({\mathbf{G}}^{\top }{\mathbf{e}}_n)=\mathbf{M}\hat{\mathbf{k}}\text{equivalently}{\mathbf{z}}_a^{\top }=\frac{{\hat{\mathbf{k}}}^{\top }\mathbf{M}}{{\hat{m}}_n}$$

(in Lean, the hypothesis hrow): row $j$ of $\mathbf{G}$, scaled by ${\hat{m}}_n$, is $\mathbf{M}\hat{\mathbf{k}}$. This is the algebraic content of the derivation’s §4b, certified symbolically before any Lean by test_M_maps_khat_to_za_symbolic. That invertibility of ${\mathbf{\Gamma }}_a$ on the singularity-free region enters only as $\mathbf{G}\mathbf{P}=1$ is deliberate: it is the same ring-level discipline the companion passivity theorems keep, where the inverse is taken as a hypothesis rather than computed.

The results at a glance

Seven results, each pinned in SymPy or NumPy before formalization. The doc section is that of the derivation [(~/Code/generated_reports/math/derivation_7dof.md)]; the pin test lives in test_seven_dof_p1_decoupling.py.

result	statement	doc	pin test
gamma_a_khat_eq	${\mathbf{\Gamma }}_a\hat{\mathbf{k}}={\mathbf{e}}_n$ (the self-motion is the last coordinate axis)	§4b	test_gamma_a_khat_is_last_basis_symbolic
selfmotion_inertia_eq_denom	${\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}={\hat{m}}_n$ (the scalar self-motion inertia)	§4a, §4c	test_za_normalization_symbolic, test_M_maps_khat_to_za_symbolic
task_M_orthogonal	${\mathbf{z}}_a^{\top }\mathbf{c}=0\Rightarrow {\hat{\mathbf{k}}}^{\top }\mathbf{M}\mathbf{c}=0$ (task velocities are $\mathbf{M}$-orthogonal)	§4b	test_M_orthogonality_numeric
mhat_symm	${\hat{\mathbf{M}}}^{\top }=\hat{\mathbf{M}}$ (the congruence stays symmetric)	§4c	test_block_diagonal_inertia_numeric
mhat_selfmotion_column	$\hat{\mathbf{M}}{\mathbf{e}}_n={\hat{m}}_n{\mathbf{e}}_n$ (the coupling column vanishes)	§4c	test_p1_block_diagonal_symbolic, test_block_diagonal_inertia_numeric
mhat_selfmotion_row	${\mathbf{e}}_n^{\top }\hat{\mathbf{M}}={\hat{m}}_n{\mathbf{e}}_n^{\top }$ (the coupling row vanishes)	§4c	test_block_diagonal_inertia_numeric
selfmotion_inertia_pos	$0<{\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}$ (the diagonal scalar is positive)	§4a, §4c	test_za_denominator_positive_numeric

The self-motion is the last coordinate axis (gamma_a_khat_eq)

Everything downstream leans on one clean fact: in the new coordinates, the self-motion vector is the last coordinate direction. Applying the augmented map to $\hat{\mathbf{k}}$ returns the basis vector ${\mathbf{e}}_n$.

Strategy

The self-motion was defined as the last column of the inverse, $\hat{\mathbf{k}}=\mathbf{P}{\mathbf{e}}_n$. Feeding it back through $\mathbf{G}$ should undo the inverse and return ${\mathbf{e}}_n$ — provided $\mathbf{P}$ is a genuine right inverse. This is a direct calculation, needing nothing but $\mathbf{G}\mathbf{P}=1$; no size, symmetry, or positivity enters.

Proof

Substitute the definition of $\hat{\mathbf{k}}$ and collapse the product of a matrix with its right inverse:

$$\mathbf{G}\hat{\mathbf{k}}=\mathbf{G}(\mathbf{P}{\mathbf{e}}_n)=(\mathbf{G}\mathbf{P}){\mathbf{e}}_n=1\cdot {\mathbf{e}}_n={\mathbf{e}}_n$$

Therefore ${\mathbf{\Gamma }}_a\hat{\mathbf{k}}={\mathbf{e}}_n$, as claimed. The Lean proof is this exact chain, four rewrites over a commutative ring. $■$

What this shows

Unpacking the packed identity, ${\mathbf{\Gamma }}_a\hat{\mathbf{k}}={\mathbf{e}}_n$ says two things at once: the first twelve rows give $\mathbf{\Gamma }\hat{\mathbf{k}}=0$ — the self-motion is invisible to every task coordinate — and the last row gives ${\mathbf{z}}_a^{\top }\hat{\mathbf{k}}=1$ — the appended covector reads exactly unity on a unit self-motion, the normalization that fixes the one free scale of ${\mathbf{z}}_a$. So $\hat{\mathbf{k}}$ is precisely the column ${\mathbf{c}}_{13}$ of the inverse, confirmed numerically by test_gamma_a_invertible_and_c13_numeric.

The scalar self-motion inertia (selfmotion_inertia_eq_denom)

The block-diagonal $\hat{\mathbf{M}}$ has one nontrivial scalar in its self-motion slot. Before proving the off-diagonal blocks vanish, it is worth identifying that scalar with a physical quantity — and pinning the abstract denominator ${\hat{m}}_n$ of ${\mathbf{z}}_a$ to it.

Strategy

We want ${\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}={\hat{m}}_n$. Working backward, the construction fact hrow already expresses $\mathbf{M}\hat{\mathbf{k}}$ as ${\hat{m}}_n$ times ${\mathbf{G}}^{\top }{\mathbf{e}}_n$, so contracting with $\hat{\mathbf{k}}$ turns the quadratic form into ${\hat{m}}_n$ times a pairing that the previous result — $\mathbf{G}\hat{\mathbf{k}}={\mathbf{e}}_n$ — collapses to one. It is a short computation, a chain of dot-product rewrites.

Proof

Contract $\mathbf{M}\hat{\mathbf{k}}$ against $\hat{\mathbf{k}}$ and substitute the construction fact:

$${\hat{\mathbf{k}}}^{\top }(\mathbf{M}\hat{\mathbf{k}})={\hat{\mathbf{k}}}^{\top }({\hat{m}}_n({\mathbf{G}}^{\top }{\mathbf{e}}_n))={\hat{m}}_n\left({\hat{\mathbf{k}}}^{\top }{\mathbf{G}}^{\top }{\mathbf{e}}_n\right)={\hat{m}}_n({\mathbf{e}}_n^{\top }(\mathbf{G}\hat{\mathbf{k}}))$$

where the last step moves the transpose off $\mathbf{G}$ and rebrackets. By the previous result, $\mathbf{G}\hat{\mathbf{k}}={\mathbf{e}}_n$, so the trailing pairing is ${\mathbf{e}}_n^{\top }{\mathbf{e}}_n=1$, a single one from slot $j$ meeting itself. Hence

$${\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}={\hat{m}}_n\cdot 1={\hat{m}}_n$$

The Lean proof is a five-line calc chain that performs exactly these moves. $■$

What this shows

The scalar ${\hat{m}}_n={\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}$ is twice the kinetic energy of the self-motion at unit amplitude, and this result names it as the $(13,13)$ entry of the block-diagonal $\hat{\mathbf{M}}$. It ties the abstract scale ${\hat{m}}_n$ appearing in hrow to the physical self-motion inertia, through the normalization ${\mathbf{z}}_a^{\top }\hat{\mathbf{k}}=1$. Its positivity is the last result below.

Task velocities are inertia-orthogonal to the self-motion (task_M_orthogonal)

Now the geometric core. Reading row thirteen of the identity ${\mathbf{\Gamma }}_a{\mathbf{\Gamma }}_a^{-1}=\mathbf{E}$ against a task column gives the tautology ${\mathbf{z}}_a^{\top }{\mathbf{c}}_i=0$ — the appended covector reads zero on every task velocity, simply because it is a row of an identity matrix off its diagonal. The content is turning that tautology into a physical statement about the inertia.

Strategy

We want: if a velocity $\mathbf{c}$ is read as zero by the appended covector, meaning ${\mathbf{z}}_a^{\top }\mathbf{c}=0$ — in the module’s dot-product form, ${\mathbf{e}}_n^{\top }(\mathbf{G}\mathbf{c})=0$ — then it is $\mathbf{M}$-orthogonal to the self-motion, ${\hat{\mathbf{k}}}^{\top }\mathbf{M}\mathbf{c}=0$. The lever is again hrow, which rewrites $\mathbf{M}\hat{\mathbf{k}}$ as ${\hat{m}}_n{\mathbf{G}}^{\top }{\mathbf{e}}_n$; symmetry of $\mathbf{M}$ lets us move $\mathbf{M}$ from $\mathbf{c}$ onto $\hat{\mathbf{k}}$ first, so that the substitution can act.

Proof

Assume the velocity $\mathbf{c}\in {\mathbb{R}}^{13}$ satisfies ${\mathbf{e}}_n^{\top }(\mathbf{G}\mathbf{c})=0$, the statement that ${\mathbf{z}}_a$ reads it as zero. Since $\mathbf{M}$ is symmetric, the inertia pairing is itself symmetric, and we may move $\mathbf{M}$ onto the other factor:

$${\hat{\mathbf{k}}}^{\top }(\mathbf{M}\mathbf{c})=(\mathbf{M}\hat{\mathbf{k}}{)}^{\top }\mathbf{c}$$

Now substitute the construction fact $\mathbf{M}\hat{\mathbf{k}}={\hat{m}}_n({\mathbf{G}}^{\top }{\mathbf{e}}_n)$ and slide the transpose across:

$$(\mathbf{M}\hat{\mathbf{k}}{)}^{\top }\mathbf{c}={\hat{m}}_n({\mathbf{G}}^{\top }{\mathbf{e}}_n{)}^{\top }\mathbf{c}={\hat{m}}_n{\mathbf{e}}_n^{\top }(\mathbf{G}\mathbf{c})={\hat{m}}_n\cdot 0=0$$

Therefore ${\hat{\mathbf{k}}}^{\top }\mathbf{M}\mathbf{c}=0$: the velocity $\mathbf{c}$ is $\mathbf{M}$-orthogonal to the self-motion, as desired. $■$

What this shows

This is the derivation’s §4b bridge, and it is the single implication that carries all the physics. Because it holds for every task basis velocity ${\mathbf{c}}_i$ (whose ${\mathbf{z}}_a$-reading is zero by the off-diagonal identity), every one of them is inertia-orthogonal to $\hat{\mathbf{k}}$. Inertia-orthogonality of the task columns to the self-motion column is exactly the vanishing of the off-diagonal inertia blocks, which the next two results state directly. The numerical check test_M_orthogonality_numeric confirms ${\max }_i|{\hat{\mathbf{k}}}^{\top }\mathbf{M}{\mathbf{c}}_i|$ at the level of $10^{-14}$ across nine random configurations.

The congruence stays symmetric (mhat_symm)

A one-line structural fact, but a load-bearing one: it is what lets a single computation deliver both the vanishing column and the vanishing row.

Strategy

The transformed inertia is the congruence $\hat{\mathbf{M}}={\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}$ of a symmetric $\mathbf{M}$. A congruence of a symmetric matrix is symmetric — a direct proof: expand the transpose of the triple product and substitute ${\mathbf{M}}^{\top }=\mathbf{M}$.

Proof

Taking the transpose of the congruence and using that transposition reverses products and is an involution,

$$({\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}{)}^{\top }={\mathbf{P}}^{\top }{\mathbf{M}}^{\top }({\mathbf{P}}^{\top }{)}^{\top }={\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}$$

where the middle step used ${\mathbf{M}}^{\top }=\mathbf{M}$. Hence ${\hat{\mathbf{M}}}^{\top }=\hat{\mathbf{M}}$, over any commutative ring. $■$

What this shows

Symmetry is a basis-independent property. Here it does concrete work: once we show the self-motion column of $\hat{\mathbf{M}}$ vanishes off its diagonal, symmetry reflects that across the diagonal into the vanishing of the self-motion row, at no extra cost. The numerical pin also uses it in the reverse direction — it checks the $12\times 12$ task block ${\hat{\mathbf{M}}}_{\text{task}}$ is symmetric (test_block_diagonal_inertia_numeric).

The self-motion column decouples — the hard half of P1 (mhat_selfmotion_column)

This is the result the derivation marks “Proved above,” the hard half of proof obligation P1. It says the entire self-motion column of $\hat{\mathbf{M}}$ collapses to a single scalar on the diagonal: the task-from-self coupling block vanishes, and the diagonal entry is ${\hat{m}}_n$.

Strategy

Technique. Direct proof, following the derivation’s own forward route. We want $\hat{\mathbf{M}}{\mathbf{e}}_n={\hat{m}}_n{\mathbf{e}}_n$, where $\hat{\mathbf{M}}={\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}$. Working backward from the target, the natural moves are: fold $\mathbf{P}{\mathbf{e}}_n$ into $\hat{\mathbf{k}}$; use hrow to turn $\mathbf{M}\hat{\mathbf{k}}$ into ${\hat{m}}_n{\mathbf{G}}^{\top }{\mathbf{e}}_n$; and recognize ${\mathbf{P}}^{\top }{\mathbf{G}}^{\top }$ as $(\mathbf{G}\mathbf{P}{)}^{\top }=1$. Notice what is absent from that list: symmetry of $\mathbf{M}$ is not needed for the column at all.

Proof

Apply the congruence to the self-motion basis vector and walk it inward. First, $\mathbf{P}{\mathbf{e}}_n$ is by definition $\hat{\mathbf{k}}$, so

$$\hat{\mathbf{M}}{\mathbf{e}}_n={\mathbf{P}}^{\top }\mathbf{M}(\mathbf{P}{\mathbf{e}}_n)={\mathbf{P}}^{\top }\mathbf{M}\hat{\mathbf{k}}$$

The construction fact hrow rewrites the inner product $\mathbf{M}\hat{\mathbf{k}}$ as ${\hat{m}}_n({\mathbf{G}}^{\top }{\mathbf{e}}_n)$; pulling the scalar out front,

$${\mathbf{P}}^{\top }\mathbf{M}\hat{\mathbf{k}}={\mathbf{P}}^{\top }\left({\hat{m}}_n{\mathbf{G}}^{\top }{\mathbf{e}}_n\right)={\hat{m}}_n\left({\mathbf{P}}^{\top }{\mathbf{G}}^{\top }\right){\mathbf{e}}_n$$

Finally recognize the product ${\mathbf{P}}^{\top }{\mathbf{G}}^{\top }=(\mathbf{G}\mathbf{P}{)}^{\top }=1^{\top }=1$, using the right-inverse relation. Therefore

$$\hat{\mathbf{M}}{\mathbf{e}}_n={\hat{m}}_{n}1{\mathbf{e}}_n={\hat{m}}_n{\mathbf{e}}_n$$

which is the claim. In Lean the whole route is a single chain of rewrites; symmetry of $\mathbf{M}$ is never invoked. $■$

What this shows

The vector equation $\hat{\mathbf{M}}{\mathbf{e}}_n={\hat{m}}_n{\mathbf{e}}_n$ packs the entire self-motion column of the transformed inertia. Read entry by entry: the task-from-self coupling entries — rows $i\le 12$, column thirteen — are all zero, and the diagonal self-motion inertia is ${\hat{m}}_n$. There are no kinetic-energy cross-terms feeding the twelve task coordinates from the self-motion. This is the inertial decoupling the redundant-manipulator literature obtains from the dynamically consistent inverse (Khatib; Ott’s monograph on redundant arms, ott2008cartesian), here read directly off one column of the transformed inertia. The symbolic pin test_p1_block_diagonal_symbolic certifies the same identity for a generic inertia and a generic kernel, and the numeric test_block_diagonal_inertia_numeric confirms the off-diagonal block at $10^{-14}$.

And so does the row (mhat_selfmotion_row)

The column result has a mirror image, and symmetry hands it to us for free.

Strategy

We want the self-motion row of $\hat{\mathbf{M}}$ to vanish off its diagonal too: ${\mathbf{e}}_n^{\top }\hat{\mathbf{M}}={\hat{m}}_n{\mathbf{e}}_n^{\top }$. A row of a matrix is a column of its transpose, and $\hat{\mathbf{M}}$ equals its own transpose. So the row is the column, and we already have the column.

Proof

Reading the row-vector product as a column of the transpose, then substituting symmetry of $\hat{\mathbf{M}}$ from mhat_symm,

$${\mathbf{e}}_n^{\top }\hat{\mathbf{M}}={\hat{\mathbf{M}}}^{\top }{\mathbf{e}}_n=\hat{\mathbf{M}}{\mathbf{e}}_n$$

and the right-hand side is ${\hat{m}}_n{\mathbf{e}}_n$ by the column result mhat_selfmotion_column. Therefore ${\mathbf{e}}_n^{\top }\hat{\mathbf{M}}={\hat{m}}_n{\mathbf{e}}_n^{\top }$: the self-from-task coupling block — row thirteen, columns $i\le 12$ — vanishes. $■$

What this shows

Together with the column, this is the full statement that $\hat{\mathbf{M}}$ is block-diagonal:

$$\hat{\mathbf{M}}=\left[\begin{array}{cc}{\hat{\mathbf{M}}}_{\text{task}}& 0\\ 0^{\top }& {\hat{m}}_n\end{array}\right]$$

The self-motion coordinate $v_n$ decouples completely, in the inertia, from the twelve task coordinates. The elegance is that only the column needed a genuine argument; the row is the same computation viewed through the mirror of symmetry.

The self-motion block is nondegenerate (selfmotion_inertia_pos)

Block-diagonal is not yet the whole story: the lone scalar ${\hat{m}}_n$ could in principle be zero, which would leave ${\mathbf{z}}_a$ ill defined and the block degenerate. Over the reals, with a genuine inertia matrix, it cannot be.

Strategy

Technique. Direct, but with a small existence step. We want $0<{\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}$ for $\mathbf{M}$ positive definite. Positive definiteness gives strict positivity of the quadratic form on any nonzero vector, so the whole task is to show $\hat{\mathbf{k}}\ne 0$. That follows from the first result: if $\hat{\mathbf{k}}$ were zero, then ${\mathbf{\Gamma }}_a\hat{\mathbf{k}}$ would be zero — but it equals ${\mathbf{e}}_n$, which is not.

Proof

We first show $\hat{\mathbf{k}}\ne 0$. Suppose, for contradiction, that $\hat{\mathbf{k}}=0$. By gamma_a_khat_eq, $\mathbf{G}\hat{\mathbf{k}}={\mathbf{e}}_n$; but the left side is $\mathbf{G}0=0$, so ${\mathbf{e}}_n=0$. Reading slot $j$, this forces $1=0$, which is absurd. Hence $\hat{\mathbf{k}}\ne 0$.

Since $\mathbf{M}$ is positive definite (M.PosDef), its quadratic form is strictly positive on every nonzero vector. Applying this to $\hat{\mathbf{k}}\ne 0$,

$$0<{\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}={\hat{m}}_n$$

the equality being selfmotion_inertia_eq_denom. The Lean proof extracts the nonvanishing of $\hat{\mathbf{k}}$ exactly as above, then applies Mathlib’s PosDef.dotProduct_mulVec_pos. $■$

What this shows

The scalar self-motion inertia ${\hat{m}}_n>0$ is well posed at every configuration, so the appended covector ${\mathbf{z}}_a={\hat{\mathbf{k}}}^{\top }\mathbf{M}/{\hat{m}}_n$ never divides by zero, and the self-motion block of $\hat{\mathbf{M}}$ is nondegenerate. This is the last piece the companion damping argument needs: it scales the self-motion’s second-order law ${\hat{m}}_n{\dot{v}}_n=u_n+(\text{drive})$, and its strict positivity is what makes the closed-loop oscillator well defined. Notably, this positivity holds on all of the singularity-free region: it is the inertia weighting, and not an extended-Jacobian gradient, that avoids the algorithmic singularity where a ${\mathbf{z}}_a=\nabla g(\mathbf{q})$ would degenerate. The numeric pin test_za_denominator_positive_numeric confirms ${\hat{m}}_n>0$ across nine random configurations.

Assumptions taken as given

None — in the sense that matters. Every one of the seven results is interface-free: its hypotheses are the definitional givens of a congruence transform together with the construction of the appended covector, not un-formalized analysis facts carried on trust. Concretely, the hypotheses are the right-inverse relation $\mathbf{G}\mathbf{P}=1$ (which is what invertibility of ${\mathbf{\Gamma }}_a$ on the singularity-free region means, taken at the ring level exactly as the companion passivity theorems take their inverse), symmetry ${\mathbf{M}}^{\top }=\mathbf{M}$, the definition $\hat{\mathbf{k}}=\mathbf{P}{\mathbf{e}}_n$, positive definiteness of $\mathbf{M}$ for the single real result, and the construction bridge hrow that encodes ${\mathbf{z}}_a^{\top }={\hat{\mathbf{k}}}^{\top }\mathbf{M}/{\hat{m}}_n$. There are no named hypotheses of the kind the assumptions ledger tracks, so this module neither assumes nor discharges any: it adds no row to that ledger and introduces no new assumption.

Scope and limitations

• What is proved. The block-diagonal structure of the transformed inertia: the self-motion column and row decouple (mhat_selfmotion_column, mhat_selfmotion_row), every task velocity is $\mathbf{M}$-orthogonal to the self-motion (task_M_orthogonal), and the scalar self-motion inertia is well posed and strictly positive (selfmotion_inertia_eq_denom, selfmotion_inertia_pos). This is the hard half of proof obligation P1, the half the derivation marks “Proved above.”
• What is not formalized — the §4c bookkeeping. The derivation’s own P1 row (§6) reads: “Remaining: relate the task block to the old $\breve{\mathbf{M}}$.” That residual step — identifying the $12\times 12$ task block ${\hat{\mathbf{M}}}_{\text{task}}$ with the nonredundant reduced inertia $\breve{\mathbf{M}}$ of the six-joint theory — is not proved here. It is bookkeeping, not a new idea, and the derivation lists it as remaining; this module makes no claim about it. What is certified is the decoupling structure, which is the load-bearing content.
• The inertia, not the Coriolis, is block-diagonal. Decoupling holds for the transformed inertia $\hat{\mathbf{M}}$ alone. The transformed Coriolis matrix $\hat{\mathbf{C}}$ is not block-diagonal — its off-diagonal blocks are populated by the configuration-rate $\dot{\hat{\mathbf{M}}}$ — and any claim otherwise would be false. Those workless-but-present cross-terms, and why they drive rather than corrupt the self-motion, are treated in the companion module; this page never asserts $\hat{\mathbf{C}}$ decouples.
• Abstract over a commutative ring. The results hold for the abstract congruence data $(\mathbf{G},\mathbf{P},\mathbf{M})$ over any commutative ring (the one real result additionally needs positive definiteness). No matrix-inverse machinery is used; the concrete $13\times 13$ structure of ${\mathbf{\Gamma }}_a$ enters only through the symbolic and numerical cross-checks below.

Provenance

• giordano2019coordinated (RA-L 2019) — the coordinated-control framing, which assumes a nonredundant manipulator (“Let us assume a nonredundant manipulator”); the redundant self-motion coordinate this decoupling supports is the new content. → giordano2019coordinated.
• khatib1987unified — the dynamically consistent, inertia-weighted generalized inverse; the sense in which ${\mathbf{z}}_a^{\top }={\hat{\mathbf{k}}}^{\top }\mathbf{M}/({\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}})$ is the canonical squaring-up row, and the source of the resulting inertial decoupling. → khatib1987unified.
• ott2008cartesian — the monograph treatment of redundant-arm dynamics from which the inertially decoupled self-motion is standard; the reused fact that the dynamically consistent inverse yields a block-diagonal transformed inertia. → ott2008cartesian.
• nakamura1991advanced (Nakamura, Advanced Robotics: Redundancy and Optimization, 1991) — the classical null-space reconstruction reference for redundant manipulators, the setting in which the one-dimensional self-motion of the seven-joint arm is characterized. → nakamura1991advanced.
• The derivation transcribed here is the project’s ratified [(~/Code/generated_reports/math/derivation_7dof.md)], sections 3–5, with §4b–c the load-bearing algebra.

Symbolic and numerical cross-checks (test_seven_dof_p1_decoupling.py)

Every identity was pinned in SymPy or NumPy before it was formalized; the pin test_seven_dof_p1_decoupling.py (in Inspection/validation/tests/, run under new-pin-env) passes ten of ten, each test citing the derivation section it checks. The load-bearing cases:

• The self-motion is the kernel — test_gamma_kernel_symbolic verifies $\mathbf{\Gamma }\hat{\mathbf{k}}=0$ by block algebra (§3.2), and test_kernel_dimension_numeric confirms $\ker \mathbf{\Gamma }$ is one-dimensional, spanned by $\hat{\mathbf{k}}$, across nine configurations.
• The appended covector — test_za_normalization_symbolic checks the normalization ${\mathbf{z}}_a^{\top }\hat{\mathbf{k}}=1$ (§4), and test_za_denominator_positive_numeric checks ${\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}>0$ (§4a), pinning selfmotion_inertia_pos.
• The §4b bridge — test_M_maps_khat_to_za_symbolic certifies the construction fact $\mathbf{M}\hat{\mathbf{k}}={\hat{m}}_n{\mathbf{z}}_a^{\top }$ symbolically, and test_M_orthogonality_numeric confirms every task column is $\mathbf{M}$-orthogonal to the self-motion at $10^{-14}$ — pinning task_M_orthogonal.
• The last inverse column — test_gamma_a_khat_is_last_basis_symbolic and test_gamma_a_invertible_and_c13_numeric verify ${\mathbf{\Gamma }}_a\hat{\mathbf{k}}={\mathbf{e}}_n$ and ${\mathbf{c}}_{13}=\hat{\mathbf{k}}$ — pinning gamma_a_khat_eq.
• The block-diagonal inertia — test_p1_block_diagonal_symbolic certifies $\hat{\mathbf{M}}{\mathbf{e}}_n={\hat{m}}_n{\mathbf{e}}_n$ for generic $\mathbf{M}$ and generic kernel, and test_block_diagonal_inertia_numeric confirms both coupling blocks vanish at $10^{-14}$, the diagonal equals ${\hat{m}}_n$, and the task block is symmetric — pinning mhat_selfmotion_column, mhat_selfmotion_row, and mhat_symm.

Machine verification (#print axioms)

Lean’s kernel reports the axiom dependency of each of the seven results. Nothing beyond [propext, Classical.choice, Quot.sound] appears on any of them; there is no sorryAx, and the module contains no sorry.

info: 'Ctrllib.gamma_a_khat_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.mhat_symm' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.mhat_selfmotion_column' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.mhat_selfmotion_row' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.task_M_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.selfmotion_inertia_eq_denom' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.selfmotion_inertia_pos' depends on axioms: [propext, Classical.choice, Quot.sound]

The machine-checked source is [(~/Code/vault/lean/SevenDofDecoupling.lean)] (build copy ~/lean/ctrllib/Ctrllib/SevenDofDecoupling.lean, registered in Ctrllib.lean; this directory’s copy is the tracked source of truth).