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.

source

def golden_ratio :

ℝ

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

Equations

golden_ratio = (1 + real.sqrt 5) / 2

source

def golden_conj :

ℝ

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

Equations

golden_conj = (1 - real.sqrt 5) / 2

source

theorem inv_gold :

golden_ratio ⁻¹ = -golden_conj

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

source

theorem inv_gold_conj :

golden_conj ⁻¹ = -golden_ratio

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

source

@[simp]

theorem gold_mul_gold_conj :

golden_ratio * golden_conj = -1

source

@[simp]

theorem gold_conj_mul_gold :

golden_conj * golden_ratio = -1

source

@[simp]

theorem gold_add_gold_conj :

golden_ratio + golden_conj = 1

source

theorem one_sub_gold_conj :

1 - golden_ratio = golden_conj

source

theorem one_sub_gold :

1 - golden_conj = golden_ratio

source

@[simp]

theorem gold_sub_gold_conj :

golden_ratio - golden_conj = real.sqrt 5

source

@[simp]

theorem gold_sq :

golden_ratio ^ 2 = golden_ratio + 1

source

@[simp]

theorem gold_conj_sq :

golden_conj ^ 2 = golden_conj + 1

source

theorem gold_pos :

0 < golden_ratio

source

theorem gold_ne_zero :

golden_ratio ≠ 0

source

theorem one_lt_gold :

1 < golden_ratio

source

theorem gold_conj_neg :

golden_conj < 0

source

theorem gold_conj_ne_zero :

golden_conj ≠ 0

source

theorem neg_one_lt_gold_conj :

-1 < golden_conj

Irrationality

source

theorem gold_irrational :

irrational golden_ratio

The golden ratio is irrational.

source

theorem gold_conj_irrational :

irrational golden_conj

The conjugate of the golden ratio is irrational.

Links with Fibonacci sequence

source

def fib_rec {α : Type u_1} [comm_semiring α] :

linear_recurrence α

The recurrence relation satisfied by the Fibonacci sequence.

Equations

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

source

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

fib_rec.char_poly = polynomial.X ^ 2 - (polynomial.X + 1)

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

source

theorem fib_is_sol_fib_rec {α : Type u_1} [comm_semiring α] :

fib_rec.is_solution (λ (x : ℕ), ↑(x.fib))

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

source

theorem geom_gold_is_sol_fib_rec :

fib_rec.is_solution (has_pow.pow golden_ratio)

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

source

theorem geom_gold_conj_is_sol_fib_rec :

fib_rec.is_solution (has_pow.pow golden_conj)

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

source

theorem real.coe_fib_eq' :

(λ (n : ℕ), ↑(n.fib)) = λ (n : ℕ), (golden_ratio ^ n - golden_conj ^ n) / real.sqrt 5

Binet's formula as a function equality.

source

theorem real.coe_fib_eq (n : ℕ) :

↑(n.fib) = (golden_ratio ^ n - golden_conj ^ n) / real.sqrt 5

Binet's formula as a dependent equality.

mathlib documentation

data.real.golden_ratio

The golden ratio and its conjugate

Irrationality

Links with Fibonacci sequence

General documentation

Additional documentation

Library

mathlib documentation

data.​real.​golden_ratio

The golden ratio and its conjugate

Irrationality

Links with Fibonacci sequence

General documentation

Additional documentation

Library

data.real.golden_ratio