Grace/Cumulus/NumberTheory/FibonacciGCD.g17

Open in Workbench Download source

Imports

GCDMore · Combinatorics.Fibonacci

Declarations

Source

1-- Consecutive Fibonacci numbers are coprime, and so are Fibonacci numbers2-- two apart3-- Part of Cumulus, the Grace17 mathematics library.4-- Copyright (c) 2026 Grant Passmore.5-- Released under the Apache License 2.0. See LICENSE in the repository root.6-- Authors: Grant Passmore78module Grace.Cumulus.NumberTheory.FibonacciGCD9import GCDMore10import Combinatorics.Fibonacci1112theorem fibonacci.coprime_consecutive (n : Nat)13  shows gcd(fibonacci(n), fibonacci(n + 1)) = 114proof15  induction n16  | zero =>17    have zero := fibonacci.zero18    have index : fibonacci(0 + 1) = 119      have sum : 0 + 1 = 1 by ring20      rw sum21      exact fibonacci.one22    rw [zero, index]23    exact gcd.zero_left at 124  | k + 1 using ih =>25    have two : k + 1 + 1 = k + 2 by ring26    have step := fibonacci.succ_succ at k27    rw [two, step]28    have shifted := gcd.add_right_swap at fibonacci(k + 1), fibonacci(k)29    rw shifted30    have commute := gcd.commutative at fibonacci(k + 1), fibonacci(k)31    rw commute32    exact ih3334theorem fibonacci.coprime_consecutive_left (n : Nat)35  shows gcd(fibonacci(n + 1), fibonacci(n)) = 136proof37  have commute := gcd.commutative at fibonacci(n + 1), fibonacci(n)38  rw commute39  exact fibonacci.coprime_consecutive at n4041theorem fibonacci.coprime_skip (n : Nat)42  shows gcd(fibonacci(n), fibonacci(n + 2)) = 143proof44  have step := fibonacci.succ_succ at n45  rw step46  have shifted := gcd.add_right at fibonacci(n), fibonacci(n + 1)47  rw shifted48  exact fibonacci.coprime_consecutive at n4950theorem fibonacci.divides_consecutive_one (d n : Nat)51  requires left : d ∣ fibonacci(n)52  requires right : d ∣ fibonacci(n + 1)53  shows d = 154proof55  have coprimeFib := fibonacci.coprime_consecutive at n56  exact coprime.divisor_one at fibonacci(n), fibonacci(n + 1), d57    with coprimeFib, left, right58