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.

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

$$ \beginproof \pexp{\text{$\fapp{\fib}{(n{\times}k)}$ is a multiple of $\fapp{\fib}{k}$}} \hint{=}{definition} \pexp{\fapp{\fib}{k} \setminus \fapp{\fib}{(n{\times}k)}} \hint{=}{rewrite in terms of $\nabla$} \pexp{\fapp{\fib}{k} ~\nabla~ \fapp{\fib}{(n{\times}k)} ~=~ \fapp{\fib}{k}} \hint{=}{$\fib$ distributes over $\nabla$} \pexp{\fapp{\fib}{(k{\nabla}(n{\times}k))} = \fapp{\fib}{k}} \hint{=}{$k{\nabla}(n{\times}k) = k$} \pexp{\fapp{\fib}{k} = \fapp{\fib}{k}} \hint{=}{reflexivity} \pexp{true~~.} \endproof $$

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 $\fapp{\fib}{k}$ nor $\fapp{\fib}{(n{\times}k)}$, but applying the distributivity property prioritised the $\nabla$ operator — and we know how to simplify $k \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!