# 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 golden ratio `φ := (1 + √5)/2`

.

## Equations

- goldenRatio = (1 + √5) / 2

## Instances For

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

.

## Equations

- goldenConj = (1 - √5) / 2

## Instances For

The golden ratio `φ := (1 + √5)/2`

.

## Equations

- goldenRatio.termφ = Lean.ParserDescr.node `goldenRatio.termφ 1024 (Lean.ParserDescr.symbol "φ")

## Instances For

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

.

## Equations

- goldenRatio.termψ = Lean.ParserDescr.node `goldenRatio.termψ 1024 (Lean.ParserDescr.symbol "ψ")

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

## Equations

- fibRec = { order := 2, coeffs := ![1, 1] }

## Instances For

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.

Relationship between the Fibonacci Sequence, Golden Ratio and its conjugate's exponents -

Relationship between the Fibonacci Sequence, Golden Ratio and its exponents -