Documentation

FUST.Math.FibonacciArithmetic

Lucas Numbers via Binet Formula #

source
noncomputable def FUST.FibonacciArithmetic.lucasConst (n : ℕ) :
ℝ

Lucas number L_n = φ^n + ψ^n (Binet form)

Equations
Instances For
    source
    theorem FUST.FibonacciArithmetic.lucasConst_zero :
    lucasConst 0 = 2
    source
    theorem FUST.FibonacciArithmetic.lucasConst_one :
    lucasConst 1 = 1
    source
    theorem FUST.FibonacciArithmetic.lucasConst_two :
    lucasConst 2 = 3
    source
    theorem FUST.FibonacciArithmetic.lucasConst_three :
    lucasConst 3 = 4
    source
    theorem FUST.FibonacciArithmetic.lucasConst_recurrence (n : ℕ) :
    lucasConst (n + 2) = lucasConst (n + 1) + lucasConst n

    Lucas recurrence: L_{n+2} = L_{n+1} + L_n

    source
    theorem FUST.FibonacciArithmetic.phi_psi_pow_prod (n : ℕ) :
    φ ^ n * ψ ^ n = (-1) ^ n

    Product identity: φ^n · ψ^n = (-1)^n

    Diff6Coeff Integrality #

    Diff6Coeff(n) / √5 = F_{3n} - 3F_{2n} + F_n ∈ ℤ

    source
    def FUST.FibonacciArithmetic.fibCombination (n : ℕ) :
    ℤ

    The Fibonacci combination F_{3n} - 3F_{2n} + F_n is an integer

    Equations
    Instances For
      source
      theorem FUST.FibonacciArithmetic.Diff6Coeff_eq_sqrt5_mul_int (n : ℕ) :
      SpectralCoefficients.Diff6Coeff n = √5 * ↑(fibCombination n)

      Diff6Coeff(n) = √5 · fibCombination(n)

      source
      theorem FUST.FibonacciArithmetic.fibCombination_zero :
      fibCombination 0 = 0
      source
      theorem FUST.FibonacciArithmetic.fibCombination_one :
      fibCombination 1 = 0
      source
      theorem FUST.FibonacciArithmetic.fibCombination_two :
      fibCombination 2 = 0
      source
      theorem FUST.FibonacciArithmetic.fibCombination_three :
      fibCombination 3 = 12
      source
      theorem FUST.FibonacciArithmetic.fibCombination_four :
      fibCombination 4 = 84
      source
      theorem FUST.FibonacciArithmetic.fibCombination_five :
      fibCombination 5 = 450
      source
      theorem FUST.FibonacciArithmetic.fibCombination_eq_zero_iff (n : ℕ) :
      fibCombination n = 0 ↔ n ≤ 2

      fibCombination vanishes iff n ≤ 2

      Fibonacci Strong Divisibility #

      F_m | F_n when m | n. This is Nat.fib_dvd from Mathlib.

      source
      theorem FUST.FibonacciArithmetic.fib_dvd_of_dvd (m n : ℕ) (h : m ∣ n) :
      Nat.fib m ∣ Nat.fib n

      Fibonacci strong divisibility (from Mathlib)

      source
      theorem FUST.FibonacciArithmetic.fib_coprime_succ (n : ℕ) :
      (Nat.fib n).Coprime (Nat.fib (n + 1))

      Consecutive Fibonacci numbers are coprime (from Mathlib)

      source
      theorem FUST.FibonacciArithmetic.fib_gcd (m n : ℕ) :
      Nat.fib (m.gcd n) = (Nat.fib m).gcd (Nat.fib n)

      GCD of Fibonacci = Fibonacci of GCD (from Mathlib)

      source
      theorem FUST.FibonacciArithmetic.fib_even_of_three_dvd (n : ℕ) (h : 3 ∣ n) :
      2 ∣ Nat.fib n

      3 | n → F_3 = 2 divides F_n

      source
      theorem FUST.FibonacciArithmetic.fib_three_dvd_of_four_dvd (n : ℕ) (h : 4 ∣ n) :
      3 ∣ Nat.fib n

      4 | n → F_4 = 3 divides F_n

      source
      theorem FUST.FibonacciArithmetic.fib_five_dvd_of_five_dvd (n : ℕ) (h : 5 ∣ n) :
      5 ∣ Nat.fib n

      5 | n → F_5 = 5 divides F_n

      Diff6Coeff via Lucas and Fibonacci #

      Express Diff6Coeff using both Fibonacci (φ^n-ψ^n)/√5 and Lucas (φ^n+ψ^n).

      source
      theorem FUST.FibonacciArithmetic.Diff6Coeff_lucas_fibonacci (n : ℕ) :
      SpectralCoefficients.Diff6Coeff n = (φ ^ n - ψ ^ n) * (lucasConst (2 * n) - 3 * lucasConst n + (-1) ^ n + 1)

      Diff6Coeff via triple factorization with Lucas: C_n = (φ^n-ψ^n) · (L_{2n} - 3·L_n + (-1)^n + 1)