Multiples in the Fibonacci Series

I found the following problem on K. Rustan M. Leino’s puzzles page:

[Carroll Morgan told me this puzzle.]

Prove that for any positive K, every Kth number in the Fibonacci sequence is a multiple of the Kth number in the Fibonacci sequence.

More formally, for any natural number n, let F(n) denote Fibonacci number n. That is, F(0) = 0, F(1) = 1, and F(n+2) = F(n+1) + F(n). Prove that for any positive K and natural n, F(n*K) is a multiple of F(K).

This problem caught my attention, because it looks like a good example for using a result that I have derived last year. My result gives a reasonable sufficient condition for showing that a function distributes over the greatest common divisor and shows that the Fibonacci function satisfies the condition.

$$In fact, using the property that the Fibonacci function distributes over the greatest common divisor, we can solve this problem very easily. Using $fib.n$ to denote the Fibonacci number $n$, $m\mathrm{\nabla }n$ to denote the greatest common divisor of m and n, and $\setminus$ to denote the division relation, a possible proof is:

$$\begin{array}{cl}& fib.(n\times k)\text{ is a multiple of }fib.k\\ =& \{\text{definition}\}\\ & fib.k\setminus fib.(n\times k)\\ =& \{\text{rewrite in terms of }\mathrm{\nabla }\}\\ & fib.k\mathrm{\nabla }fib.(n\times k)=fib.k\\ =& \{fib\text{ distributes over }\mathrm{\nabla }\}\\ & fib.(k\mathrm{\nabla }(n\times k))=fib.k\\ =& \{k\mathrm{\nabla }(n\times k)=k\}\\ & fib.k=fib.k\\ =& \{\text{reflexivity}\}\\ & true.\end{array}$$

The crucial step is clearly the one where we apply the distributivity property. Distributivity properties are very important, because they allow us to rewrite expressions in a way that prioritizes the function that has the most relevant properties. In the example above we could not simplify $fib.k$ nor $fib.(n\times k)$, but applying the distributivity property prioritised the $\mathrm{\nabla }$ operator — and we know how to simplify $k\mathrm{\nabla }(n\times k)$. Furthermore, in practice, distributivity properties reduce to simple syntactic manipulations, thus reducing the introduction of error and simplifying the verification of our arguments.

(Now that I think about it, perhaps it would be a good idea to write a note on distributivity properties, summarizing their importance and their relation with symbol dynamics.)

If you have any corrections, questions, or alternative proofs, please get in touch!