Cassini-Fricke Antiinvariant

Abstract

The Cassini-Fricke quadratic form is an alternating invariant of Binet recurrences.

Theorem 1.1 (Cassini-Fricke quadratic-form antiinvariant).

$$Q(u_{K+1},u_K)=u_{K+1}^2-u_{K+1}{u}_K-u_K^2=-5AB(-1{)}^K$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/CassiniFricke.cassini_fricke (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let phi and psi satisfy phi^2 = phi + 1, psi^2 = psi + 1, phi + psi = 1, and phipsi = -1 in a commutative ring. For the Binet sequence u_K = Aphi^K + Bpsi^K and the quadratic form Q(a,b) = a^2 - ab - b^2, the value Q(u_(K+1),u_K) is -5AB*(-1)^K. Taking A = -xphi and B = ypsi gives AB = xy, so the result is 5xy*(-1)^(K+1), exactly the source theorem’s Cassini-Fricke antiinvariant.

References

• Truth anchor: D5/S1/Recurrence/CassiniFricke.cassini_fricke