Long-form companion to generated_reports/math/dynamics_modifications_7dof.md, §7.2 (the lemma the source file numbers “Lemma 1”; we keep that name). This file unpacks the two steps flagged as sticking points: the expansion of \(\dot{\hat{\boldsymbol M}}\) and the simplification of \(\dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C}\). Every transpose is written out; no step is “left to the reader.” The algebra here is machine-checked end to end in validation/test_passivity_lemma_skew.py (PASS at \(n=2\) and \(n=3\)).
If you remember nothing else, remember this. The whole proof is one product rule and one cancellation. We differentiate a triple product, three terms fall out, and when we subtract \(2\hat{\boldsymbol C}\) the messy terms collect into a single clean congruence plus an “obviously skew” leftover. That is the entire idea. There is no cleverness hiding in the multi-term products — only careful bookkeeping, which we will now do together, slowly.
You are not missing some deep trick. You are missing a place to put the terms while you work. This document is that place.
Before the algebra, the stakes. The stability argument of the coordinated-control paper (equations 37–38 there) leans on one structural fact about the equations of motion: the matrix \(\dot{\boldsymbol M} - 2\boldsymbol C\) is skew-symmetric, meaning \((\dot{\boldsymbol M} - 2\boldsymbol C)^T = -(\dot{\boldsymbol M} - 2\boldsymbol C)\).
Why does anyone care about a matrix being skew? Because a skew matrix \(\boldsymbol A\) satisfies \(\boldsymbol w^T\boldsymbol A\boldsymbol w = 0\) for every vector \(\boldsymbol w\) — it does no work along any velocity. Physically, “\(\dot{\boldsymbol M} - 2\boldsymbol C\) is skew” is exactly the statement that the Coriolis and centrifugal forces never add or remove energy; they only shuffle it around. That is what lets the energy ledger in the Lyapunov proof close, and it is the reason the closed loop is provably stable. It is the hinge the whole stability story hangs on.
Now the worry that creates this lemma. For the 7-DOF extension we changed coordinates by an augmented map \(\boldsymbol\Gamma_a\) — a \(13\times 13\) matrix whose thirteenth row is the inertia-weighted covector \(\hat{\boldsymbol z}_a^T\), an object with, as the source file admits, “no clean geometric pedigree.” The natural fear: when we transport the inertia and Coriolis matrices through this strange new transformation, does the precious skew-symmetry survive, or did we just quietly break the stability proof?
The lemma’s answer is reassuring and almost insolent in its generality: it survives for any invertible, smooth \(\boldsymbol\Gamma_a\) whatsoever. The thirteenth row could be anything. The energy bookkeeping does not care what coordinates we choose, only that the choice is invertible and differentiable. Let us see precisely why.
The “multi-term products” feel hard only because several small rules are firing at once. Here they are, separated, each with its short reason. Everything in §6–§8 is just these five facts applied in sequence.
Fact 1 — Transposing a product reverses the order. For conformable matrices, \[ (\boldsymbol{A}\boldsymbol{B}\boldsymbol{C})^T = \boldsymbol C^T\boldsymbol B^T\boldsymbol A^T . \] Read it right to left. This is the rule that will turn one of our terms into the transpose of another.
Fact 2 — The product rule has one term per factor. For three matrices that each depend on time, \[ \frac{d}{dt}\big(\boldsymbol{A}\boldsymbol{B}\boldsymbol{C}\big) = \dot{\boldsymbol A}\,\boldsymbol B\boldsymbol C + \boldsymbol A\,\dot{\boldsymbol B}\,\boldsymbol C + \boldsymbol A\boldsymbol B\,\dot{\boldsymbol C}. \] You differentiate one factor at a time and leave the others alone, then add up the results. (It is just the ordinary product rule applied twice; matrices are fine as long as you never change their left-to-right order.) This is the rule you were missing for \(\dot{\hat{\boldsymbol M}}\) — \(\hat{\boldsymbol M}\) is a product of three time-varying factors, so it produces exactly three terms.
Fact 3 — The derivative of an inverse. This is the matrix version of \(\frac{d}{dt}\big(\tfrac1x\big) = -\tfrac{\dot x}{x^2}\). Start from the definition \(\boldsymbol\Gamma_a\,\boldsymbol\Gamma_a^{-1} = \boldsymbol E\) (the identity, which is constant). Differentiate both sides with Fact 2: \[ \dot{\boldsymbol\Gamma}_a\,\boldsymbol\Gamma_a^{-1} + \boldsymbol\Gamma_a\,\frac{d}{dt}\big(\boldsymbol\Gamma_a^{-1}\big) = \boldsymbol 0 . \] Now solve for the piece we want. Move the first term across and left-multiply by \(\boldsymbol\Gamma_a^{-1}\): \[ \boxed{\;\frac{d}{dt}\big(\boldsymbol\Gamma_a^{-1}\big) = -\,\boldsymbol\Gamma_a^{-1}\,\dot{\boldsymbol\Gamma}_a\,\boldsymbol\Gamma_a^{-1}\;} \] The minus sign is the whole personality of this rule; do not lose it.
Fact 3′ — The same rule, transposed. We will also need the derivative of \(\boldsymbol\Gamma_a^{-T}\) (shorthand for \((\boldsymbol\Gamma_a^{-1})^T\)). Transposing Fact 3 and using Fact 1 to reverse the order: \[ \frac{d}{dt}\big(\boldsymbol\Gamma_a^{-T}\big) = \Big(-\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\boldsymbol\Gamma_a^{-1}\Big)^T = -\,\boldsymbol\Gamma_a^{-T}\,\dot{\boldsymbol\Gamma}_a^{T}\,\boldsymbol\Gamma_a^{-T}. \] (Transposing and differentiating commute, so the dot and the \(T\) can be applied in either order.)
Fact 4 — A congruence preserves skew-symmetry. A congruence of a matrix \(\boldsymbol A\) is the sandwich \(\boldsymbol P^T\boldsymbol A\boldsymbol P\). Suppose \(\boldsymbol A\) is skew, \(\boldsymbol A^T = -\boldsymbol A\). Then, using Fact 1 twice, \[ \big(\boldsymbol P^T\boldsymbol A\boldsymbol P\big)^T = \boldsymbol P^T\boldsymbol A^T\boldsymbol P = \boldsymbol P^T(-\boldsymbol A)\boldsymbol P = -\,\boldsymbol P^T\boldsymbol A\boldsymbol P . \] So the sandwich is skew too. Squeezing a skew matrix between \(\boldsymbol P^T\) and \(\boldsymbol P\) keeps it skew. (Notice this needs nothing about \(\boldsymbol P\) — not invertibility, not anything. Pure algebra.)
Fact 5 — Anything minus its own transpose is skew. For any square matrix \(\boldsymbol S\), \[ \big(\boldsymbol S - \boldsymbol S^T\big)^T = \boldsymbol S^T - \boldsymbol S = -\big(\boldsymbol S - \boldsymbol S^T\big). \] So \(\boldsymbol S - \boldsymbol S^T\) is automatically skew, no matter what \(\boldsymbol S\) is. Keep this in your back pocket; it is the last line of the proof.
The moral of the toolbox. Four of these five facts are one line each, and the fifth (Fact 3) is three lines. Nothing here is hard. The difficulty you felt was the difficulty of doing all five at once in your head. We will do them one at a time on paper instead.
It is much easier to manipulate \(\hat{\boldsymbol M}\) and \(\hat{\boldsymbol C}\) once you know why they have the shapes they do — especially the odd-looking second term inside \(\hat{\boldsymbol C}\). They are not handed down from on high; they are what you get when you rewrite the equations of motion in the new velocity coordinates. Let us derive them, because that derivation makes the lemma feel inevitable rather than lucky.
Write the generalized-velocity dynamics in the native coordinates as \[ \boldsymbol M\,\dot{\boldsymbol x} + \boldsymbol C\,\boldsymbol x + \boldsymbol g = \boldsymbol F, \] where \(\boldsymbol x\) is the generalized velocity, \(\boldsymbol M\) the (symmetric) inertia, \(\boldsymbol C\) the Coriolis matrix, \(\boldsymbol g\) the configuration forces, and \(\boldsymbol F\) the generalized force. Now introduce the new velocity coordinate \(\boldsymbol\xi = \boldsymbol\Gamma_a\boldsymbol x\), equivalently \(\boldsymbol x = \boldsymbol\Gamma_a^{-1}\boldsymbol\xi\). We need \(\dot{\boldsymbol x}\) in the new coordinates, and here is the crucial subtlety: \(\boldsymbol\Gamma_a\) depends on the configuration, which changes in time, so \(\boldsymbol\Gamma_a^{-1}\) must itself be differentiated. By Fact 2 and Fact 3, \[ \dot{\boldsymbol x} = \frac{d}{dt}\big(\boldsymbol\Gamma_a^{-1}\big)\boldsymbol\xi + \boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\xi} = -\,\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\boldsymbol\Gamma_a^{-1}\boldsymbol\xi + \boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\xi}. \] Substitute this into the dynamics and then left-multiply the whole equation by \(\boldsymbol\Gamma_a^{-T}\). (We multiply by \(\boldsymbol\Gamma_a^{-T}\) specifically because it makes the new force read \(\boldsymbol\Gamma_a^{-T}\boldsymbol F\), which keeps power invariant: \(\boldsymbol\xi^T(\boldsymbol\Gamma_a^{-T}\boldsymbol F) = \boldsymbol x^T\boldsymbol F\). Preserving power is the physical reason the energy structure is going to survive.) Collecting the coefficient of \(\dot{\boldsymbol\xi}\) and the coefficient of \(\boldsymbol\xi\): \[ \underbrace{\boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}}_{\hat{\boldsymbol M}}\,\dot{\boldsymbol\xi} \;+\; \underbrace{\boldsymbol\Gamma_a^{-T}\big(\boldsymbol C - \boldsymbol M\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\big)\boldsymbol\Gamma_a^{-1}}_{\hat{\boldsymbol C}}\,\boldsymbol\xi \;+\; \boldsymbol\Gamma_a^{-T}\boldsymbol g \;=\; \boldsymbol\Gamma_a^{-T}\boldsymbol F . \]
There they are. \(\hat{\boldsymbol M} = \boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}\) is just the inertia seen in the new coordinates, and the strange second term inside \(\hat{\boldsymbol C}\), \(-\boldsymbol M\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\), is precisely the inertial correction born from the coordinate frame itself accelerating — the matrix analogue of a fictitious force. It is not optional decoration; it is the price of a time-varying change of coordinates, and it is exactly the term that will make the bookkeeping in §7 close.
Lemma 1 (§7.2) — passivity survives any invertible augmentation. Let \(\boldsymbol\Gamma_a(\boldsymbol q) \in \mathbb R^{13\times 13}\) be invertible and continuously differentiable along the motion, and define \[ \hat{\boldsymbol M} = \boldsymbol\Gamma_a^{-T}\boldsymbol M\,\boldsymbol\Gamma_a^{-1}, \qquad \hat{\boldsymbol C} = \boldsymbol\Gamma_a^{-T}\big(\boldsymbol C - \boldsymbol M\,\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\big)\boldsymbol\Gamma_a^{-1}. \] If \(\dot{\boldsymbol M} - 2\boldsymbol C\) is skew-symmetric, then so is \(\dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C}\).
We will assume throughout that \(\boldsymbol M\) is symmetric, \(\boldsymbol M^T = \boldsymbol M\) — this is true of every inertia matrix, and it is the one property of \(\boldsymbol M\) the proof actually uses.
Let us think backward from the goal before writing anything polished, the way you would at the whiteboard.
What do we want? To show \(\dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C}\) is skew.
What do we already know is skew? \(\dot{\boldsymbol M} - 2\boldsymbol C\), by hypothesis. And by Fact 4, its congruence \(\boldsymbol\Gamma_a^{-T}(\dot{\boldsymbol M} - 2\boldsymbol C)\boldsymbol\Gamma_a^{-1}\) is skew too. So if only we could massage \(\dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C}\) into the form \[ \dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C} \;\overset{?}{=}\; \underbrace{\boldsymbol\Gamma_a^{-T}(\dot{\boldsymbol M} - 2\boldsymbol C)\boldsymbol\Gamma_a^{-1}}_{\text{skew by Facts 4}} \;+\; \underbrace{(\text{something} - \text{its transpose})}_{\text{skew by Fact 5}}, \] we would be finished, because a sum of two skew matrices is skew. So the entire game is algebra: push \(\dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C}\) until it looks like that target. That tells us our technique — direct computation — and tells us exactly what shape to aim for. No contradiction, no cases; just differentiate and collect.
The only place a derivative even enters is \(\dot{\hat{\boldsymbol M}}\), so that is where we start.
Here is the step that was blocking you, done with nothing skipped.
The object \(\hat{\boldsymbol M} = \boldsymbol\Gamma_a^{-T}\,\boldsymbol M\,\boldsymbol\Gamma_a^{-1}\) is a product of three matrices, each depending on time: \(\boldsymbol\Gamma_a^{-T}\), then \(\boldsymbol M\), then \(\boldsymbol\Gamma_a^{-1}\). By the three-factor product rule (Fact 2), differentiating produces three terms — one for each factor, with the other two held fixed: \[ \dot{\hat{\boldsymbol M}} = \Big(\tfrac{d}{dt}\boldsymbol\Gamma_a^{-T}\Big)\,\boldsymbol M\,\boldsymbol\Gamma_a^{-1} \;+\; \boldsymbol\Gamma_a^{-T}\,\dot{\boldsymbol M}\,\boldsymbol\Gamma_a^{-1} \;+\; \boldsymbol\Gamma_a^{-T}\,\boldsymbol M\,\Big(\tfrac{d}{dt}\boldsymbol\Gamma_a^{-1}\Big). \] That is already the expansion; we have just not yet substituted what the two derivatives of inverses are. Do that now, pulling the boxed Fact 3 into the third term and Fact 3′ into the first:
Putting the three pieces in a row, and labelling them so we can refer back: \[ \dot{\hat{\boldsymbol M}} = \underbrace{-\,\boldsymbol\Gamma_a^{-T}\dot{\boldsymbol\Gamma}_a^{T}\boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}}_{\text{(I)}} \;+\; \underbrace{\boldsymbol\Gamma_a^{-T}\dot{\boldsymbol M}\boldsymbol\Gamma_a^{-1}}_{\text{(II)}} \;\underbrace{-\,\boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\boldsymbol\Gamma_a^{-1}}_{\text{(III)}} . \]
That is the complete expansion of \(\dot{\hat{\boldsymbol M}}\), and it matches the three-term line in the source proof exactly. Notice the shape of each term:
Why three and not more? Students often expect a mess here. There are exactly three terms because there are exactly three time-varying factors. The product rule cannot manufacture more terms than there are factors. That is the entire reason the expansion is finite and tidy.
Now the second blocker. We have \(\dot{\hat{\boldsymbol M}}\) in three pieces. We need to subtract \(2\hat{\boldsymbol C}\) and watch the junk collapse. The trick that makes this readable is to name the junk so we are not copying long products over and over.
Define \[ \boldsymbol S \;:=\; \boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\boldsymbol\Gamma_a^{-1}. \] Compare with term (III) above: term (III) is exactly \(-\boldsymbol S\). Good — one term is now a single letter.
This is the one genuinely clever observation in the whole proof, so let us go very slowly. Take the transpose of \(\boldsymbol S\). We use Fact 1 — transpose reverses the order and transposes each factor. Writing \(\boldsymbol S\) as the five-factor product \(\boldsymbol\Gamma_a^{-T}\cdot\boldsymbol M\cdot\boldsymbol\Gamma_a^{-1}\cdot\dot{\boldsymbol\Gamma}_a\cdot\boldsymbol\Gamma_a^{-1}\) and reversing: \[ \boldsymbol S^{T} = \big(\boldsymbol\Gamma_a^{-1}\big)^{T}\,\big(\dot{\boldsymbol\Gamma}_a\big)^{T}\,\big(\boldsymbol\Gamma_a^{-1}\big)^{T}\,\boldsymbol M^{T}\,\big(\boldsymbol\Gamma_a^{-T}\big)^{T}. \] Now simplify each transposed factor one at a time:
Substituting these back in, \[ \boldsymbol S^{T} = \boldsymbol\Gamma_a^{-T}\,\dot{\boldsymbol\Gamma}_a^{T}\,\boldsymbol\Gamma_a^{-T}\,\boldsymbol M\,\boldsymbol\Gamma_a^{-1}. \] Look back at term (I): it is \(-\boldsymbol\Gamma_a^{-T}\dot{\boldsymbol\Gamma}_a^{T}\boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}\), which is precisely \(-\boldsymbol S^{T}\). So the two scary junk terms were a matched pair all along: \[ \text{(I)} = -\boldsymbol S^{T}, \qquad \text{(III)} = -\boldsymbol S . \] With this, the expansion of \(\dot{\hat{\boldsymbol M}}\) from §6 collapses to a one-liner: \[ \dot{\hat{\boldsymbol M}} = -\,\boldsymbol S^{T} \;+\; \boldsymbol\Gamma_a^{-T}\dot{\boldsymbol M}\boldsymbol\Gamma_a^{-1} \;-\; \boldsymbol S . \]
(Sanity check you can do in the margin: \(\hat{\boldsymbol M}\) is symmetric, so \(\dot{\hat{\boldsymbol M}}\) must be symmetric too. Transpose the right-hand side: \(-\boldsymbol S - (\boldsymbol\Gamma_a^{-T}\dot{\boldsymbol M}\boldsymbol\Gamma_a^{-1})^{T} - \boldsymbol S^{T}\). Since \(\dot{\boldsymbol M}\) is symmetric, its congruence is symmetric, and we get the same three terms back. It checks out — a small reassurance that the signs are right.)
Now look at \(\hat{\boldsymbol C}\) itself. Multiply out the bracket in its definition: \[ \hat{\boldsymbol C} = \boldsymbol\Gamma_a^{-T}\big(\boldsymbol C - \boldsymbol M\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\big)\boldsymbol\Gamma_a^{-1} = \boldsymbol\Gamma_a^{-T}\boldsymbol C\boldsymbol\Gamma_a^{-1} \;-\; \boldsymbol\Gamma_a^{-T}\boldsymbol M\boldsymbol\Gamma_a^{-1}\dot{\boldsymbol\Gamma}_a\boldsymbol\Gamma_a^{-1}. \] The second piece is exactly \(\boldsymbol S\) again. So \(\hat{\boldsymbol C}\) has a remarkably simple form: \[ \hat{\boldsymbol C} = \boldsymbol\Gamma_a^{-T}\boldsymbol C\boldsymbol\Gamma_a^{-1} \;-\; \boldsymbol S, \qquad\text{hence}\qquad -2\hat{\boldsymbol C} = -2\,\boldsymbol\Gamma_a^{-T}\boldsymbol C\boldsymbol\Gamma_a^{-1} \;+\; 2\boldsymbol S . \] This is the moment the funny second term of \(\hat{\boldsymbol C}\) (the fictitious-force term from §3) earns its keep: it is the \(\boldsymbol S\) that will cancel the junk from \(\dot{\hat{\boldsymbol M}}\).
Everything is now in terms of three ingredients: clean congruences, \(\boldsymbol S\), and \(\boldsymbol S^{T}\). Let us tabulate every term and its coefficient, so nothing can hide.
| source | term | clean congruence | \(\boldsymbol S\) | \(\boldsymbol S^{T}\) |
|---|---|---|---|---|
| \(\dot{\hat{\boldsymbol M}}\), (I) | \(-\boldsymbol S^{T}\) | — | — | \(-1\) |
| \(\dot{\hat{\boldsymbol M}}\), (II) | \(+\boldsymbol\Gamma_a^{-T}\dot{\boldsymbol M}\boldsymbol\Gamma_a^{-1}\) | \(+\dot{\boldsymbol M}\) | — | — |
| \(\dot{\hat{\boldsymbol M}}\), (III) | \(-\boldsymbol S\) | — | \(-1\) | — |
| \(-2\hat{\boldsymbol C}\), part a | \(-2\,\boldsymbol\Gamma_a^{-T}\boldsymbol C\boldsymbol\Gamma_a^{-1}\) | \(-2\boldsymbol C\) | — | — |
| \(-2\hat{\boldsymbol C}\), part b | \(+2\boldsymbol S\) | — | \(+2\) | — |
Now read the columns:
The \(\boldsymbol S\) accounting in words, since this is the exact phrase the source proof compresses: the \(+2\boldsymbol S\) that came from \(-2\hat{\boldsymbol C}\) cancels the \(-\boldsymbol S\) in term (III) and leaves one more \(\boldsymbol S\) over. Put the three surviving columns together: \[ \boxed{\;\dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C} = \boldsymbol\Gamma_a^{-T}\big(\dot{\boldsymbol M} - 2\boldsymbol C\big)\boldsymbol\Gamma_a^{-1} \;+\; \big(\boldsymbol S - \boldsymbol S^{T}\big).\;} \] This is exactly the shape we wished for back in §5. The hard part is over.
We now just apply two toolbox facts to the boxed result.
The first summand, \(\boldsymbol\Gamma_a^{-T}(\dot{\boldsymbol M} - 2\boldsymbol C)\boldsymbol\Gamma_a^{-1}\), is a congruence (with \(\boldsymbol P = \boldsymbol\Gamma_a^{-1}\), so \(\boldsymbol P^T = \boldsymbol\Gamma_a^{-T}\)) of the matrix \(\dot{\boldsymbol M} - 2\boldsymbol C\). By hypothesis \(\dot{\boldsymbol M} - 2\boldsymbol C\) is skew, so by Fact 4 the congruence is skew.
The second summand, \(\boldsymbol S - \boldsymbol S^{T}\), is skew by Fact 5 — it is a matrix minus its own transpose, which is skew no matter what \(\boldsymbol S\) is. We never had to understand what \(\boldsymbol S\) “means”; its structure alone guarantees the skewness.
A sum of two skew matrices is skew (transpose the sum, each piece flips sign). Therefore \[ \dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C}\ \text{is skew-symmetric}, \] which is exactly what the lemma claimed. \(\blacksquare\)
The moral. The energy bookkeeping does not care which thirteenth row we appended to build \(\boldsymbol\Gamma_a\) — the proof never opened up \(\boldsymbol\Gamma_a\) or used a single property of \(\hat{\boldsymbol z}_a\). It used only that \(\boldsymbol\Gamma_a\) is invertible (so that \(\boldsymbol\Gamma_a^{-1}\) exists) and smooth (so that \(\dot{\boldsymbol\Gamma}_a\) exists). Every worry about the “pedigree” of the inertia-weighted row evaporates. All the genuine risk of the redundant extension therefore lives in structure — which coordinate couples to which, the open obligations P1/P3/P4 in the source file — and never in passivity. That is precisely why the team could run the mission before those structural obligations were discharged.
Where did the magic actually happen? In one place: §7.2, recognizing term (I) as \(-\boldsymbol S^{T}\). Everything else is mechanical. And even that step was not magic — it was forced. Once you decide to name the (III)-product \(\boldsymbol S\), the symmetry of \(\boldsymbol M\) makes (I) into \(-\boldsymbol S^T\) automatically. The proof essentially writes itself once you give the junk a name.
Could it be shorter? Yes — there is a slick coordinate-free argument. “\(\dot{\boldsymbol M} - 2\boldsymbol C\) skew” is equivalent to the energy balance \(\frac{d}{dt}\big(\tfrac12\boldsymbol x^T\boldsymbol M\boldsymbol x\big) = \boldsymbol x^T\boldsymbol F\), a statement about the physical system that no change of coordinates can touch. From that viewpoint the lemma is almost a tautology. But a careful committee will rightly ask, “where does the \(\dot{\boldsymbol\Gamma}_a\) correction go in that one-liner?” — and the honest answer is the explicit computation above, which exhibits it sitting inside \(\boldsymbol S - \boldsymbol S^{T}\). The long way is the one that survives cross-examination. (This is also why \(\hat{\boldsymbol C}\) had to contain its fictitious-force term: without it, the leftover would have been \(2\boldsymbol S\), which is not skew, and passivity would genuinely break. The definition of \(\hat{\boldsymbol C}\) is exactly engineered so the leftover is \(\boldsymbol S - \boldsymbol S^T\) instead.)
What this lemma does not give you. It is a statement about the open-loop coordinate change only. It does not prove the closed-loop theorem for a finite-gain null-space law — that needs the cascade argument rerun with the extended Lyapunov function \(V \mathrel{+}= \tfrac12\hat m_n v_n^2 + \tfrac12 k_n\tilde x_n^2\) (obligation P4) — and it does not bound the Coriolis cross-couplings between the ghost coordinate (a.k.a. the self-motion velocity \(v_n\) — the null-space motion of the coordinated map \(\boldsymbol\Gamma\)) and the task (obligation P3). Skew-symmetry is necessary for the stability story, not the whole of it. Keep that boundary crisp when you present this.
The central identity of §7.4, \[ \dot{\hat{\boldsymbol M}} - 2\hat{\boldsymbol C} = \boldsymbol\Gamma_a^{-T}\big(\dot{\boldsymbol M} - 2\boldsymbol C\big)\boldsymbol\Gamma_a^{-1} + \big(\boldsymbol S - \boldsymbol S^{T}\big), \] and the skew conclusion of §8 are both verified symbolically in validation/test_passivity_lemma_skew.py. The check keeps \(\boldsymbol\Gamma_a\) as the fundamental symbol and lets the computer-algebra system differentiate it, so the product rule (§6) and the inverse-derivative rule (Fact 3) are exercised by the machine rather than assumed. Result, at generic time-varying matrices of dimension \(n = 2\) and \(n = 3\):
identity (the term-collection the hand proof performs):
n=2: d/dt(Mhat) - 2 Chat == G^-T(dM-2C)G^-1 + (S - S^T) -> PASS
n=3: d/dt(Mhat) - 2 Chat == G^-T(dM-2C)G^-1 + (S - S^T) -> PASS
conclusion (skewness is preserved):
n=2: (dM - 2C) skew => d/dt(Mhat) - 2 Chat skew -> PASS
n=3: (dM - 2C) skew => d/dt(Mhat) - 2 Chat skew -> PASS
ALL PASSRegenerate with:
python validation/test_passivity_lemma_skew.py