AGORA v5 Lemma 1 symbolic check
P shape: (2, 3)
c = row1 x row2 =
Matrix([[p12*p23 - p13*p22], [-p11*p23 + p13*p21], [p11*p22 - p12*p21]])
P*c simplifies to:
Matrix([[0], [0]])
quadratic identity (should be 0):
0
Vdot = -x^T(K+P^T P)x =
-k*x1**2 - k*x2**2 - k*x3**2 - p11**2*x1**2 - 2*p11*p12*x1*x2 - 2*p11*p13*x1*x3 - p12**2*x2**2 - 2*p12*p13*x2*x3 - p13**2*x3**2 - p21**2*x1**2 - 2*p21*p22*x1*x2 - 2*p21*p23*x1*x3 - p22**2*x2**2 - 2*p22*p23*x2*x3 - p23**2*x3**2
For k>0, x^T(K+P^T P)x = k||x||^2 + ||Px||^2 > 0 for x != 0.
m=2 determinant condition det(P2)=
a*d - b*c2
If det(P2) != 0, ker(P2)={0}; therefore no nonzero c satisfies P2*c=0.
