# 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.

The conjugate of the golden ratio `ψ := (1 - √5)/2`

.

## Instances For

The inverse of the golden ratio is the opposite of its conjugate.

The opposite of the golden ratio is the inverse of its conjugate.

## Irrationality #

The conjugate of the golden ratio is irrational.

## Links with Fibonacci sequence #

The recurrence relation satisfied by the Fibonacci sequence.

## Instances For

The characteristic polynomial of `fibRec`

is `X² - (X + 1)`

.

As expected, the Fibonacci sequence is a solution of `fibRec`

.

The geometric sequence `fun n ↦ φ^n`

is a solution of `fibRec`

.

The geometric sequence `fun n ↦ ψ^n`

is a solution of `fibRec`

.

Binet's formula as a function equality.

Binet's formula as a dependent equality.