seven_dof

Arc 7 — the 7-DOF passivity extension (P3 + P4)

Seal

Rung rung-5 · Status interfaced · #print axioms verbatim in The machine seal (full-library build green, 2656 jobs, 2026-07-09). P3 (inv_deriv_eq, congruence_skew, augmented_passivity_decomp, augmented_passivity_skew, augmented_passivity_identity) is SEALED with no open interface — pure finite-dimensional algebra over a commutative ring. P4 (nullspace_damping_gas, nullspace_damping_driven) is interfaced, resting on the same cascade interfaces as cascade (hsand, hdi, IsSolutionTo, the SPD-operator hypotheses via propIV1_cascade_gas). See interfaces.
Links: module index · interface ledger · extends passivity_transport · reuses cascade, passivity_identity · sources giordano2019coordinated, ott2008cartesian, panteley2001growth, khatib1987unified · pin pin_seven_dof.py · derivation [(~/Code/generated_reports/math/derivation_7dof.md)]

The ratified derivation is [(~/Code/generated_reports/math/derivation_7dof.md)]; this page is its §5 and §6/P4 as machine-checked Lean. With a 7-joint arm the coordinated task map $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 13}$ is wide; the augmentation appends one inertia-weighted row to make it square and invertible on the singularity-free region $\Omega$:

$${\mathbf{\Gamma }}_a=\left[\begin{array}{c}\mathbf{\Gamma }\\ {\mathbf{z}}_a^{\top }\end{array}\right]\in {\mathbb{R}}^{13\times 13}{\mathbf{z}}_a^{\top }=\frac{{\hat{\mathbf{k}}}^{\top }\mathbf{M}}{{\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}}$$

with $\hat{\mathbf{k}}$ the one-dimensional self-motion (kernel of $\mathbf{\Gamma }$) and ${\mathbf{z}}_a$ the dynamically consistent (Khatib) covector. The transformed dynamics are the standard congruence with the moving-frame correction:

$$\hat{\mathbf{M}}={\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1}\hat{\mathbf{C}}={\mathbf{\Gamma }}_a^{-\top }(\mathbf{C}-\mathbf{M}{\mathbf{\Gamma }}_a^{-1}{\dot{\mathbf{\Gamma }}}_a){\mathbf{\Gamma }}_a^{-1}$$

The augmentation is square. An earlier pseudo-inverse / non-square $\mathbf{\Gamma }$ framing was refuted and deleted; nothing below uses a Moore–Penrose inverse.

Sealed theorems

inv_deriv_eq

The §5 “differentiate ${\mathbf{\Gamma }}_a{\mathbf{\Gamma }}_a^{-1}=\mathbf{E}$ and solve” step. If $\mathbf{P}={\mathbf{\Gamma }}_a^{-1}$ is a left inverse ($\mathbf{P}\mathbf{G}=1$) and the product rule holds for the identity ($\dot{\mathbf{G}}\mathbf{P}+\mathbf{G}\dot{\mathbf{P}}=0$), then $\dot{\mathbf{P}}=-\mathbf{P}\dot{\mathbf{G}}\mathbf{P}$. Purely algebraic — no size, symmetry, or positivity.

congruence_skew

“A change of basis of a skew matrix is skew” (§5). If ${\mathbf{A}}^{\top }=-\mathbf{A}$ then $({\mathbf{P}}^{\top }\mathbf{A}\mathbf{P}{)}^{\top }=-({\mathbf{P}}^{\top }\mathbf{A}\mathbf{P})$ for any $\mathbf{P}$.

augmented_passivity_decomp

The Arc’s new content — the §5 additive identity. With $\mathbf{M}$ symmetric and the Christoffel factorization $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }$, substituting the inverse-derivative $\dot{\mathbf{P}}=-\mathbf{P}\dot{\mathbf{G}}\mathbf{P}$,

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

the congruence of the original skew term plus a manifestly antisymmetric correction. ($\mathbf{P}={\mathbf{\Gamma }}_a^{-1}$, $\dot{\mathbf{G}}={\dot{\mathbf{\Gamma }}}_a$.)

augmented_passivity_skew

P3 headline. $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}$ is skew-symmetric — proved via the §5 additive route: congruence_skew on the sealed mdot_sub_two_coriolis_skew gives the congruence term skew, $\mathbf{S}-{\mathbf{S}}^{\top }$ is antisymmetric, and a sum of skews is skew.

augmented_passivity_identity

Giordano eq 23 for the augmented dynamics: ${\mathbf{v}}^{\top }(\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}})\mathbf{v}=0$ for every $\mathbf{v}$ — the passivity / energy-balance identity, now established for the square $13\times 13$ augmentation.

nullspace_damping_gas

P4 engine instantiation. The damped self-motion state $({\tilde{x}}_n,v_n)\in \mathbb{R}\times \mathbb{R}$ (from $u_n=-k_n{\tilde{x}}_n-d_n{v}_n$) is the driven subsystem of the sealed cascade_gas: reshaped Lyapunov $V_n$ lower-bounded by a class-${\mathcal{K}}_{\infty }$ ${\alpha }_1$ (hsand), driven by the vanishing task output $x_2$ through $v_n^{\prime }\le -a{V}_n+c\Vert x_2\Vert$ (hdi). A vanishing driver gives $(({\tilde{x}}_n,v_n),x_2)\to 0$.

nullspace_damping_driven

P4 assembled (§6, “re-run the cascade”). The driving output is the full task block — the com→coupled cascade propIV1_cascade_gas gives $({\mathbf{x}}_t,{\mathbf{\phi }}_c{z}_0)\to 0$ — fed as the vanishing driver of the null-space cascade. Conclusion: the joint (null-space, task) state $(({\tilde{x}}_n,v_n),({\mathbf{x}}_t,{\mathbf{\phi }}_c{z}_0))\to 0$. Two sealed cascade stones composed; no fresh convergence proof.

P3 — the §5 lemma, re-derivable by hand

Quoting derivation_7dof.md §5:

Lemma (passivity survives). If $\dot{\mathbf{M}}-2\mathbf{C}$ is skew, so is $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}$. Proof. Two ingredients: the product rule, and $\frac{d}{dt}({\mathbf{\Gamma }}_a^{-1})=-{\mathbf{\Gamma }}_a^{-1}{\dot{\mathbf{\Gamma }}}_a{\mathbf{\Gamma }}_a^{-1}$. Differentiate $\hat{\mathbf{M}}$, subtract $2\hat{\mathbf{C}}$, and collect — two of the six terms cancel, leaving $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}={\mathbf{\Gamma }}_a^{-\top }(\dot{\mathbf{M}}-2\mathbf{C}){\mathbf{\Gamma }}_a^{-1}+(\mathbf{S}-{\mathbf{S}}^{\top })$, $\mathbf{S}\triangleq {\mathbf{\Gamma }}_a^{-\top }\mathbf{M}{\mathbf{\Gamma }}_a^{-1}{\dot{\mathbf{\Gamma }}}_a{\mathbf{\Gamma }}_a^{-1}$. A change of basis of a skew matrix is skew, and $\mathbf{S}-{\mathbf{S}}^{\top }$ is skew by construction. Sum of skews is skew. $■$

Writing $\mathbf{P}={\mathbf{\Gamma }}_a^{-1}$, the six product-rule terms of $\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}}$ and $\hat{\mathbf{C}}={\mathbf{P}}^{\top }(\mathbf{C}\mathbf{P}+\mathbf{M}\dot{\mathbf{P}})$ collect to

$$\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}={\mathbf{P}}^{\top }(\dot{\mathbf{M}}-2\mathbf{C})\mathbf{P}+\underset{\text{remainder}}{\underbrace{({\dot{\mathbf{P}}}^{\top }\mathbf{M}\mathbf{P}-{\mathbf{P}}^{\top }\mathbf{M}\dot{\mathbf{P}})}}$$

and substituting $\dot{\mathbf{P}}=-\mathbf{P}\dot{\mathbf{G}}\mathbf{P}$ (inv_deriv_eq) with ${\mathbf{M}}^{\top }=\mathbf{M}$ turns the remainder into exactly $\mathbf{S}-{\mathbf{S}}^{\top }$, since ${\mathbf{S}}^{\top }=({\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}\dot{\mathbf{G}}\mathbf{P}{)}^{\top }={\mathbf{P}}^{\top }{\dot{\mathbf{G}}}^{\top }{\mathbf{P}}^{\top }\mathbf{M}\mathbf{P}$ absorbs the transposed inverse-derivative term. This is augmented_passivity_decomp; SymPy pin (B) certifies the identity symbolically before any Lean.

The two hypotheses are exactly those of the sealed transport: symmetry of $\mathbf{M}$ and the Christoffel factorization in the original coordinates. Nothing about ${\mathbf{\Gamma }}_a$ beyond invertibility (through the product rule) is used — so this holds for any smooth invertible ${\mathbf{\Gamma }}_a(t)$, the wide-then-squared $13\times 13$ augmentation being one instance. augmented_passivity_skew then reads the skew off the decomposition, and augmented_passivity_identity off the skew (the sealed dotProduct_mulVec_self_of_skew, a real skew quadratic form vanishes).

Relation to the sealed factorization route

passivity_transport already proves the same skew and eq-23 conclusion for any invertible time-varying transform through the factorization form $\dot{\hat{\mathbf{M}}}=\hat{\mathbf{C}}+{\hat{\mathbf{C}}}^{\top }$ — transported_skew / transported_passivity_identity, both polymorphic in the index type and therefore already covering the $13\times 13$ augmentation with no size hypothesis. This module is the paper’s own §5 additive route (congruence + (S − Sᵀ)) made explicit, resting on the new inv_deriv_eq step; the two routes are independent kernel-checked confirmations of the same fact.

The honest P3 boundary — Ĉ is NOT block-diagonal

From derivation_7dof.md §6/P3:

P3. Coriolis cross-terms between $v_n$ and $({\mathbf{\omega }}_b,{\mathbf{\nu }}_e^{\oplus })$ — expect them to EXIST. Inertia decoupling is pointwise in $q$; $\hat{\mathbf{M}}(q)$ varies with configuration, and its rate enters the off-diagonal blocks of $\hat{\mathbf{C}}$. These terms do not break passivity (§5), but they couple $v_n$ to the task dynamics; do not claim a block-diagonal $\hat{\mathbf{C}}$.

The transformed inertia $\hat{\mathbf{M}}$ is block-diagonal (pin (C): the self-motion is $\mathbf{M}$-orthogonal to every task velocity, ${\hat{m}}_n={\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}>0$). The transformed Coriolis $\hat{\mathbf{C}}$ is not: the rate $\dot{\hat{\mathbf{M}}}$ populates the off-diagonal blocks. What P3 establishes is that these genuinely-present cross-terms are workless — passivity is safe — and it is precisely they that DRIVE the null-space in P4. Any statement that $\hat{\mathbf{C}}$ is block-diagonal would be false and is not claimed here.

P4 — closed-loop null-space damping

With $\hat{\mathbf{M}}$ block-diagonal (hat m_n > 0) the self-motion obeys ${\hat{m}}_n{\dot{v}}_n=u_n+(\text{cross-Coriolis drive})$, and ${\dot{\tilde{x}}}_n=v_n$. Under $u_n=-k_n{\tilde{x}}_n-d_n{v}_n$ the pair $({\tilde{x}}_n,v_n)$ is a damped oscillator driven by the task-block cross-terms — a textbook cascade whose driving output is the task state, which the sealed Prop IV.1 (propIV1_cascade_gas, cascade) already sends to the origin. So P4 is assembly over the sealed cascade engine, not a new convergence proof: nullspace_damping_gas instantiates cascade_gas with the null-space as the driven block, and nullspace_damping_driven discharges the driver from propIV1_cascade_gas.

The reshaped Lyapunov. The raw mechanical energy $\frac{1}{2}{\hat{m}}_n{v}_n^2+\frac{1}{2}{k}_n{\tilde{x}}_n^2$ does not satisfy the proportional inequality $\dot{V}\le -aV+c\Vert x_2\Vert$ — its rate $-d_n{v}_n^2+v_{n}w$ has no $-{\tilde{x}}_n^2$ term, so ${\tilde{x}}_n$ does not decrease when $v_n=0$. The reshaped $V_n=\frac{1}{2}{\hat{m}}_n{v}_n^2+\frac{1}{2}{k}_n{\tilde{x}}_n^2+\epsilon {\hat{m}}_n{\tilde{x}}_n{v}_n$ (Panteley Prop 1 shape, small $\epsilon$) is coercive and, on a bounded orbit, does satisfy it. Pin (D) exhibits concrete ${\hat{m}}_n,k_n,d_n,\epsilon$ with $a=0.399>0$ and $c=6$ over $2\times 10^5$ box draws. This is why hsand (the ${\mathcal{K}}_{\infty }$ sandwich) and hdi (the interconnection inequality) enter as named modelling inputs — the same status they carry throughout cascade — rather than being re-derived; the pin shows they are realizable for the null-space, not assumed into existence.

Out of scope (flagged design decision, not a proof target): the null space is one-dimensional but three secondary objectives compete for it (singular-value maximization, envelope clearance, pan-centering). Allocating one DOF among three objectives is a data-driven weighting/scheduling decision, made explicitly elsewhere.

Interfaces left open (honest scope)

• P3: none. The five passivity theorems are pure finite-dimensional algebra over a CommRing; they take only ${\mathbf{M}}^{\top }=\mathbf{M}$ and the original-coordinate Christoffel factorization, and discharge both from hypotheses that are physical facts. The product-rule naming of $\dot{\hat{\mathbf{M}}}$ and the $\mathbf{P}={\mathbf{\Gamma }}_a^{-1}$ identification are the same statement-level scaffolding passivity_transport draws (pin (C) certifies the concrete ${\mathbf{\Gamma }}_a$ structure); no Flow-level or analytic hypothesis enters P3.
• P4: the cascade interfaces, inherited unchanged from cascade — hsand/hdi (the reshaped-Lyapunov sandwich and interconnection inequality, Panteley Prop 1 / eq 35), the applier-side regularity hvc/hv, and — via propIV1_cascade_gas — IsSolutionTo (flow existence on $\Omega$), the discharged hcpt/ForwardPrecompact, and the SPD-operator hypotheses (discharged for concrete matrices by ComLaSalleMatrix). The null-space is a new consumer of hsand/hdi; it opens no new interface family. See interfaces.

Sources and provenance

• giordano2019coordinated (RA-L 2019) — the coordinated-control framing paper; assumes a nonredundant arm (“Let us assume a nonredundant manipulator”). The redundant extension formalized here is the new content.
• ott2008cartesian Lemma 3.2 — the Christoffel skew-symmetry $\dot{\mathbf{M}}=\mathbf{C}+{\mathbf{C}}^{\top }\Rightarrow \dot{\mathbf{\Lambda }}-2\mathbf{\mu }$ skew, the reused stone (via passivity_transport, passivity_identity).
• panteley2001growth — the Panteley–Loría cascade (Lemma 2), the reused P4 engine (via cascade).
• khatib1987unified — the dynamically-consistent (inertia-weighted) generalized inverse; the sense in which ${\mathbf{z}}_a={\hat{\mathbf{k}}}^{\top }\mathbf{M}/({\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}})$ is canonical.
• Giordano thesis (whole-body coordinated control, §5.2 redundant formulation + §5.8c damping law) — the direct prior art for both P3 (his “internal Coriolis stays fully coupled” is P3 in print) and P4 (his finite-$d$ damping law). Not yet corpus-filed — plain-text citation, flagged.
• Nakamura (redundant-manipulator null-space reconstruction) — the classical null-space fiber-reconstruction reference. On disk, not yet corpus-filed — plain-text citation, flagged.

SymPy / NumPy pin

pin_seven_dof.py in this directory, run under new-pin-env, all blocks PASS:

• (A) inverse derivative — $\dot{\mathbf{P}}=-\mathbf{P}\dot{\mathbf{G}}\mathbf{P}$ both as the algebraic solve of the product-rule relation and as an honest $\frac{d}{dt}(\mathbf{A}+t\mathbf{B}{)}^{-1}$.
• (B) §5 additive decomposition — symbolic $n=3$, $\mathbf{M}$ symmetric, $\dot{\mathbf{M}}:=\mathbf{C}+{\mathbf{C}}^{\top }$: the residual $(\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}})-[{\mathbf{P}}^{\top }(\dot{\mathbf{M}}-2\mathbf{C})\mathbf{P}+(\mathbf{S}-{\mathbf{S}}^{\top })]$ is the zero matrix; plus $\mathbf{S}-{\mathbf{S}}^{\top }$ skew and congruence-of-skew. This is the exact identity augmented_passivity_decomp formalizes.
• (C) concrete 13-dim model — a structured $\mathbf{\Gamma }\in {\mathbb{R}}^{12\times 13}$ with prescribed 1-D kernel $\hat{\mathbf{k}}$, SPD $\mathbf{M}$, the square ${\mathbf{\Gamma }}_a$: $\Vert \mathbf{\Gamma }\hat{\mathbf{k}}\Vert =6\times 10^{-16}$, ${\max }_i|{\hat{\mathbf{k}}}^{\top }\mathbf{M}{\mathbf{c}}_i|=2\times 10^{-14}$ (M-orthogonality), block-diagonal $\hat{\mathbf{M}}$ (off-diagonal $10^{-14}$), ${\hat{m}}_n={\hat{\mathbf{k}}}^{\top }\mathbf{M}\hat{\mathbf{k}}$, ${\mathbf{c}}_{13}=\hat{\mathbf{k}}$, and a time-varying draw with $\dot{\hat{\mathbf{M}}}-2\hat{\mathbf{C}}$ numerically skew ($2\times 10^{-7}$).
• (D) §6/P4 reshaped Lyapunov — the raw energy fails the proportional decrease; the reshaped $V_{\epsilon }$ is coercive and satisfies $V_{\epsilon }^{\prime }\le -a{V}_{\epsilon }+c|w|$ with $a=0.399$, $c=6$ over $2\times 10^5$ box draws.

The machine seal

SevenDof.lean in this directory (build copy ~/lean/ctrllib/Ctrllib/SevenDof.lean, registered in Ctrllib.lean; this directory’s copy is the tracked source of truth). Verbatim #print axioms (full-library build 2026-07-09, 2656 jobs):

info: 'Ctrllib.inv_deriv_eq' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.congruence_skew' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.augmented_passivity_decomp' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.augmented_passivity_skew' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.augmented_passivity_identity' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.nullspace_damping_gas' depends on axioms: [propext, Classical.choice, Quot.sound]
info: 'Ctrllib.nullspace_damping_driven' depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx; every public theorem’s axiom set is $\subseteq \{$propext, Classical.choice, Quot.sound$\}$.