passivity_identity

The passivity identity of the coordinated dynamics — L3 sub-phase (iii)

Why this identity matters

Every Lyapunov argument in the framing paper’s control section leans, at its central step, on one algebraic fact. Differentiating the energy-shaped Lyapunov function along the coupled attitude-and-end-effector dynamics produces the term $\frac{1}{2}{\breve{\mathbf{v}}}^{\top }(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}$, and the entire proof of Proposition IV.1 survives because that term is identically zero — the paper’s eq 38 kills it in one stroke and leaves $\dot{V}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}\le 0$. The vanishing is the passivity property, eq 23, transcribed in the house equation sheet as eq 3.5 of (~/Code/Inspection/GNC/equations/current_sota.md).

Here is the curious thing, and the reason this sub-phase exists. The framing paper states eq 23 — verbatim: “remark that (22b) enjoys the fruitful property … This property is an advantage of the machinery (19), (20), (21) used to obtain (22). Indeed, while (22a) is a common result, the advantage lies instead in (22b), for which (23) automatically holds.” — but exhibits no construction making it true. There is no Appendix B in the paper; the only deferred fact (the vanishing centroid Coriolis) points to a different paper, its reference [4]. So what, exactly, makes eq 23 hold “automatically”?

Sources and provenance

• giordano2019coordinated, eq 23 (verbatim quadratic-form statement) and eq 38 (the use site inside the proof of Prop IV.1); prose quoted above. Extraction from the rendered corpus page 2026-07-05.
• ott2008cartesian, Lemma 3.2 — the construction anchor in our corpus: “The matrix $\dot{\mathbf{\Lambda }}(x)-2\mathbf{\mu }(x,\dot{x})$ … is skew symmetric”, proved via the equality $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$ (its Property 2.6 with Lemma A.22), which in turn holds because $\mathbf{\mu }$ is chosen through the Christoffel symbols (its eq 3.11 and the remark following the proof: a different valid choice of $\mathbf{\mu }$ would not enjoy the lemma).
• House transcription: (~/Code/Inspection/GNC/equations/current_sota.md) §3 eq 3.5, with the note at its eq 3.2 that the $-\mathbf{M}{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}$ correction inside $\breve{\mathbf{C}}$ “is what makes $\breve{\mathbf{C}}$ more than a naive congruence and lets the passivity property (3.5) hold”.

The precise statements

Three lemmas, in the order the logic flows. Let $n$ index a finite dimension and write $\dot{\mathbf{M}}$ for the value of the inertia-rate matrix at some instant — the lemmas are pointwise matrix algebra and need no calculus.

Lemma 1 (factorization gives skew-symmetry — ott2008 Lemma 3.2 shape). Let $\dot{\mathbf{M}},\mathbf{C}$ be $n\times n$ matrices over a commutative ring with $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$. Then $(\dot{\mathbf{M}}-2\mathbf{C}{)}^{\top }=-(\dot{\mathbf{M}}-2\mathbf{C})$.

Notice what is not assumed: no symmetry of $\dot{\mathbf{M}}$ (it follows from the hypothesis, since $(\mathbf{C}+{\mathbf{C}}^{\top }{)}^{\top }={\mathbf{C}}^{\top }+\mathbf{C}$), and nothing about positive definiteness.

Lemma 2 (the quadratic form of a skew-symmetric matrix vanishes). If ${\mathbf{A}}^{\top }=-\mathbf{A}$ over $\mathbb{R}$, then ${\mathbf{x}}^{\top }\mathbf{Ax}=0$ for every vector $\mathbf{x}$.

Theorem (eq 23). If $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$, then ${\mathbf{v}}^{\top }(\dot{\mathbf{M}}-2\mathbf{C})\mathbf{v}=0$ for every $\mathbf{v}$ — the framing paper’s eq 23, with the $9\times 9$ circumcentroidal blocks $\dot{\breve{\mathbf{M}}},\breve{\mathbf{C}}$ and $\mathbf{v}=[{\mathbf{\omega }}_b;{\mathbf{\nu }}_e^{\oplus }]$ as the thesis instance.

Scratch work — why it is true

Substitute the factorization into the matrix of interest: $\dot{\mathbf{M}}-2\mathbf{C}=\mathbf{C}+{\mathbf{C}}^{\top }-2\mathbf{C}={\mathbf{C}}^{\top }-\mathbf{C}$, and a difference of a matrix and its transpose is the canonical skew-symmetric object. For Lemma 2, the trick every textbook uses: a $1\times 1$ matrix equals its own transpose, so the scalar ${\mathbf{x}}^{\top }\mathbf{Ax}$ satisfies ${\mathbf{x}}^{\top }\mathbf{Ax}=({\mathbf{x}}^{\top }\mathbf{Ax}{)}^{\top }={\mathbf{x}}^{\top }{\mathbf{A}}^{\top }\mathbf{x}=-{\mathbf{x}}^{\top }\mathbf{Ax}$, and a real number equal to its own negative is zero.

Proof

Lemma 1. Substituting the hypothesis, the matrix in question is ${\mathbf{C}}^{\top }-\mathbf{C}$. Taking entries, $({\mathbf{C}}^{\top }-\mathbf{C}{)}_{ij}^{\top }=({\mathbf{C}}^{\top }-\mathbf{C}{)}_{ji}=C_{ij}-C_{ji}$, while $-({\mathbf{C}}^{\top }-\mathbf{C}{)}_{ij}=-(C_{ji}-C_{ij})=C_{ij}-C_{ji}$. The two agree entrywise, which proves the lemma over any commutative ring — indeed any ring, since only additive structure was used. $\square$

Lemma 2. Since the transpose of the scalar ${\mathbf{x}}^{\top }\mathbf{Ax}$ is itself, and transposition reverses products, we have ${\mathbf{x}}^{\top }\mathbf{Ax}={\mathbf{x}}^{\top }{\mathbf{A}}^{\top }\mathbf{x}$. By skew-symmetry the right side equals $-{\mathbf{x}}^{\top }\mathbf{Ax}$. Therefore $2{\mathbf{x}}^{\top }\mathbf{Ax}=0$, and dividing by two (we are over $\mathbb{R}$) gives the claim. $\square$

Theorem. Apply Lemma 1 to obtain skew-symmetry, then Lemma 2 to kill the quadratic form. $\square$

Post-proof analysis

The moral. Eq 23 is not a property of the dynamics; it is a property of a choice. The Coriolis matrix of a mechanical system is determined only up to terms that vanish against the velocity, and ott2008’s remark after Lemma 3.2 is explicit that a different valid $\mathbf{\mu }$ would break the lemma. The Christoffel-symbol choice is precisely the one satisfying $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$, and the house sheet’s observation that the $-\mathbf{M}{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}$ correction is “what lets the passivity property hold” is the transformed-coordinates face of the same choice. So Giordano’s “automatically holds” means: the machinery of eqs 19–21 transports the Christoffel choice through the congruence.

What this seal does and does not cover. The Lean theorem is conditional: given the factorization, eq 23 holds — that is exactly the shape of ott2008’s Lemma 3.2, and it is the reusable mathematical content. What remains outside the seal is the thesis-specific computation that Giordano’s transformed $\breve{\mathbf{C}}$ (built through $\mathbf{\Gamma }$ with the $\dot{\mathbf{\Gamma }}$ correction, current_sota eq 3.2) actually satisfies $\dot{\breve{\mathbf{M}}}=\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top }$. That is a finite symbolic computation on the house matrices — a natural SymPy pipeline check (same recipe as the L1 pre-check) before any future Lean formalization of the transported construction.

Generality. Lemma 1 holds over any ring; only Lemma 2 uses division by two. A char-$\ne 2$ generalization is a one-line change if ever needed — not done, because the thesis lives over $\mathbb{R}$.

The machine seal

Passivity.lean in this directory. Verbatim #print axioms (build 2026-07-05):

info: Leanpunov/Passivity.lean:58:0: 'Leanpunov.mdot_sub_two_coriolis_skew' depends on axioms: [propext, Quot.sound]
info: Leanpunov/Passivity.lean:59:0: 'Leanpunov.dotProduct_mulVec_self_of_skew' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/Passivity.lean:60:0: 'Leanpunov.passivity_identity' depends on axioms: [propext, Classical.choice, Quot.sound]

The skew-symmetry lemma is even choice-free. Build copy at ~/lean/leanpunov/Leanpunov/Passivity.lean; this directory’s copy is the tracked source of truth.