Passivity in the Circumcentroidal Dynamics

At a glance

Two companion pages carry the reusable algebra: the passivity identity proves that the Christoffel factorization $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$ forces Giordano’s eq 23, and the congruence transport proves that a change of coordinates carries that factorization along with it. Both are stated for abstract matrices, and Lean’s kernel has checked them. This page is the bridge to the thesis’s own matrices: it says why the controller’s stability proof needs eq 23, transcribes the project’s equation sheet, identifies the abstract congruence with the circumcentroidal transform, and reduces the full $12\times 12$ operators to the $9\times 9$ attitude-and-end-effector blocks the controller runs on. Nothing here is machine-checked in Lean — it is the correspondence between the checked algebra and the concrete construction, with a SymPy pin standing in for the parts that are only symbolic.
Links: the passivity identity · the congruence transport · the assumptions ledger · sources giordano2019coordinated, ott2008cartesian

Why the controller’s stability proof needs eq 23

Giordano’s stability argument for the circumcentroidal controller — Proposition IV.1 — turns on one algebraic fact. When the energy-shaped Lyapunov function is differentiated along the coupled attitude-and-end-effector dynamics, out falls a cross term $\frac{1}{2}{\breve{\mathbf{v}}}^{\top }(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}$, and the proof survives only because that term vanishes identically — the passivity property, eq 23. In the thesis instance the abstract matrices carry the $9\times 9$ circumcentroidal blocks $\dot{\breve{\mathbf{M}}},\breve{\mathbf{C}}$, and the velocity is the stacked attitude-and-end-effector rate $\mathbf{v}=[{\mathbf{\omega }}_b;{\mathbf{\nu }}_e^{\oplus }]$.

The abstract identity — that the factorization forces the quadratic form to vanish — is proved on the passivity identity page, and the reason the transformed dynamics inherit that factorization is proved on the congruence transport page. What this page adds is the concrete link: why those particular circumcentroidal blocks are the ones the abstract theorems describe.

The house transcription: eq 3.5 and the $\dot{\mathbf{\Gamma }}$ correction

The vanishing cross term is transcribed in the project’s equation sheet (current_sota §3, at (~/Code/Inspection/GNC/equations/current_sota.md)) as eq 3.5, and the two matrices it is built from are the transformed inertia and Coriolis of eqs 3.1–3.2. Written with the circumcentroidal map $\mathbf{\Gamma }$, the sheet records the transformed inertia $\hat{\mathbf{M}}={\mathbf{\Gamma }}^{-\top }\mathbf{M}{\mathbf{\Gamma }}^{-1}$ and Coriolis $\hat{\mathbf{C}}={\mathbf{\Gamma }}^{-\top }(\mathbf{C}-\mathbf{M}{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}){\mathbf{\Gamma }}^{-1}$, with the sheet’s own note that the $-\mathbf{M}{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}$ correction “is what makes $\hat{\mathbf{C}}$ more than a naive congruence and lets the passivity property (3.5) hold.” Eq 3.5 is the target quadratic form.

Read from the reduced side, the same note says the correction $-\mathbf{M}{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}$ inside $\breve{\mathbf{C}}$ “is what makes $\breve{\mathbf{C}}$ more than a naive congruence and lets the passivity property (3.5) hold” — the transformed-coordinates face of the same Christoffel choice. The transport page proves, abstractly, that this correction is exactly the amount needed to keep the factorization intact through the change of coordinates; here we only record that the house form is that abstract object.

Identifying the abstract transform with $\mathbf{P}={\mathbf{\Gamma }}^{-1}$

The congruence transport theorem holds for any invertible time-varying transform $\mathbf{P}$; the thesis fixes $\mathbf{P}={\mathbf{\Gamma }}^{-1}$, the inverse of the circumcentroidal map. SymPy pin (C) certifies that this choice reproduces the equation sheet’s Coriolis form symbol for symbol. With $\mathbf{P}={\mathbf{\Gamma }}^{-1}$ (so that $\dot{\mathbf{P}}=-{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}{\mathbf{\Gamma }}^{-1}$), the abstract $\hat{\mathbf{C}}={\mathbf{P}}^{\top }(\mathbf{C}\mathbf{P}+\mathbf{M}\dot{\mathbf{P}})$ equals the house eq-3.2 form ${\mathbf{\Gamma }}^{-\top }(\mathbf{C}-\mathbf{M}{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}){\mathbf{\Gamma }}^{-1}$ symbolically. This certifies that the abstract $\mathbf{P}$-lemma is the circumcentroidal construction.

From the full operators to the reduced blocks

The abstract lemma is stated for the full $12\times 12$ transformed operators, whereas the controller acts on the reduced $9\times 9$ attitude-and-end-effector blocks; passing between them is a short piece of block bookkeeping. The reduced $\breve{\mathbf{M}},\breve{\mathbf{C}}$ are the lower-right $9\times 9$ block of the $12\times 12$ $\hat{\mathbf{M}},\hat{\mathbf{C}}$ (the hat-versus-breve convention); since $\hat{\mathbf{M}}=\mathrm{blkdiag}(m\mathbf{E},\breve{\mathbf{M}})$ with constant total mass, the bottom-right block of $\dot{\hat{\mathbf{M}}}=\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }$ is precisely $\dot{\breve{\mathbf{M}}}=\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top }$, and specializing eq 23 to $\hat{\mathbf{v}}=[0;\breve{\mathbf{v}}]$ recovers the reduced eq 3.5. This block bookkeeping is left applier-side; the reusable mathematical content is the full-system transport proved on the congruence transport page, and the assumptions ledger records the boundary.

The thesis-specific factorization check (SymPy)

Everything above establishes the shape of the correspondence; what remains is to verify that the project’s own transformed Coriolis block actually factors. That is the thesis-specific computation that Giordano’s transformed Coriolis block $\breve{\mathbf{C}}$ — built through the coordinate map $\mathbf{\Gamma }$ with the $\dot{\mathbf{\Gamma }}$ correction of 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, the same recipe as the earlier symbolic pre-check — that would precede any future formalization of the transported construction.

Provenance

• giordano2019coordinated, eq 23 (the passivity property as a velocity quadratic form) and eq 38 (its use site inside the proof of Proposition IV.1).
• House equation sheet, current_sota §3 (at (~/Code/Inspection/GNC/equations/current_sota.md)), eqs 3.1–3.2 and eq 3.5 — the transformed inertia and Coriolis matrices, and the target quadratic form.
• The abstract results this page instantiates are the passivity identity and the congruence transport; both cite Giordano (2019) eq 23 and Ott (2008) Lemma 3.2 for the underlying mathematics.