seven_dof_passivity_extension

7-DOF Passivity Extension: Redundant Augmentation (P3, P4)

The redundant ($n=7$) extension of the coordinated controller. The wide task map is made square by one inertia-weighted row; passivity survives the augmentation (P3) and the resulting self-motion is damped through the sealed cascade (P4). Machine-checked in Lean: SevenDof (lean module). Derivation: derivation_7dof.md.

Statement

With a 7-joint arm the coordinated task map is wide: $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 13}$ (notation.md), so on the singularity-free region $\Omega$ its kernel is one-dimensional — a single self-motion direction $\hat{\mathbf{k}}$ with $\mathbf{\Gamma }\hat{\mathbf{k}}=0$. Appending one inertia-weighted row makes the map square and invertible on $\Omega$:

$${\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}}},$$

with ${\mathbf{z}}_a$ the dynamically consistent (Khatib inertia-weighted) covector. The augmented transformed dynamics are the standard congruence with the moving-frame correction

$$\hat{\mathbf{M}}={\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1},\hat{\mathbf{C}}={\mathbf{\Gamma }}_a^{-\top }(\mathbf{C}-\mathbf{M}{\mathbf{\Gamma }}_a^{-1}{\dot{\mathbf{\Gamma }}}_a){\mathbf{\Gamma }}_a^{-1}.$$

Augmented $13\times 13$, not the $n=6$ hat — load-bearing

Here $\hat{\mathbf{M}},\hat{\mathbf{C}}\in {\mathbb{R}}^{13\times 13}$ are the augmented transformed matrices of the redundant system, a different, larger object than the $12\times 12$ $\widehat{(\cdot )}$ of the nonredundant case in notation.md. The augmentation is square; an earlier pseudo-inverse / non-square $\mathbf{\Gamma }$ framing was refuted and deleted, and nothing here uses a Moore–Penrose inverse. Keeping the augmented block distinct from the reduced $\breve{(\cdot )}$ $9\times 9$ block is the distinction a prior 7-DOF effort conflated — see Circumcentroidal Decoupling.

P3 — passivity survives the augmentation. For any smooth invertible ${\mathbf{\Gamma }}_a(t)$, if $\dot{\mathbf{M}}-2\mathbf{C}$ is skew-symmetric then so is $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}$. The paper’s §5 route is the additive decomposition

$$\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}={\mathbf{\Gamma }}_a^{-\top }(\dot{\mathbf{M}}-2\mathbf{C}){\mathbf{\Gamma }}_a^{-1}+(\mathbf{S}-{\mathbf{S}}^{\top }),\mathbf{S}={\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1}{\dot{\mathbf{\Gamma }}}_a{\mathbf{\Gamma }}_a^{-1},$$

the congruence of the original skew term plus a manifestly antisymmetric correction. Hence the energy-balance (Giordano eq 23) identity holds for the augmented dynamics:

$${\mathbf{v}}^{\top }(\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}})\mathbf{v}=0\forall \mathbf{v}\in {\mathbb{R}}^{13}.$$

P4 — the self-motion is damped through the cascade. Under the null-space control $u_n=-k_n{\tilde{x}}_n-d_n{v}_n$ (with $v_n={\mathbf{z}}_a^{\top }\mathbf{x}$ the self-motion velocity and ${\tilde{x}}_n$ its regulation error), the pair $({\tilde{x}}_n,v_n)$ is a damped oscillator driven by the task-block cross-Coriolis; with the task state sent to the origin by the sealed coordinated cascade, the joint (self-motion, task) state converges. It reuses the sealed cascade engine directly — assembly, not a new convergence proof.

Assumptions

• Free-flying regime. Fully-actuated 6-DOF base; the coordinated controller leaves base translation free (“partial base control”). See Free Flying vs Free Floating. The self-motion here is not a free-floating reaction-null-space motion from momentum conservation — the base moves, and the coordinates are chosen so the combined motion registers as zero.
• Singularity-free region $\Omega =\{{\sigma }_{\min }({\mathbf{J}}_{{\nu }_e}^{\oplus })>0\}$. $\mathbf{\Gamma }$ (hence ${\mathbf{\Gamma }}_a$) is invertible there; ${\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}>0$ since $\mathbf{M}$ is SPD and $\hat{\mathbf{k}}\ne 0$, so ${\mathbf{z}}_a$ is well defined on all of $\Omega$.
• P3 uses only: ${\mathbf{M}}^{\top }=\mathbf{M}$ and the Christoffel factorization $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$ in the original coordinates. Nothing about ${\mathbf{\Gamma }}_a$ beyond invertibility enters — so it holds for any smooth invertible augmentation.
• P4 inherits the cascade interfaces of the coordinated controller (the reshaped-Lyapunov sandwich and interconnection inequality, flow existence on $\Omega$) — see the ledger interfaces. It opens no new interface family.

Proof sketch

Machine-checked in Lean 4: SevenDof (lean module) — seven theorems, every #print axioms $\subseteq \{$propext, Classical.choice, Quot.sound$\}$, no sorryAx; SymPy/NumPy pin (kernel $\Vert \mathbf{\Gamma }\hat{\mathbf{k}}\Vert =6\times 10^{-16}$, block-diagonal $\hat{\mathbf{M}}$ to $10^{-14}$, time-varying §5 skew to $2\times 10^{-7}$, reshaped-Lyapunov $a=0.399$). Full annotated derivation: derivation_7dof.md.

P3 (additive route). Differentiate $\hat{\mathbf{M}}={\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1}$ with the inverse-derivative identity $\frac{d}{dt}({\mathbf{\Gamma }}_a^{-1})=-{\mathbf{\Gamma }}_a^{-1}{\dot{\mathbf{\Gamma }}}_a{\mathbf{\Gamma }}_a^{-1}$; subtract $2\hat{\mathbf{C}}$ and collect — two of six terms cancel — to reach the displayed decomposition. A congruence ${\mathbf{P}}^{\top }\mathbf{A}\mathbf{P}$ of a skew $\mathbf{A}$ is skew, and $\mathbf{S}-{\mathbf{S}}^{\top }$ is skew by construction; the sum is skew, and a real skew quadratic form vanishes. This is an independent confirmation of the same fact the sealed factorization route Skew-Symmetry already gives (which, being polymorphic in the index type, already covered the $13\times 13$ size).

P4 (assembly). With $\hat{\mathbf{M}}$ block-diagonal (${\hat{m}}_n={\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}>0$; the self-motion is $\mathbf{M}$-orthogonal to every task velocity) the self-motion obeys ${\hat{m}}_n{\dot{v}}_n=u_n+(\text{cross-Coriolis drive})$, ${\dot{\tilde{x}}}_n=v_n$. This is a cascade whose driving output is the task state; the sealed coordinated-control convergence sends that output to zero, and the self-motion follows. The Lyapunov function is reshaped — the raw energy $\frac{1}{2}{\hat{m}}_n{v}_n^2+\frac{1}{2}{k}_n{\tilde{x}}_n^2$ lacks the $-{\tilde{x}}_n^2$ decrease, so it does not satisfy the proportional inequality $\dot{V}\le -aV+c\Vert x_2\Vert$; the reshaped

$$V_n=\frac{1}{2}{\hat{m}}_n{v}_n^2+\frac{1}{2}{k}_n{\tilde{x}}_n^2+\epsilon {\hat{m}}_n{\tilde{x}}_n{v}_n(\text{small }\epsilon >0)$$

is coercive and does (pin: $a=0.399$, $c=6$ over $2\times 10^5$ draws). This is the same reshaping Barbalat’s Lemma and the Panteley–Loría cascade sit behind.

Source / provenance

• giordano2019coordinated — the coordinated-control framing paper; it assumes a nonredundant arm (“Let us assume a nonredundant manipulator”). The redundant extension here is the new content.
• ott2008cartesian — the Christoffel skew-symmetry stone reused for P3.
• panteley2001growth — the Panteley–Loría cascade (reshaped Lyapunov, interconnection inequality) reused for P4.
• khatib1987unified — the dynamically-consistent (inertia-weighted) generalized inverse; the sense in which ${\mathbf{z}}_a$ is canonical.
• Prior art (not yet corpus-filed — plain-text, flagged): Giordano’s thesis (whole-body coordinated control) §5.2 (redundant formulation) + §5.8c (finite-$d$ damping law); his remark that the internal Coriolis stays “fully coupled” is P3 in print. Nakamura (redundant-manipulator null-space reconstruction) for the self-motion fiber.
• Ours: the square augmentation with the inertia-weighted row, the §5 additive-route Lean proof of P3, and the cascade assembly of P4.

Caveats

• $\hat{\mathbf{C}}$ is NOT block-diagonal — the honest P3 boundary. Only the transformed inertia $\hat{\mathbf{M}}$ decouples the self-motion from the task block; the Coriolis $\hat{\mathbf{C}}$ does not — the rate $\dot{\hat{\mathbf{M}}}(q)$ populates its off-diagonal blocks, so genuine cross-Coriolis terms couple $v_n$ to $({\mathbf{\omega }}_b,{\mathbf{\nu }}_e^{\oplus })$. P3 establishes these are workless (passivity is safe); it is precisely they that drive the self-motion in P4. Any claim that $\hat{\mathbf{C}}$ is block-diagonal would be false and is not made.
• P4 is interfaced, not standalone. Its convergence rests on the same named cascade interfaces as the coordinated controller (the reshaped-Lyapunov sandwich / interconnection inequality, flow existence on $\Omega$); the pin shows them realizable for the concrete damped oscillator, but they enter as hypotheses. See interfaces.
• Null-space allocation is out of scope (a design decision, not a proof target). The self-motion is one-dimensional, but three secondary objectives compete for it (singular-value maximization, envelope clearance, pan-centering). Allocating one DOF among three is a data-driven weighting/scheduling choice, made explicitly elsewhere.