passivity_transport

The Christoffel choice transports through the congruence — TARGET 7

Seal

Rung rung-2 · Status sealed · #print axioms verbatim in The machine seal. Discharges the Christoffel-factorization hypothesis hM that passivity_identity consumed — “automatically holds” is now machine-checked. Two statement-level boundaries stay applier-side (the product-rule identification of $\dot{\hat{\mathbf{M}}}$ and the $9\times 9$ block extraction) — see interfaces.
Links: module index · interface ledger · related passivity_identity, coupled_dissipation · sources giordano2019coordinated, ott2008cartesian · pin pin_passivity_transport.py

Sealed theorems

congruence_transport

Over any commutative ring: $\mathbf{M}$ symmetric and $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$ give the transported factorization $\dot{\hat{\mathbf{M}}}=\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }$.

transported_skew

Consequently $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}$ is skew-symmetric.

transported_passivity_identity

Over $\mathbb{R}$: ${\hat{\mathbf{v}}}^{\top }(\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}})\hat{\mathbf{v}}=0$ — Giordano eq 23 for the transformed dynamics, produced rather than assumed.

Thesis role — closing the passivity interface

The sealed Passivity.lean proved Giordano’s eq 23 (the house sheet’s eq 3.5) conditionally: given the factorization $\dot{\breve{\mathbf{M}}}=\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top }$, the velocity quadratic form ${\breve{\mathbf{v}}}^{\top }(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}$ vanishes. That factorization was a consumed hypothesis — the reusable ott2008 Lemma 3.2 shape. What the framing paper never exhibits, and what the post-proof note of (~/Code/vault/lean/passivity_identity.md) flagged as the open pipeline check, is why the transformed dynamics actually satisfy that factorization. Giordano only says eq 23 “automatically holds … an advantage of the machinery (19), (20), (21)”. This module supplies the missing construction: it is a theorem that the congruence machinery transports the Christoffel factorization from the original coordinates to the transformed ones. “Automatically holds” is now machine-checked, and the hdec target after this lane inherits a discharged, not assumed, passivity property.

Sources and provenance

• current_sota §3 (~/Code/Inspection/GNC/equations/current_sota.md), eqs 3.1–3.2: 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.
• ott2008cartesian Lemma 3.2: skew-symmetry of $\dot{\mathbf{\Lambda }}-2\mathbf{\mu }$ via the Christoffel choice $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$ (its eq 3.11). ott2008’s operational-space map $\mathbf{\Lambda }={\mathbf{J}}^{-\top }\mathbf{M}{\mathbf{J}}^{-1}$ is the same congruence shape with $\mathbf{P}={\mathbf{J}}^{-1}$; the circumcentroidal $\mathbf{\Gamma }$ generalizes $\mathbf{J}$.
• Composition anchor: the sealed Leanpunov.mdot_sub_two_coriolis_skew and Leanpunov.passivity_identity (Passivity.lean), reused verbatim.

The precise statement

Let $\mathbf{P}={\mathbf{\Gamma }}^{-1}$ be the (time-varying, invertible) transform. Write $\dot{\mathbf{P}}$ for its rate. The transformed matrices, current_sota eqs 3.1–3.2 rewritten in $\mathbf{P}$ (SymPy pin (C) certifies the rewrite):

$$\hat{\mathbf{M}}={\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}\hat{\mathbf{C}}={\mathbf{P}}^{\top }(\mathbf{C}\mathbf{P}+\mathbf{M}\dot{\mathbf{P}})$$

The product rule gives the transported inertia rate

$$\dot{\hat{\mathbf{M}}}={\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}+{\mathbf{P}}^{\top }\dot{\mathbf{M}}\mathbf{P}+{\mathbf{P}}^{\top }\mathbf{M}\dot{\mathbf{P}}$$

Theorem (congruence transport). Let $\mathbf{M}$ be symmetric (${\mathbf{M}}^{\top }=\mathbf{M}$) and let the original system obey the Christoffel choice $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$. Then $\dot{\hat{\mathbf{M}}}=\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }$ — the transported factorization. Consequently $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}$ is skew-symmetric and ${\hat{\mathbf{v}}}^{\top }(\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}})\hat{\mathbf{v}}=0$ for every $\hat{\mathbf{v}}$ (Giordano eq 23 for the transformed dynamics).

Two hypotheses, and only two: symmetry of the inertia, and the Christoffel factorization in the original coordinates. Neither positive-definiteness nor any property of $\mathbf{P}$ beyond appearing in the product rule is used — the transport is purely algebraic.

Proof

Expand $\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }$. The transpose distributes and reverses products:

$${\hat{\mathbf{C}}}^{\top }=({\mathbf{P}}^{\top }(\mathbf{C}\mathbf{P}+\mathbf{M}\dot{\mathbf{P}}){)}^{\top }=(\mathbf{C}\mathbf{P}+\mathbf{M}\dot{\mathbf{P}}{)}^{\top }\mathbf{P}=({\mathbf{P}}^{\top }{\mathbf{C}}^{\top }+{\dot{\mathbf{P}}}^{\top }{\mathbf{M}}^{\top })\mathbf{P}$$

Use the symmetry ${\mathbf{M}}^{\top }=\mathbf{M}$ in the last term, then collect:

$$\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }={\mathbf{P}}^{\top }\mathbf{C}\mathbf{P}+{\mathbf{P}}^{\top }\mathbf{M}\dot{\mathbf{P}}+{\mathbf{P}}^{\top }{\mathbf{C}}^{\top }\mathbf{P}+{\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}={\mathbf{P}}^{\top }(\mathbf{C}+{\mathbf{C}}^{\top })\mathbf{P}+{\mathbf{P}}^{\top }\mathbf{M}\dot{\mathbf{P}}+{\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}$$

Now substitute the Christoffel factorization $\mathbf{C}+{\mathbf{C}}^{\top }=\dot{\mathbf{M}}$ into the middle group:

$$\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }={\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}+{\mathbf{P}}^{\top }\dot{\mathbf{M}}\mathbf{P}+{\mathbf{P}}^{\top }\mathbf{M}\dot{\mathbf{P}}=\dot{\hat{\mathbf{M}}}$$

which is exactly the product-rule expression. $\square$

The skew and eq-23 corollaries are then one application each of the sealed lemmas: $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}={\hat{\mathbf{C}}}^{\top }-\hat{\mathbf{C}}$ is a matrix-minus-its-transpose (skew), and a real skew quadratic form vanishes.

Why the symmetry hypothesis is load-bearing

Drop ${\mathbf{M}}^{\top }=\mathbf{M}$ and repeat the collection: the term ${\dot{\mathbf{P}}}^{\top }{\mathbf{M}}^{\top }\mathbf{P}$ no longer merges with ${\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}$, and the residual $\dot{\hat{\mathbf{M}}}-(\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top })={\dot{\mathbf{P}}}^{\top }(\mathbf{M}-{\mathbf{M}}^{\top })\mathbf{P}$ survives. SymPy pin (B) exhibits exactly this residual. So the transport is a joint property of the Christoffel choice and the symmetry of the inertia matrix — both physical facts, neither decorative. This is the precise sense in which Giordano’s “advantage of the machinery” is real: the congruence preserves the factorization only because $\mathbf{M}$ is a genuine (symmetric) inertia.

SymPy pin

pin_passivity_transport.py in this directory, run under new-pin-env, all pins PASS:

• (A) identity — symbolic $n=3$ with every entry an independent symbol, $\mathbf{M}$ symmetric, $\dot{\mathbf{M}}:=\mathbf{C}+{\mathbf{C}}^{\top }$: residual matrix is exactly zero; plus a 20000-sample random $5\times 5$ hammer (max residual $5.7\times 10^{-14}$).
• (B) necessity — with generic non-symmetric $\mathbf{M}$ the residual is nonzero and equals ${\dot{\mathbf{P}}}^{\top }(\mathbf{M}-{\mathbf{M}}^{\top })\mathbf{P}$, pinning symmetry as necessary and sufficient.
• (C) house correspondence — with $\mathbf{P}={\mathbf{\Gamma }}^{-1}$ (so $\dot{\mathbf{P}}=-{\mathbf{\Gamma }}^{-1}\dot{\mathbf{\Gamma }}{\mathbf{\Gamma }}^{-1}$), our $\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.

Interfaces left named (honest boundary)

The seal is the finite-dimensional algebra of the transport. Two pieces of scaffolding are supplied at the statement level rather than proved, by the same IsSolutionTo precedent used across L3/L4:

1. The product rule. The lemma’s left-hand side is the expression ${\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}+{\mathbf{P}}^{\top }\dot{\mathbf{M}}\mathbf{P}+{\mathbf{P}}^{\top }\mathbf{M}\dot{\mathbf{P}}$; it is named as $\dot{\hat{\mathbf{M}}}$ and its identification with $\frac{d}{dt}({\mathbf{P}}^{\top }\mathbf{M}\mathbf{P})$ along a trajectory is standard calculus, deliberately not re-derived from Mathlib’s HasDerivAt. The theorem’s content is the algebraic cancellation, which is what makes the Christoffel choice transport — not the product rule, which holds for any smooth matrix product.
2. The $\mathbf{P}={\mathbf{\Gamma }}^{-1}$ identification and the 9×9 block extraction. The abstract lemma holds for any $\mathbf{P}$; pin (C) certifies $\mathbf{P}={\mathbf{\Gamma }}^{-1}$ gives the house $\hat{\mathbf{C}}$. 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}}$; 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 here.

Neither interface substitutes weaker math for the theorem’s content — they are the same boundary the campaign draws everywhere between algebra (sealed) and coordinate/analytic plumbing (named).

The machine seal

PassivityTransport.lean in this directory. Public theorems: congruence_transport (CommRing), transported_skew (CommRing), transported_passivity_identity (ℝ). Verbatim #print axioms (build 2026-07-06):

info: 'Leanpunov.congruence_transport' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Leanpunov.transported_skew' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Leanpunov.transported_passivity_identity' depends on axioms: [propext, Classical.choice, Quot.sound]

Build copy at ~/lean/leanpunov/Leanpunov/PassivityTransport.lean; this directory’s copy is the tracked source of truth.

Cost feel

Below an L2-scale push. One SymPy pin (one correction to a residual-formula typo, math itself never in doubt), one Lean file compiling on the first attempt, one linter-silence follow-up matching existing precedent. The algebra is short; the leverage is that it discharges the single hypothesis the whole L3 passivity chain rested on.