Documentation

Mathlib.Data.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.

@[reducible, inline]

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

Equations
Instances For
    @[reducible, inline]

    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

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

          @[deprecated Real.inv_goldenRatio (since := "2025-08-23")]

          Alias of Real.inv_goldenRatio.


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

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

          @[deprecated Real.inv_goldenConj (since := "2025-08-23")]

          Alias of Real.inv_goldenConj.


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

          @[deprecated Real.goldenRatio_mul_goldenConj (since := "2025-08-23")]

          Alias of Real.goldenRatio_mul_goldenConj.

          @[deprecated Real.goldenConj_mul_goldenRatio (since := "2025-08-23")]

          Alias of Real.goldenConj_mul_goldenRatio.

          @[deprecated Real.goldenRatio_add_goldenConj (since := "2025-08-23")]

          Alias of Real.goldenRatio_add_goldenConj.

          @[deprecated Real.one_sub_goldenConj (since := "2025-08-23")]

          Alias of Real.one_sub_goldenConj.

          @[deprecated Real.one_sub_goldenRatio (since := "2025-08-23")]

          Alias of Real.one_sub_goldenRatio.

          @[deprecated Real.goldenRatio_sub_goldenConj (since := "2025-08-23")]

          Alias of Real.goldenRatio_sub_goldenConj.

          @[deprecated Real.goldenRatio_pow_sub_goldenRatio_pow (since := "2025-08-23")]

          Alias of Real.goldenRatio_pow_sub_goldenRatio_pow.

          @[deprecated Real.goldenRatio_sq (since := "2025-08-23")]

          Alias of Real.goldenRatio_sq.

          @[deprecated Real.goldenConj_sq (since := "2025-08-23")]

          Alias of Real.goldenConj_sq.

          @[deprecated Real.goldenRatio_pos (since := "2025-08-23")]

          Alias of Real.goldenRatio_pos.

          @[deprecated Real.goldenRatio_ne_zero (since := "2025-08-23")]

          Alias of Real.goldenRatio_ne_zero.

          @[deprecated Real.one_lt_goldenRatio (since := "2025-08-23")]

          Alias of Real.one_lt_goldenRatio.

          @[deprecated Real.goldenRatio_lt_two (since := "2025-08-23")]

          Alias of Real.goldenRatio_lt_two.

          @[deprecated Real.goldenConj_neg (since := "2025-08-23")]

          Alias of Real.goldenConj_neg.

          @[deprecated Real.goldenConj_ne_zero (since := "2025-08-23")]

          Alias of Real.goldenConj_ne_zero.

          @[deprecated Real.neg_one_lt_goldenConj (since := "2025-08-23")]

          Alias of Real.neg_one_lt_goldenConj.

          Irrationality #

          The golden ratio is irrational.

          @[deprecated Real.goldenRatio_irrational (since := "2025-08-23")]

          Alias of Real.goldenRatio_irrational.


          The golden ratio is irrational.

          The conjugate of the golden ratio is irrational.

          @[deprecated Real.goldenConj_irrational (since := "2025-08-23")]

          Alias of Real.goldenConj_irrational.


          The conjugate of the golden ratio is irrational.

          The recurrence relation satisfied by the Fibonacci sequence.

          Equations
          Instances For

            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.

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

            @[deprecated Real.geom_goldenRatio_isSol_fibRec (since := "2025-08-23")]

            Alias of Real.geom_goldenRatio_isSol_fibRec.


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

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

            @[deprecated Real.geom_goldenConj_isSol_fibRec (since := "2025-08-23")]

            Alias of Real.geom_goldenConj_isSol_fibRec.


            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 : ) :

            Binet's formula as a dependent equality.

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

            @[deprecated Real.fib_succ_sub_goldenRatio_mul_fib (since := "2025-08-23")]

            Alias of Real.fib_succ_sub_goldenRatio_mul_fib.


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

            Relationship between the Fibonacci Sequence, Golden Ratio and its exponents

            @[deprecated Real.goldenRatio_mul_fib_succ_add_fib (since := "2025-08-23")]
            theorem fib_golden_exp' (n : ) :

            Alias of Real.goldenRatio_mul_fib_succ_add_fib.


            Relationship between the Fibonacci Sequence, Golden Ratio and its exponents