geom_goldConj_isSol_fibRec
theorem geom_goldConj_isSol_fibRec : fibRec.IsSolution fun x => goldenConj ^ x
This theorem states that the geometric sequence defined by the power of the conjugate of the golden ratio, represented as `ψ^n` where `n` is the sequence index and `ψ` is `(1 - √5) / 2`, is a solution of the Fibonacci recurrence relation. The Fibonacci recurrence relation is defined as a sequence where each element is the sum of the two preceding ones (coefficients are `[1, 1]`), commencing from the second term.
More concisely: The sequence defined by the power of the conjugate of the golden ratio, `ψ^n` where `ψ = (1 - √5) / 2`, is a solution of the Fibonacci recurrence relation `X(n+1) = X(n) + X(n-1)` with initial values `X(0) = 0` and `X(1) = 1`.
|
fibRec_charPoly_eq
theorem fibRec_charPoly_eq :
∀ {β : Type u_2} [inst : CommRing β], fibRec.charPoly = Polynomial.X ^ 2 - (Polynomial.X + 1)
This theorem states that the characteristic polynomial of the Fibonacci recurrence relation is `X² - (X + 1)`. In other words, if we define a recurrence relation by `fibRec` that describes the Fibonacci sequence in the context of commutative rings, the polynomial that characterizes this recurrence relation, when expressed in terms of `X`, a variable of the polynomial ring, will be `X² - (X + 1)`. This is a universal property and holds for any commutative ring `β`.
More concisely: The characteristic polynomial of the Fibonacci recurrence relation `X��₂ - Xⁱ - 1` holds in any commutative ring.
|
fib_golden_exp'
theorem fib_golden_exp' : ∀ (n : ℕ), goldenRatio * ↑(n + 1).fib + ↑n.fib = goldenRatio ^ (n + 1)
This theorem states that for any natural number `n`, the product of the golden ratio and the Fibonacci number of `(n + 1)` added to the Fibonacci number of `n` is equal to the golden ratio raised to the power of `(n + 1)`. In simple terms, this theorem expresses a relationship between the Fibonacci sequence, the Golden Ratio, and its exponents. It highlights an interesting property of the Fibonacci sequence where its relation with the Golden Ratio can be expressed in terms of powers of the Golden Ratio.
More concisely: For any natural number `n`, the golden ratio raised to the power of `(n + 1)` equals the Fibonacci number of `(n + 1)` multiplied by the golden ratio plus the Fibonacci number of `n`.
|
inv_gold
theorem inv_gold : goldenRatio⁻¹ = -goldenConj
The theorem `inv_gold` states that the multiplicative inverse (or reciprocal) of the golden ratio, denoted as `φ := (1 + √5)/2`, is equal to the opposite (or negative) of its conjugate, denoted as `ψ := (1 - √5)/2`. In simpler terms, if you take 1 divided by the golden ratio, the result will be the negative of the conjugate of the golden ratio.
More concisely: The golden ratio's multiplicative inverse is equal to the negation of its conjugate: `(1 + √5)/2 * (1 - √5)/(1 + √5) = -(1 - √5)/2`.
|
fib_golden_conj_exp
theorem fib_golden_conj_exp : ∀ (n : ℕ), ↑(n + 1).fib - goldenRatio * ↑n.fib = goldenConj ^ n
This theorem states that for any natural number `n`, the difference between the Fibonacci number of `n+1` and the product of the golden ratio and the Fibonacci number of `n` equals the power of the golden ratio's conjugate raised to `n`. In other words, if we denote the Fibonacci sequence as `F(n)`, the golden ratio as `φ` and its conjugate as `ψ`, the theorem can be written in mathematical notation as `F(n+1) - φ * F(n) = ψ^n` for all natural numbers `n`.
More concisely: For any natural number `n`, the difference between the Fibonacci number `F(n+1)` and the product of the golden ratio `φ` and `F(n)` equals the power of the conjugate of the golden ratio `ψ` raised to `n`: `F(n+1) - φ * F(n) = ψ^n`.
|
geom_gold_isSol_fibRec
theorem geom_gold_isSol_fibRec : fibRec.IsSolution fun x => goldenRatio ^ x
This theorem states that the geometric sequence defined by the function `fun n ↦ φ^n`, where `φ` is the golden ratio `(1 + √5)/2`, satisfies the Fibonacci recurrence relation. In other words, each term in the sequence is the sum of the two preceding ones, which is the defining property of the Fibonacci sequence.
More concisely: The sequence defined by the function `n => φ^n` where `φ = (1 + √5)/2 satisfies the Fibonacci recurrence relation, i.e., for all `n`, `φ^(n+2) - φ^n * φ^(n+1) = 1`.
|
goldConj_irrational
theorem goldConj_irrational : Irrational goldenConj
The theorem `goldConj_irrational` states that the conjugate of the golden ratio, which is defined as `(1 - sqrt(5))/2`, is an irrational number. In other words, this number cannot be expressed as a ratio of two integers.
More concisely: The square root of 5 minus 1, divided by 2, is an irrational number.
|
Real.coe_fib_eq'
theorem Real.coe_fib_eq' : (fun n => ↑n.fib) = fun n => (goldenRatio ^ n - goldenConj ^ n) / √5
This is a formal statement of Binet's formula. It states that the Fibonacci sequence, when considered as a function on the natural numbers (the function `fun n => ↑n.fib`), can be expressed in terms of powers of the golden ratio (`goldenRatio`) and its conjugate (`goldenConj`). Specifically, the nth Fibonacci number is equal to `(goldenRatio ^ n - goldenConj ^ n) / √5`.
More concisely: The nth Fibonacci number is given by the formula (goldenRatio^n - goldenConj^n) / √5, where goldenRatio and goldenConj are the golden ratio and its conjugate, respectively.
|
Real.coe_fib_eq
theorem Real.coe_fib_eq : ∀ (n : ℕ), ↑n.fib = (goldenRatio ^ n - goldenConj ^ n) / √5
This theorem is a statement of Binet's formula in the context of natural numbers and real numbers. For each natural number 'n', the 'n'-th Fibonacci number (when considered as a real number) is equal to the difference of the 'n'-th power of the golden ratio and the 'n'-th power of the conjugate of the golden ratio, all divided by the square root of 5. Here, the golden ratio is defined as `(1 + √5)/2` and its conjugate is `(1 - √5)/2`.
More concisely: The n-th Fibonacci number, as a real number, is equal to ((1 + √5 / 2)^n - (1 - √5 / 2)^n) / √5.
|
inv_goldConj
theorem inv_goldConj : goldenConj⁻¹ = -goldenRatio
This theorem states that the multiplicative inverse (or reciprocal) of the golden conjugate is equal to the negation (or opposite) of the golden ratio. In other words, if `ψ := (1 - √5)/2` represents the golden conjugate and `φ := (1 + √5)/2` represents the golden ratio, then `1/ψ = -φ`.
More concisely: The golden conjugate's multiplicative inverse is equal to the negative of the golden ratio: 1/((1 - √5)/2) = -(1 + √5)/2.
|
fib_isSol_fibRec
theorem fib_isSol_fibRec : ∀ {α : Type u_1} [inst : CommSemiring α], fibRec.IsSolution fun x => ↑x.fib
This theorem states that the Fibonacci sequence (denoted by `fib`) is a solution to the recurrence relation `fibRec`. The recurrence relation `fibRec` is defined such that it is satisfied by the Fibonacci sequence, where the order is 2 and the coefficients are both 1. The theorem holds for any type `α` that forms a commutative semiring. This essentially means that the Fibonacci sequence follows the property where each number is the sum of the two preceding ones.
More concisely: The Fibonacci sequence `fib` satisfies the recurrence relation `fibRec` of order 2 and coefficients 1 in any commutative semiring.
|
gold_irrational
theorem gold_irrational : Irrational goldenRatio
This theorem states that the golden ratio is irrational. In mathematical terms, the golden ratio, denoted by `φ` and defined as `(1 + √5) / 2`, is not equal to any rational number. This means there are no integers `a` and `b` such that `φ = a / b`, which is the definition of a rational number.
More concisely: The golden ratio `(1 + √5) / 2` is not a rational number.
|