# mathlibdocumentation

data.real.golden_ratio

# 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]
noncomputable def golden_ratio  :

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

Equations
@[reducible]
noncomputable def golden_conj  :

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

Equations
theorem inv_gold  :

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

theorem inv_gold_conj  :

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

@[simp]
theorem gold_mul_gold_conj  :
@[simp]
theorem gold_conj_mul_gold  :
@[simp]
theorem one_sub_gold  :
@[simp]
theorem gold_sub_gold_conj  :
@[simp]
theorem gold_sq  :
@[simp]
theorem gold_conj_sq  :
theorem gold_pos  :
theorem gold_ne_zero  :
theorem one_lt_gold  :
theorem gold_conj_neg  :

## Irrationality #

The golden ratio is irrational.

The conjugate of the golden ratio is irrational.

def fib_rec {α : Type u_1}  :

The recurrence relation satisfied by the Fibonacci sequence.

Equations
theorem fib_rec_char_poly_eq {β : Type u_1} [comm_ring β] :

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

theorem fib_is_sol_fib_rec {α : Type u_1}  :

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

The geometric sequence λ n, φ^n is a solution of fib_rec.

The geometric sequence λ n, ψ^n is a solution of fib_rec.

theorem real.coe_fib_eq'  :
(λ (n : ), (nat.fib n)) = λ (n : ), - /

Binet's formula as a function equality.

theorem real.coe_fib_eq (n : ) :

Binet's formula as a dependent equality.