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

@[reducible, inline]

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

Equations
Instances For
@[reducible, inline]
abbrev goldenConj :

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

Equations
Instances For

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

Equations
Instances For

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

Equations
Instances For
theorem inv_gold :

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

theorem inv_goldConj :

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

@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem gold_sq :
@[simp]
theorem goldConj_sq :
=
theorem gold_pos :

## Irrationality #

theorem gold_irrational :

The golden ratio is irrational.

The conjugate of the golden ratio is irrational.

def fibRec {α : Type u_1} [] :

The recurrence relation satisfied by the Fibonacci sequence.

Equations
• fibRec = { order := 2, coeffs := ![1, 1] }
Instances For
theorem fibRec_charPoly_eq {β : Type u_2} [] :
fibRec.charPoly = Polynomial.X ^ 2 - (Polynomial.X + 1)

The characteristic polynomial of fibRec is X² - (X + 1).

theorem fib_isSol_fibRec {α : Type u_1} [] :
fibRec.IsSolution fun (x : ) => x.fib

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

theorem geom_gold_isSol_fibRec :
fibRec.IsSolution fun (x : ) =>

The geometric sequence fun n ↦ φ^n is a solution of fibRec.

theorem geom_goldConj_isSol_fibRec :
fibRec.IsSolution fun (x : ) =>

The geometric sequence fun n ↦ ψ^n is a solution of fibRec.

theorem Real.coe_fib_eq' :
(fun (n : ) => n.fib) = fun (n : ) => ( - ) / 5

Binet's formula as a function equality.

theorem Real.coe_fib_eq (n : ) :
n.fib = ( - ) / 5

Binet's formula as a dependent equality.

theorem fib_golden_conj_exp (n : ) :
(n + 1).fib - goldenRatio * n.fib =

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

theorem fib_golden_exp' (n : ) :
goldenRatio * (n + 1).fib + n.fib = goldenRatio ^ (n + 1)

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