Nat.fib_add_two_strictMono
theorem Nat.fib_add_two_strictMono : StrictMono fun n => (n + 2).fib
The theorem `Nat.fib_add_two_strictMono` states that the function which maps a natural number `n` to the Fibonacci of `n + 2` is strictly monotone. In other words, for all natural numbers `a` and `b`, if `a` is less than `b`, then the Fibonacci of `a + 2` is less than the Fibonacci of `b + 2`. This is a property of the Fibonacci function where the output strictly increases as the input natural number increases.
More concisely: The Fibonacci function is strictly increasing on natural numbers. (Equivalently, for all natural numbers `a` and `b` with `a < b`, `Fib(a+2)` < `Fib(b+2)`.)
|
Nat.fib_add_two
theorem Nat.fib_add_two : ∀ {n : ℕ}, (n + 2).fib = n.fib + (n + 1).fib
This theorem verifies the correctness of the Fibonacci sequence implementation `Nat.fib` in Lean 4. It asserts that for all natural numbers `n`, the `n + 2`-th term of the Fibonacci sequence is equal to the sum of the `n`-th and `(n + 1)`-th terms, validating the recurrence relation `Fₙ₊₂ = Fₙ + Fₙ₊₁` which characterizes the Fibonacci sequence.
More concisely: For all natural numbers n, the (n+2)-th Fibonacci number is equal to the sum of the n-th and (n+1)-th Fibonacci numbers.
|
Nat.fib_gcd
theorem Nat.fib_gcd : ∀ (m n : ℕ), (m.gcd n).fib = m.fib.gcd n.fib
This theorem states that the Fibonacci sequence, denoted as `fib n`, shows strong divisibility properties. Specifically, for any two natural numbers `m` and `n`, the greatest common divisor (GCD) of `m` and `n`, when input into the Fibonacci sequence, equals the GCD of the Fibonacci numbers at positions `m` and `n`. This is a property of the Fibonacci sequence proven in number theory. The proof can be found at the provided Proof Wiki link.
More concisely: The theorem asserts that for all natural numbers m and n, the greatest common divisor of m and n is equal to the greatest common divisor of `fib m` and `fib n`, where `fib` denotes the Fibonacci sequence.
|
Nat.fib_add
theorem Nat.fib_add : ∀ (m n : ℕ), (m + n + 1).fib = m.fib * n.fib + (m + 1).fib * (n + 1).fib
This theorem states that for any two natural numbers `m` and `n`, the Fibonacci number at the position of `m + n + 1` is equal to the sum of the product of the Fibonacci number at position `m` and the Fibonacci number at position `n`, and the product of the Fibonacci number at position `m + 1` and the Fibonacci number at position `n + 1`. This is a property of the Fibonacci sequence and provides a relationship between the Fibonacci numbers at different positions.
More concisely: The Fibonacci number at position `m + n + 1` equals the product of the Fibonacci number at position `m` with the Fibonacci number at position `n`, plus the product of the Fibonacci number at position `m + 1` with the Fibonacci number at position `n + 1`.
|
Nat.fib_coprime_fib_succ
theorem Nat.fib_coprime_fib_succ : ∀ (n : ℕ), n.fib.Coprime (n + 1).fib
This theorem states that any two consecutive Fibonacci numbers are coprime. In other words, for any natural number `n`, the Greatest Common Divisor (gcd) of the `n`th Fibonacci number and the `(n+1)`th Fibonacci number is 1. For more information and proof of this property, you can refer to https://proofwiki.org/wiki/Consecutive_Fibonacci_Numbers_are_Coprime.
More concisely: For all natural numbers `n`, the greatest common divisor of the `n`th and `(n+1)`th Fibonacci numbers is 1.
|