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]

noncomputable abbrev Real.goldenRatio : ℝ

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

@[reducible, inline]

noncomputable abbrev Real.goldenConj : ℝ

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

def goldenRatio.termφ : Lean.ParserDescr

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

def goldenRatio.termψ : Lean.ParserDescr

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

theorem Real.inv_goldenRatio : goldenRatio⁻¹ = -goldenConj

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

theorem Real.inv_goldenConj : goldenConj⁻¹ = -goldenRatio

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

@[simp]

theorem Real.goldenRatio_mul_goldenConj : goldenRatio * goldenConj = -1

@[simp]

theorem Real.goldenConj_mul_goldenRatio : goldenConj * goldenRatio = -1

@[simp]

theorem Real.goldenRatio_add_goldenConj : goldenRatio + goldenConj = 1

theorem Real.one_sub_goldenConj : 1 - goldenRatio = goldenConj

theorem Real.one_sub_goldenRatio : 1 - goldenConj = goldenRatio

@[simp]

theorem Real.goldenRatio_sub_goldenConj : goldenRatio - goldenConj = √5

theorem Real.goldenRatio_pow_sub_goldenRatio_pow (n : ℕ) : goldenRatio ^ (n + 2) - goldenRatio ^ (n + 1) = goldenRatio ^ n

@[simp]

theorem Real.goldenRatio_sq : goldenRatio ^ 2 = goldenRatio + 1

@[simp]

theorem Real.goldenConj_sq : goldenConj ^ 2 = goldenConj + 1

theorem Real.goldenRatio_pos : 0 < goldenRatio

theorem Real.goldenRatio_ne_zero : goldenRatio ≠ 0

theorem Real.one_lt_goldenRatio : 1 < goldenRatio

theorem Real.goldenRatio_lt_two : goldenRatio < 2

theorem Real.goldenConj_neg : goldenConj < 0

theorem Real.goldenConj_ne_zero : goldenConj ≠ 0

theorem Real.neg_one_lt_goldenConj : -1 < goldenConj

Irrationality

theorem Real.goldenRatio_irrational : Irrational goldenRatio

The golden ratio is irrational.

theorem Real.goldenConj_irrational : Irrational goldenConj

The conjugate of the golden ratio is irrational.

Links with Fibonacci sequence

def Real.fibRec {α : Type u_1} [CommSemiring α] : LinearRecurrence α

The recurrence relation satisfied by the Fibonacci sequence.

theorem Real.fibRec_charPoly_eq {β : Type u_2} [CommRing β] : fibRec.charPoly = Polynomial.X ^ 2 - (Polynomial.X + 1)

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

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

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

theorem Real.geom_goldenRatio_isSol_fibRec : fibRec.IsSolution fun (x : ℕ) => goldenRatio ^ x

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

theorem Real.geom_goldenConj_isSol_fibRec : fibRec.IsSolution fun (x : ℕ) => goldenConj ^ x

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

theorem Real.coe_fib_eq' : (fun (n : ℕ) => ↑(Nat.fib n)) = fun (n : ℕ) => (goldenRatio ^ n - goldenConj ^ n) / √5

Binet's formula as a function equality.

theorem Real.coe_fib_eq (n : ℕ) : ↑(Nat.fib n) = (goldenRatio ^ n - goldenConj ^ n) / √5

Binet's formula as a dependent equality.

theorem Real.coe_intFib_eq (n : ℤ) : ↑(Int.fib n) = (goldenRatio ^ n - goldenConj ^ n) / √5

Binet's formula for integer values.

theorem Real.fib_succ_sub_goldenRatio_mul_fib (n : ℕ) : ↑(Nat.fib (n + 1)) - goldenRatio * ↑(Nat.fib n) = goldenConj ^ n

Relationship between the Fibonacci Sequence, the golden ratio, and its conjugate's exponents.

theorem Real.goldenConj_mul_fib_succ_add_fib (n : ℕ) : goldenConj * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = goldenConj ^ (n + 1)

Relationship between the Fibonacci Sequence, the conjugate of the golden ratio, and its exponents.

theorem Real.goldenRatio_mul_fib_succ_add_fib (n : ℕ) : goldenRatio * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = goldenRatio ^ (n + 1)

Relationship between the Fibonacci Sequence, the golden ratio, and its exponents.

theorem Real.fib_succ_sub_goldenConj_mul_fib (n : ℕ) : ↑(Nat.fib (n + 1)) - goldenConj * ↑(Nat.fib n) = goldenRatio ^ n

Relationship between the Fibonacci Sequence, exponents of the golden ratio, and its conjugate.