Multiples in the Fibonacci series : Joao Ferreira

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 $\setms{0.1em}$\mathit{fib\/}{.}n$$ to denote the Fibonacci number $n$ , $m {\raisebox{0.5mm}{\ensuremath{\bigtriangledown}}} n$ to denote the greatest common divisor of $m$ and $n$ , and $\setminus$ to denote the division relation, a possible proof is:

$\begin{mpdisplay}{0.1em}{6.5mm}{2mm}{3}$\mathit{fib\/}{.}(n{\times}k)$ is a multiple of $\mathit{fib\/}{.}k$\push\-\\$=$ \> \>$\{$ \>\+\+\+definition\-\-$~~~ \}$\pop\\$\mathit{fib\/}{.}k\ms{1}{\setminus}\ms{1}\mathit{fib\/}{.}(n{\times}k)$\push\-\\$=$ \> \>$\{$ \>\+\+\+$\mathit{fib\/}{.}k$ divides $\mathit{fib\/}{.}(n{\times}k)$\-\-$~~~ \}$\pop\\$\mathit{fib\/}{.}k\ms{0}{\raisebox{0.5mm}{\ensuremath{\bigtriangledown}}} \ms{1}\mathit{fib\/}{.}(n{\times}k)\ms{1}{=}\ms{1}\mathit{fib\/}{.}k$\push\-\\$=$ \> \>$\{$ \>\+\+\+$\mathit{fib\/}$ distributes over $\raisebox{0.8mm}{\ensuremath{\bigtriangledown}}$\-\-$~~~ \}$\pop\\$\mathit{fib\/}{.}(k\ms{0}\raisebox{0.8mm}{\ensuremath{\bigtriangledown}} \ms{1}(n{\times}k))\ms{1}{=}\ms{1}\mathit{fib\/}{.}k$\push\-\\$=$ \> \>$\{$ \>\+\+\+$k\ms{0}\raisebox{0.8mm}{\ensuremath{\bigtriangledown}} \ms{1}(n{\times}k)\ms{1}{=}\ms{1}k$\-\-$~~~ \}$\pop\\$\mathit{fib\/}{.}k\ms{1}{=}\ms{1}\mathit{fib\/}{.}k$\push\-\\$=$ \> \>$\{$ \>\+\+\+reflexivity\-\-$~~~ \}$\pop\\$\mathit{true\/}~~.$\end{mpdisplay}$

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 $\bigtriangledown$ operator — and we know how to simplify $k\ms{0}\raisebox{0.8mm}{\ensuremath{\bigtriangledown}} \ms{1}(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 leave a comment!

4 Comments

Hugo wrote:

Can you help me understand your second equality?

Sunday, May 11, 2008 at 6:52 pm | Permalink
jff wrote:

Hi Hugo,

If fib.k divides fib.(n*k), then the greatest common divisor of fib.k and fib.(n*k) is fib.k (it divides both, and is the largest divisor of itself).

Also, if fib.k is the greatest common divisor of itself and fib.(n*k), then it clearly divides fib.(n*k).

Do you agree?

Joao

Sunday, May 11, 2008 at 7:08 pm | Permalink
Hugo wrote:

That’s right, I disregarded fib.(n*k) represents a number, thanks for the help. Congratulations! Your work it’s really interesting.

Sunday, May 11, 2008 at 7:59 pm | Permalink
jff wrote:

Yes, it’s just the (n*k)th Fibonacci number Thanks for your comments!

Sunday, May 11, 2008 at 8:26 pm | Permalink

João Ferreira