On 7 May 2012, at 00:22, Bill Richter wrote:
> John, that's definitely an example of poor hol_light readability, and
> I vastly prefer my pseudo-TeX:
>
> (x1^2 + x2^2 + x3^2 + x4^2) (y1^2 + y2^2 + y3^2 + y4^2)
> =
> (x1 y1 - x2 y2 - x3 y3 - x4 y4)^2 +
> (x1 y2 + x2 y1 + x3 y4 - x4 y3)^2 +
> (x1 y3 - x2 y4 + x3 y1 + x4 y2)^2 +
> (x1 y4 + x2 y3 - x3 y2 + x4 y1)^2
>
>
>
> Those are amazing equations, and adding them we get 0, and this proves
> your equation is true. Wow! How did anyone think your equation up?
What the equations say is that the (squared) norm function on the quaternions
is multiplicative N(X)N(Y) = N(XY). See
http://en.wikipedia.org/wiki/Lagrange's_four-square_theorem. So with 20-20
hindsight, it becomes a rather natural conjecture to make (by analogy with the
same statement for the reals and the complex numbers). I imagine Hamilton would
have found a mechanized decision procedure for real arithmetic a considerable
boon.
Regards,
Rob.
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
