Some of the decomposition algorithms of Eigen are described as “proven”. I am someone who sometimes works on machine-checked proofs of code, so I am wondering what “proven” actually means here. I am thinking is most likely means that there is a hand proof (somewhere) of the algorithm but that the code itself has not been subjected to machine-checked proof. In any case, can someone point me to the proofs in question, please?

Regards, Eliot Moss, Professor Emeritus, UMass Amherst

I tried some quick web searches but could not readily find proofs because there are so many hits on class and other presentations on the various decompositions.