coupled_dissipation

The coupled block’s Lyapunov derivative — TARGET 6 (the genuine core of Prop IV.1)

Seal

Rung rung-2 · Status interfaced — axiom-clean (#print axioms verbatim in The machine seal; build 2445 jobs), with hpass (passivity in operator form) and hreal (the moving-metric calculus) as the two new named interfaces plus the established operator set. Discharges the hdec hypothesis of reduction_cascade’s propIV1_tendsto via coupled_hdec. See interfaces. Public definition: coupledLyapRate (the moving-metric correction kept visible).
Links: module index · interface ledger · related coupled_field, passivity_transport, reduction_cascade, coupled_collapse · source giordano2019coordinated · pin pin_coupled_dissipation.py

Sealed theorems

coupled_total_dissipation

The keystone: $\text{coupledLyapRate}y=-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩$ — the Coriolis term killed by passivity, with the moving-metric correction as a visible proof step.

coupled_decrease

$\text{coupledLyapRate}y\le 0$ from $\breve{\mathbf{D}}⪰0$.

coupled_hdec

The exact hdec shape $DV(y)[f(y)]\le 0$, given hreal — the hole in propIV1_tendsto, filled by construction.

coupled_block_tendsto

The capstone: coupled_hdec fed straight into the sealed propIV1_tendsto — the coupled-block trajectory converges to ${\Gamma }_1$.

Thesis role — closing the hdec hole

Prop IV.1 (Giordano 2019 RA-L, §IV.D) proves stability of the driven coupled attitude+EE block by a Lyapunov/LaSalle argument on the mechanical energy. The sealed Reduction.propIV1_tendsto assembles that argument, but leaves its energy-decrease input as the named hypothesis

$$\text{hdec}:\forall y,DV(y)[f(y)]\le 0.$$

This lane discharges that hypothesis. It proves the physical statement Giordano writes as eqs 37-38 — that along the closed-loop field the storage function

$$V(y)=\frac{1}{2}⟨\breve{\mathbf{v}},\breve{\mathbf{M}}\breve{\mathbf{v}}⟩+\frac{1}{2}⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$$

has total time derivative $\dot{V}=-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩\le 0$ — and feeds it straight back into propIV1_tendsto. It is the genuine core of the cascade’s step 2: the Coriolis term that made the state-space partial sign-indefinite is killed here, by passivity, leaving pure damping.

The module is (/Code/vault/lean/CoupledDissipation.lean), build copy ~/lean/leanpunov/Leanpunov/CoupledDissipation.lean. SymPy pin (/Code/vault/lean/pin_coupled_dissipation.py). It consumes the two upstream lanes of this run — CoupledField (the field g₂, the energy V, and the state-space partial coupledEnergy_fderiv_field) and PassivityTransport (the transported Christoffel factorization that makes eq 23 hold).

Sources and provenance

• giordano2019coordinated eqs 37-38: the storage function (eq 37) and the dissipation $\dot{V}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}$ (eq 38).
• current_sota.md §4.6 eqs 4.15-4.16 (~/Code/Inspection/GNC/equations/current_sota.md): the house transcription, including the explicit $\frac{1}{2}{\breve{\mathbf{v}}}^{\top }\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}$ term from the configuration-dependent inertia and its cancellation against the Coriolis term via eq 23.
• Composition anchors (sealed, reused verbatim, not re-proved):
  • Leanpunov.coupledEnergy_fderiv_field (CoupledField) — the state-space partial with the stiffness cross-terms already cancelled;
  • Leanpunov.transported_passivity_identity (PassivityTransport) — the passivity property ${\breve{\mathbf{v}}}^{\top }(\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})\breve{\mathbf{v}}=0$, produced (not assumed) from the Christoffel choice;
  • Leanpunov.propIV1_tendsto (Reduction) — the assembly whose hdec this lane fills.

The two-part derivative, and why the correction term is mandatory

The subtlety this lane resolves — and the reason it is difficulty L, not a corollary of the sealed field lemma — is that there are two notions of "$\dot{V}$" and only the second is $\le 0$.

The state-space partial (constant operators) is what the sealed coupledEnergy_fderiv_field returns:

$$DV(y)[{\mathbf{g}}_2(y)]=-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩.$$

The stiffness cross-terms $-⟨\breve{\mathbf{v}},{\mathbf{J}}^{\top }\breve{\mathbf{K}}\tilde{\mathbf{x}}⟩$ and $+⟨\tilde{\mathbf{x}},\breve{\mathbf{K}}\mathbf{J}\breve{\mathbf{v}}⟩$ have already cancelled ($\breve{\mathbf{K}}$ symmetric, ${\mathbf{J}}^{\top }$ the adjoint of $\mathbf{J}$). But the Coriolis term $-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩$ survives, and it is sign-indefinite ($\breve{\mathbf{C}}$ is not symmetric). This partial alone is not $\le 0$ — it cannot discharge hdec.

The total time derivative along a real trajectory $\mathbf{y}(t)$ is larger, because the storage form $V(y)=\frac{1}{2}{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{M}}\breve{\mathbf{v}}+\dots$ carries a configuration-dependent inertia $\breve{\mathbf{M}}=\breve{\mathbf{M}}(\mathbf{q}(t))$. Differentiating $V(\mathbf{y}(t))$ by the chain rule picks up, on top of the state-space partial, the extra term from $\breve{\mathbf{M}}$ itself moving:

$$\frac{d}{dt}V(\mathbf{y}(t))=DV[{\mathbf{g}}_2]+\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩.$$

This correction term is not optional bookkeeping — it is the physical difference between differentiating a quadratic form with a frozen metric and with the true moving metric. The constant-operator CoupledField module deliberately drops it (its operators are fixed continuous linear maps); reinstating it is precisely this lane’s job.

Passivity closes the gap. The sealed transported_passivity_identity gives, for every $\breve{\mathbf{v}}$,

$$⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩=2⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩⟺\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩=⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩,$$

which is exactly what is needed to cancel the surviving Coriolis term:

$$\dot{V}=(-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩)+⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩=-⟨\breve{\mathbf{v}},\breve{\mathbf{D}}\breve{\mathbf{v}}⟩\le 0.$$

This is the whole content of Giordano’s “the Coriolis terms cancel by the skew-symmetry property” — made a theorem, with the skew-symmetry property itself already a theorem (produced by PassivityTransport), not an assertion.

The SymPy pin (frozen before the Lean)

pin_coupled_dissipation.py verifies the single new algebraic step, recomputing the state-space partial exactly as the Lean stone returns it (honest gradient of $V$, $\breve{\mathbf{M}},\breve{\mathbf{K}}$ held constant and symmetric, dotted into ${\mathbf{g}}_2$):

1. Total dissipation — $\text{partial}+\frac{1}{2}{\breve{\mathbf{v}}}^{\top }(\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top })\breve{\mathbf{v}}=-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}$, with $\dot{\breve{\mathbf{M}}}:=\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top }$ the Christoffel/passivity source. Symbolic $n=2,3$ (simplify → 0); numeric $n=3,6,9$ (max residual $3.98\times 10^{-13}$).
2. Sign — $-{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{D}}\breve{\mathbf{v}}\le 0$ for $\breve{\mathbf{D}}$ SPD (numeric, $\max \dot{V}<0$ over 400 random draws at each $n$).
3. Passivity operator form — ${\breve{\mathbf{v}}}^{\top }(\breve{\mathbf{C}}+{\breve{\mathbf{C}}}^{\top })\breve{\mathbf{v}}=2{\breve{\mathbf{v}}}^{\top }\breve{\mathbf{C}}\breve{\mathbf{v}}$, symbolic $n=2,3,4$. This certifies that the operator-form hypothesis hpass ($⟨v,\dot{\breve{\mathbf{M}}}v⟩=2⟨v,\breve{\mathbf{C}}v⟩$) is the faithful transcription of the sealed matrix identity $v\cdot (\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})v=0$.

All pins pass; the Lean statement was frozen only afterward.

The Lean, theorem by theorem

The module works on the same abstract real inner-product space $H$ as CoupledField (so coupledEnergy_fderiv_field applies with zero coercion friction), with the seven CoupledField operators plus $\dot{\breve{\mathbf{M}}}$ (Mdot) as continuous linear maps.

coupledLyapRate (definition). The assembled total rate

$$\text{coupledLyapRate}y:=DV(y)[{\mathbf{g}}_2(y)]+\frac{1}{2}⟨y_2,\dot{\breve{\mathbf{M}}}{y}_2⟩,$$

state-space partial (the sealed fderiv) plus the time-varying-inertia correction. Naming the correction explicitly, rather than pre-substituting $⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩$, keeps the mechanism visible: the passivity collapse is a proof step, not baked into the definition.

coupled_total_dissipation (the genuine core). $\text{coupledLyapRate}y=-⟨y_2,\breve{\mathbf{D}}{y}_2⟩$. Three-line proof: unfold the rate; rewrite the partial with the sealed coupledEnergy_fderiv_field hMsa hKsa hMinv hJadj y; rewrite the correction with hpass y.2; ring closes the cancellation $-⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩+\frac{1}{2}\cdot 2⟨\breve{\mathbf{v}},\breve{\mathbf{C}}\breve{\mathbf{v}}⟩=0$. The entire mathematical weight sits in the two sealed lemmas it composes.

coupled_decrease. $\text{coupledLyapRate}y\le 0$: rewrite by the identity, then $-⟨v,\breve{\mathbf{D}}v⟩\le 0$ from hDnn ($\breve{\mathbf{D}}⪰0$) via neg_nonpos.mpr. This is verbatim the com_decrease shape.

coupled_hdec. For any field $f$ and Lyapunov $V$ whose Fréchet-derivative along $f$ realizes the assembled rate (hreal: $\forall y,DV(y)[f(y)]=\text{coupledLyapRate}y$), the exact hdec shape $\forall y,DV(y)[f(y)]\le 0$ holds — rw [hreal y] then coupled_decrease.

coupled_block_tendsto (capstone). Feeds coupled_hdec straight into the sealed propIV1_tendsto. The coupled-block trajectory converges to ${\Gamma }_1$. The remaining inputs are Prop IV.1’s established named interfaces — hϕ (IsSolutionTo), hreal, hzero (the $\breve{\mathbf{v}}\equiv 0\Rightarrow \tilde{\mathbf{x}}=0$ containment, StiffnessResidual-sealed algebra), hcpt (precompactness). The hdec hole is now filled by construction.

Interfaces left named (honest boundary)

The algebra is proved outright: the cross-term cancellation, the Coriolis kill, the sign. Three interfaces are named — none a silent sorry, each the established campaign precedent:

1. hpass — passivity in operator form. $⟨v,\dot{\breve{\mathbf{M}}}v⟩=2⟨v,\breve{\mathbf{C}}v⟩$ on abstract $H$. It is the abstract transcription of the sealed matrix theorem transported_passivity_identity ($v\cdot (\dot{\breve{\mathbf{M}}}-2\breve{\mathbf{C}})v=0$). For a concrete EuclideanSpace block the two are identical via Matrix.toEuclideanCLM; bridging matrix↔operator is the same toEuclideanCLM/WithLp plumbing CoupledField already defers for its own hMinv/hJadj/hMsa/hKsa. This lane inherits CoupledField’s abstract-$H$ formulation (so the sealed field lemma applies with no coercion) and defers the bridge identically. This is the one place the brief’s “consume transported_passivity_identity” is met at the level of mathematical content (the passivity property, pinned identical in pin (3)) rather than a literal import — because the sealed theorem is matrix-shaped and the field is abstract, exactly the hMinv precedent. No weaker math is substituted.
2. hMsa/hKsa/hMinv/hJadj/hDnn — symmetry of $\breve{\mathbf{M}},\breve{\mathbf{K}}$; $\breve{\mathbf{M}}$ invertible; ${\mathbf{J}}^{\top }$ the adjoint; $\breve{\mathbf{D}}⪰0$. The CoupledField/ComLaSalle operator hypotheses, theorems for concrete SPD blocks (Matrix.PosDef.isHermitian, nonsingularInverse, le_dotProduct_mulVec).
3. hreal — the state-dependent-operator calculus. The TRUE closed-loop field carries $\breve{\mathbf{M}}(\mathbf{q}),\breve{\mathbf{C}}(\mathbf{q}),\dots$; its Lyapunov Fréchet-derivative equals the assembled rate $DV[{\mathbf{g}}_2]+\frac{1}{2}⟨\breve{\mathbf{v}},\dot{\breve{\mathbf{M}}}\breve{\mathbf{v}}⟩$. The constant-operator ${\mathbf{g}}_2$ linearises those operators pointwise; identifying the moving-metric chain rule with the assembled rate is the deferred analytic step — the IsSolutionTo / product-rule precedent used across L3/L4 and in PassivityTransport (which likewise names the product rule for $\dot{\hat{\mathbf{M}}}$). It brackets exactly the analytic plumbing, never the algebra: the algebra it brackets is coupled_total_dissipation, proved.

Nothing here needed BlockLyapunov (V’s coercivity/positivity) or Rayleigh (eigenvalue bounds): the $\dot{V}\le 0$ argument uses only the dissipation identity and $\breve{\mathbf{D}}⪰0$ (hDnn, a named PSD hypothesis, not an eigenvalue bound). Those two sealed modules feed the stability/precompactness side (hcpt), which enters coupled_block_tendsto as the established hcpt interface — not the derivative computation.

Mathlib stones used

fderiv (via the sealed coupledEnergy_fderiv_field), neg_nonpos, ring. Plus, in the capstone, the sealed propIV1_tendsto and the Flow/IsSolutionTo interface from LaSalle. Deliberately thin: the heavy fderiv_inner_apply calculus was spent in CoupledField; this lane is the composition that turns its sign-indefinite partial into the sign-definite total rate.

The machine seal

#print axioms on the four theorems, verbatim from the full-integration lake build (2445 jobs, 2026-07-06):

info: Leanpunov/CoupledDissipation.lean:163:0: 'Leanpunov.coupled_total_dissipation' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledDissipation.lean:164:0: 'Leanpunov.coupled_decrease' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledDissipation.lean:165:0: 'Leanpunov.coupled_hdec' depends on axioms: [propext, Classical.choice, Quot.sound]
info: Leanpunov/CoupledDissipation.lean:166:0: 'Leanpunov.coupled_block_tendsto' depends on axioms: [propext, Classical.choice, Quot.sound]

Nothing beyond {propext, Classical.choice, Quot.sound}; no sorryAx. First-attempt compile (11 s for the module). The whole L1-L4a + rung-1 + G2 + this lane project builds clean.

Cost feel

Well below an L2-scale push, despite the L difficulty label. The difficulty was conceptual, not tactical: understanding why the state-space partial is not $\le 0$ and what the total derivative adds (the moving-metric correction), then routing the passivity cancellation through it. Once the two-part structure is seen and pinned, the Lean is a three-line rw/ring composition of two sealed lemmas plus a neg_nonpos. The upstream lanes (CoupledField, PassivityTransport) did the heavy calculus and algebra respectively; this lane is the keystone that joins them, and keystones are short. No fix cycles: the SymPy pin fixed the mental model first, and the Lean compiled on the first attempt.