The golden ratio and its conjugate #
This file defines the golden ratio
φ := (1 + √5)/2 and its conjugate
ψ := (1 - √5)/2, which are the two real roots of
X² - X - 1.
Along with various computational facts about them, we prove their irrationality, and we link them to the Fibonacci sequence by proving Binet's formula.