Documentation

Mathlib.NumberTheory.Real.GoldenRatio

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
@[reducible, inline]
abbrev Real.goldenRatio :
ℝ

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Real.goldenConj :
    ℝ

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

    Equations
    Instances For
      source
      def goldenRatio.termφ :
      Lean.ParserDescr

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

      Equations
      Instances For
        source
        def goldenRatio.termψ :
        Lean.ParserDescr

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

        Equations
        Instances For
          source
          theorem Real.inv_goldenRatio :
          goldenRatio⁻¹ = -goldenConj

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

          source
          @[deprecated Real.inv_goldenRatio (since := "2025-08-23")]
          theorem inv_gold :
          Real.goldenRatio⁻¹ = -Real.goldenConj

          Alias of Real.inv_goldenRatio.

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

          source
          theorem Real.inv_goldenConj :
          goldenConj⁻¹ = -goldenRatio

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

          source
          @[deprecated Real.inv_goldenConj (since := "2025-08-23")]
          theorem inv_goldConj :
          Real.goldenConj⁻¹ = -Real.goldenRatio

          Alias of Real.inv_goldenConj.

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

          source
          @[simp]
          theorem Real.goldenRatio_mul_goldenConj :
          goldenRatio * goldenConj = -1
          source
          @[deprecated Real.goldenRatio_mul_goldenConj (since := "2025-08-23")]
          theorem gold_mul_goldConj :
          Real.goldenRatio * Real.goldenConj = -1

          Alias of Real.goldenRatio_mul_goldenConj.

          source
          @[simp]
          theorem Real.goldenConj_mul_goldenRatio :
          goldenConj * goldenRatio = -1
          source
          @[deprecated Real.goldenConj_mul_goldenRatio (since := "2025-08-23")]
          theorem goldConj_mul_gold :
          Real.goldenConj * Real.goldenRatio = -1

          Alias of Real.goldenConj_mul_goldenRatio.

          source
          @[simp]
          theorem Real.goldenRatio_add_goldenConj :
          goldenRatio + goldenConj = 1
          source
          @[deprecated Real.goldenRatio_add_goldenConj (since := "2025-08-23")]
          theorem gold_add_goldConj :
          Real.goldenRatio + Real.goldenConj = 1

          Alias of Real.goldenRatio_add_goldenConj.

          source
          theorem Real.one_sub_goldenConj :
          1 - goldenRatio = goldenConj
          source
          @[deprecated Real.one_sub_goldenConj (since := "2025-08-23")]
          theorem one_sub_goldConj :
          1 - Real.goldenRatio = Real.goldenConj

          Alias of Real.one_sub_goldenConj.

          source
          theorem Real.one_sub_goldenRatio :
          1 - goldenConj = goldenRatio
          source
          @[deprecated Real.one_sub_goldenRatio (since := "2025-08-23")]
          theorem one_sub_gold :
          1 - Real.goldenConj = Real.goldenRatio

          Alias of Real.one_sub_goldenRatio.

          source
          @[simp]
          theorem Real.goldenRatio_sub_goldenConj :
          goldenRatio - goldenConj = √5
          source
          @[deprecated Real.goldenRatio_sub_goldenConj (since := "2025-08-23")]
          theorem gold_sub_goldConj :
          Real.goldenRatio - Real.goldenConj = √5

          Alias of Real.goldenRatio_sub_goldenConj.

          source
          theorem Real.goldenRatio_pow_sub_goldenRatio_pow (n : ℕ) :
          goldenRatio ^ (n + 2) - goldenRatio ^ (n + 1) = goldenRatio ^ n
          source
          @[deprecated Real.goldenRatio_pow_sub_goldenRatio_pow (since := "2025-08-23")]
          theorem Real.gold_pow_sub_gold_pow (n : ℕ) :
          goldenRatio ^ (n + 2) - goldenRatio ^ (n + 1) = goldenRatio ^ n

          Alias of Real.goldenRatio_pow_sub_goldenRatio_pow.

          source
          @[simp]
          theorem Real.goldenRatio_sq :
          goldenRatio ^ 2 = goldenRatio + 1
          source
          @[deprecated Real.goldenRatio_sq (since := "2025-08-23")]
          theorem gold_sq :
          Real.goldenRatio ^ 2 = Real.goldenRatio + 1

          Alias of Real.goldenRatio_sq.

          source
          @[simp]
          theorem Real.goldenConj_sq :
          goldenConj ^ 2 = goldenConj + 1
          source
          @[deprecated Real.goldenConj_sq (since := "2025-08-23")]
          theorem goldConj_sq :
          Real.goldenConj ^ 2 = Real.goldenConj + 1

          Alias of Real.goldenConj_sq.

          source
          theorem Real.goldenRatio_pos :
          0 < goldenRatio
          source
          @[deprecated Real.goldenRatio_pos (since := "2025-08-23")]
          theorem gold_pos :
          0 < Real.goldenRatio

          Alias of Real.goldenRatio_pos.

          source
          theorem Real.goldenRatio_ne_zero :
          goldenRatio ≠ 0
          source
          @[deprecated Real.goldenRatio_ne_zero (since := "2025-08-23")]
          theorem gold_ne_zero :
          Real.goldenRatio ≠ 0

          Alias of Real.goldenRatio_ne_zero.

          source
          theorem Real.one_lt_goldenRatio :
          1 < goldenRatio
          source
          @[deprecated Real.one_lt_goldenRatio (since := "2025-08-23")]
          theorem one_lt_gold :
          1 < Real.goldenRatio

          Alias of Real.one_lt_goldenRatio.

          source
          theorem Real.goldenRatio_lt_two :
          goldenRatio < 2
          source
          @[deprecated Real.goldenRatio_lt_two (since := "2025-08-23")]
          theorem gold_lt_two :
          Real.goldenRatio < 2

          Alias of Real.goldenRatio_lt_two.

          source
          theorem Real.goldenConj_neg :
          goldenConj < 0
          source
          @[deprecated Real.goldenConj_neg (since := "2025-08-23")]
          theorem goldConj_neg :
          Real.goldenConj < 0

          Alias of Real.goldenConj_neg.

          source
          theorem Real.goldenConj_ne_zero :
          goldenConj ≠ 0
          source
          @[deprecated Real.goldenConj_ne_zero (since := "2025-08-23")]
          theorem goldConj_ne_zero :
          Real.goldenConj ≠ 0

          Alias of Real.goldenConj_ne_zero.

          source
          theorem Real.neg_one_lt_goldenConj :
          -1 < goldenConj
          source
          @[deprecated Real.neg_one_lt_goldenConj (since := "2025-08-23")]
          theorem neg_one_lt_goldConj :
          -1 < Real.goldenConj

          Alias of Real.neg_one_lt_goldenConj.

          Irrationality #

          source
          theorem Real.goldenRatio_irrational :
          Irrational goldenRatio

          The golden ratio is irrational.

          source
          @[deprecated Real.goldenRatio_irrational (since := "2025-08-23")]
          theorem gold_irrational :
          Irrational Real.goldenRatio

          Alias of Real.goldenRatio_irrational.

          The golden ratio is irrational.

          source
          theorem Real.goldenConj_irrational :
          Irrational goldenConj

          The conjugate of the golden ratio is irrational.

          source
          @[deprecated Real.goldenConj_irrational (since := "2025-08-23")]
          theorem goldConj_irrational :
          Irrational Real.goldenConj

          Alias of Real.goldenConj_irrational.

          The conjugate of the golden ratio is irrational.

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

          The recurrence relation satisfied by the Fibonacci sequence.

          Equations
          Instances For
            source
            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).

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

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

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

            source
            @[deprecated Real.geom_goldenRatio_isSol_fibRec (since := "2025-08-23")]
            theorem geom_gold_isSol_fibRec :
            Real.fibRec.IsSolution fun (x : ℕ) => Real.goldenRatio ^ x

            Alias of Real.geom_goldenRatio_isSol_fibRec.

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

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

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

            source
            @[deprecated Real.geom_goldenConj_isSol_fibRec (since := "2025-08-23")]
            theorem Real.geom_goldConj_isSol_fibRec :
            fibRec.IsSolution fun (x : ℕ) => goldenConj ^ x

            Alias of Real.geom_goldenConj_isSol_fibRec.

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

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

            Binet's formula as a function equality.

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

            Binet's formula as a dependent equality.

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

            source
            @[deprecated Real.fib_succ_sub_goldenRatio_mul_fib (since := "2025-08-23")]
            theorem fib_golden_conj_exp (n : ℕ) :
            ↑(Nat.fib (n + 1)) - Real.goldenRatio * ↑(Nat.fib n) = Real.goldenConj ^ n

            Alias of Real.fib_succ_sub_goldenRatio_mul_fib.

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

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

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

            source
            @[deprecated Real.goldenRatio_mul_fib_succ_add_fib (since := "2025-08-23")]
            theorem fib_golden_exp' (n : ℕ) :
            Real.goldenRatio * ↑(Nat.fib (n + 1)) + ↑(Nat.fib n) = Real.goldenRatio ^ (n + 1)

            Alias of Real.goldenRatio_mul_fib_succ_add_fib.

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

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