The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Dear Daniel,

And a supposed fixpoint (one of the two points on the rotation axis on
the sphere) is (x/r, y/r, z/r) such that
   x = m₃₂ - m₂₃
   y = m₁₃ - m₃₁
   z = m₂₁ - m₁₂
   r = √ (x² + y² + z²)

First: is it correct?

 

I am not sure it is correct, i have never seen identities like these. It seems you are attempting to brute force theorems about rotations in three dimensions. In my experience these are a bit too hard for brute forcing them in order to get useful results. At the very least it will not be a very pleasant experience. A more intelligent approach might be more fun. First note that the eigenvalue problem of this matrix has a real solution because a polynomial equation of degree three always has a real solution. Then there are two possibilities. Firstly, there can be tree real solutions. These can only be 1 or -1 because a rotation preserves the sphere. Because the determinant is 1, at least one of them must be 1. There is your fixed point and also its negative is a fixed point. Secondly, there can be one real solution and two complex ones that are each others complex conjugate. Because an orthogonal matrix is also unitary, these eigenvalues must be of length 1 in the complex plane, so they are (1, e^i phi, e^-i phi) because the determinant is 1. The eigenvector of 1 gives you your other fixed point.

Good luck!

Chris