The Number of Terms in Greedy Fibonacci–Lucas Representations

Introduction

Let $F_k$ and $L_k$ be the Fibonacci and Lucas numbers, $F_0=0$, $F_1=1$, $L_0=2$, $L_1=1$, let $\varphi=(1+\sqrt{5})/2$ and $\psi=(1-\sqrt{5})/2$, and let

be the set of positive Fibonacci and Lucas numbers (A116470 in the OEIS [8]). For $n\ge1$ let $g(n)$ be the largest element of $S$ that is at most $n$. The greedy algorithm subtracts $g(n)$ from $n$ and repeats; the number of terms it produces is

which is A214973. Let $z(n)$ be the number of terms in the Zeckendorf representation of $n$ (A007895), and let

be A214981 and A179180. Representations by Lucas numbers go back to Carlitz, Scoville and Hoggatt [1]. Kimberling [3 Section 6] recorded the following conjecture, also stated in A214981.

Two more conjectures, from 2021, are recorded in A214973. Let A049651($j$) = $(F_{3j+1}-1)/2$.

The statement that A049651($j$) is the least $n$ with $a(n)=j$ appeared earlier, without proof, in a 2012 comment by Kimberling in A049651.

Here, if $n=F_{k_1}+\cdots+F_{k_s}$ is the Zeckendorf representation of $n$, with $k_1>\cdots>k_s\ge2$ and $k_i-k_{i+1}\ge2$, then $\mathrm{A003714}(n)=\sum_i 2^{k_i-2}$, whose binary word has no two adjacent ones. Preceded by a zero, such a word is a concatenation of the words 0 and 01 in exactly one way, and A048679($n$) is the number whose binary word is obtained by replacing each factor 01 by 1. Finally A035263($m$) is the parity of the 2-adic valuation $\nu_2(2m)$, and

For $x\ge1$ let $K(x)$ be the index $k\ge2$ with $F_k\le x<F_{k+1}$, and put $K(0)=0$. We prove the three conjectures.

The formula for $V(n)$ agrees with Lekkerkerker’s theorem on the average number of Zeckendorf summands [5, 4], since $c/5=1/(\varphi^2+1)$. Pihko [7] proved the analogues of that theorem for the minimal and maximal Lucas representations and the maximal

Image not extracted

Fibonacci representation. Theorem 1.4 shows that the greedy algorithm over $S$ uses on average $\frac{1}{5}\log_{\varphi} n$ terms.

The proof of Theorem 1.6 gives $a(n)$ in terms of the Zeckendorf representation of $n$: if its indices form maximal chains $k,k-2,k-4,\ldots$ of lengths $\ell_1,\ldots,\ell_t$, then $a(n)=\sum_i\lceil\ell_i/2\rceil$ (Corollary 5.1). The proofs are elementary, and every statement of Theorems 1.4–1.6 is also proved in the Lean 4 proof assistant (§ 6).

The greedy step

We use $L_m=F_{m-1}+F_{m+1}$ for $m \ge1$.

Image not extracted

Proof. The identities follow from $L_{k-1}=F_{k-2}+F_k$ and $F_{k+1}-F_k-F_{k-2}=F_{k-1}-F_{k-2}=F_{k-3}$, and $F_{k-2},F_{k-3}\ge1$ gives the inequalities. The only Fibonacci number in $[F_k,F_{k+1})$ is $F_k$. For the Lucas numbers, $L_0=2<F_k$, the sequence $(L_m)_{m\ge1}$ is increasing, $L_{k-2}=F_{k-3}+F_{k-1}\le F_{k-2}+F_{k-1}=F_k$, and $L_k=F_{k-1}+F_{k+1}>F_{k+1}$. So $L_{k-1}$ is the only Lucas number in $(F_k,F_{k+1})$.

For $1\le n\le2$ we have $a(n)=1$. The Zeckendorf representation satisfies $z(n)=1+z(n-F_k)$ for $F_k\le n<F_{k+1}$, $k\ge2$, since its leading term is the largest Fibonacci number at most $n$.

Proof. If $k_1\le3$ then $n\in\{1,2\}$, $s=1$ and $a(n)=1$. Let $k=k_1\ge4$, so $F_k\le n<F_{k+1}$, and let $r=n-F_k$. If $k_2=k-2$, then $n\ge F_k+F_{k-2}=L_{k-1}$ and $n-L_{k-1}=F_{k_3}+\cdots+F_{k_s}$. Otherwise $r=0$ or $r<F_{k_2+1}\le F_{k-2}$, so $n<L_{k-1}$. In both cases (2.1) gives the claim.

So the greedy algorithm over $S$ is the Zeckendorf algorithm in which a leading summand $F_k$ followed by $F_{k-2}$ is merged into $L_{k-1}$.

The summatory functions

Write $T(x)=\sum_{0\le i<x}a(i)$ and $Z(x)=\sum_{0\le i<x}z(i)$, so that $W(n)=T(n+1)$ and $V(n)=Z(n+1)$. If $f(i)=1+f(i-b)$ for $b\le i<d$, then $\sum_{i<x}f(i)=\sum_{i<b}f(i)+(x-b)+\sum_{i<x-b}f(i)$ for $b\le x\le d$. With Lemma 2.1 this gives, for $k\ge4$,

and, for $k \ge2$,

By Lemmas 3.1 and 3.3 and the induction hypothesis, this lies between $-4F_k-14r$ and $2F_k+24r$. Since $r\le F_k$ and $x=F_k+r$, both bounds are at most $19x$ in absolute value.

If $x>L_{k-1}$, let $r=x-L_{k-1}<F_{k-3}$. By (6) and (5) at $x=L_{k-1}$, and since $x=F_k+F_{k-2}+r$,

which lies between $-4F_k+F_{k-2}-14r$ and $2F_k+5F_{k-2}+24r$; both are at most $19x$ in absolute value.

Proof. By induction on $x$; the case $x=0$ is trivial. Let $x\ge1$, $k=K(x)\ge2$ and $r=x-F_k<F_{k-1}$, so $K(r)\le k$ and $r\le F_k$. By (7),

Since $0<c\le2$, Lemmas 3.2 and 3.3 and the induction hypothesis place this between $-8F_k-8r$ and $4F_k+18r$, and both are at most $13x=13F_k+13r$ in absolute value.

Proof of Theorem 1.4. The bounds (1.1) are Propositions 3.4 and 3.5. Let $x=n+1$ and $K=K(x)$. Then $W(n)=T(x)$ and $V(n)=Z(x)$, and

has absolute value at most $13x+2\cdot19x=51x$, while $5W(n)\ge(K-19)x$. This gives (1.3), and $K(n+1)\to\infty$ gives the limit. Finally $6/5<(5-\sqrt{5})/2<7/5$ because $121<125<169$.

For (1.2), write $\lambda(t)=\log_\varphi t$. Since $F_{k+1}\le\varphi^k$ and $\varphi^{k-2}\le F_k$ for $k\ge2$, and $F_K\le x<F_{K+1}$, we have $\lambda(x)<K\le\lambda(x)+2$. Also $K\le x+1$, because $F_k\ge k-1$ for every $k\ge1$. Next,

and $n\log(1+1/n)\le1<3\log\varphi$, because $\varphi^3=2\varphi+1>e$. Hence $0\le x\lambda(x)-n\lambda(n)\le K+3\le n+5$. In the identity

the three terms lie in $[-19x,19x]$, $[0,2x]$ and $[0,n+5]$, so $-19(n+1)\le5W(n)-n\lambda(n)\le21(n+1)+n+5\le48n$ for $n\ge1$. In the same way, since $0<c\le2$,

lies between $-13(n+1)$ and $13(n+1)+4(n+1)+2(n+5)\le46n$. Dividing by 5 gives (1.2).

The records

Let $R_j = F_2 + F_5 + \cdots+ F_{3j-1} = \sum_{i<j} F_{3i+2}$. Since $F_{3j+1} + 2F_{3j+2} = F_{3j+3} + F_{3j+2} = F_{3j+4}$, induction gives $2R_j + 1 = F_{3j+1}$, so $R_j = \mathrm{A049651}(j)$. Moreover $R_j < F_{3j}$ for $j \ge1$, since $2R_j < F_{3j+1} \le2F_{3j}$.

Proof of Theorem 1.5. First, $a(R_j) = j$. This holds for $j = 0, 1$. For $j \ge2$ let $k = 3j - 1 \ge5$. Then $R_j = F_k + R_{j-1}$ and $R_{j-1} < F_{k-2}$, so $F_k \le R_j < L_{k-1}$, and (2.1) gives $a(R_j) = 1 + a(R_{j-1}) = j$.

Second, $a(m) \ge j$ implies $m \ge R_j$. We use induction on $m$. The cases $j \le1$ and $m \le2$ are clear, so let $j = t + 2$ with $t \ge0$, and let $m \ge3$ and $k = K(m) \ge4$. By (2.1) there is $r$ with $a(r) = a(m) - 1 \ge t + 1$, where either $r = m - F_k < F_{k-2}$ or $r = m - L_{k-1} < F_{k-3}$. By induction $r \ge R_{t+1} \ge F_{3t+2}$, so $F_{3t+2} < F_{k-2}$, hence $3t + 2 < k - 2$ and $F_{3t+5} \le F_k$. In both cases $m \ge F_k + r \ge F_{3t+5} + R_{t+1} = R_{t+2}$.

So $a(m) < j$ for $m < R_j$, and $a(R_j) = j$. Thus $R_j$ is the first occurrence of $j$, and since $R_1 < R_2 < \cdots$, the records of A214973 occur exactly at $R_1, R_2, \ldots.

Kurkov's formula

Let $n = F_{k_1} + \cdots+ F_{k_s}$ be the Zeckendorf representation of $n \ge1$. A chain is a maximal run $k_i, k_{i+1}, \ldots, k_{i+\ell-1}$ of consecutive indices with $k_p - k_{p+1} = 2$ for $i \le p < i + \ell- 1$; the indices split into chains of lengths $\ell_1, \ldots, \ell_t$, and consecutive chains are separated by gaps $k_p - k_{p+1} \ge3$.

Proof. Apply Lemma 2.2 repeatedly. Along a chain it merges the first and second terms, the third and fourth, and so on, giving $\lceil\ell/2 \rceil$ terms; it never merges the last term of a chain with the first term of the next, since they differ by at least 3.

Proof. The binary word of A003714$(n)$, preceded by a zero, consists of the factors 01 occupying positions $k_i - 1, k_i - 2$ ($1 \le i \le s$; position 0 is the units digit), separated by zeros. These factors are disjoint because $k_{i+1} - 1 \le k_i - 3$. Replacing each 01 by 1 moves the digit at position $k_i - 2$ down by one place for each of the $s-i$ factors below it, so it lands at position $h_i$. Finally $h_i - h_{i+1} = k_i - k_{i+1} - 1 \ge1$ and $h_s = k_s - 2 \ge 0.

Proof. Since $\nu_2(2m) = 1 + \nu_2(m)$, we have $1 - \mathrm{A035263}(1+u) = \nu_2(u+1) \bmod2$, and $\nu_2(\lfloor y/2^k \rfloor+ 1)$ is the number of consecutive ones of $y$ starting at position $k$ and going up. This number is 0 if the digit at position $k$ is 0, and, along a block of $\ell$ ones, it takes the values $\ell, \ell- 1, \ldots, 1$, of which $\lceil\ell/2 \rceil$ are odd. The sum defining A329320$(y)$ runs over the positions $0, \ldots, \lfloor\log_2 y \rfloor$, which contain every block.

Proof of Theorem 1.6. For $n = 0$ both sides are 0. For $n \ge1$, Lemma 5.2 shows that the blocks of ones of A048679$(n)$ correspond to the chains of the Zeckendorf representation of $n$, with the same lengths. Lemma 5.3 and Corollary 5.1 give A329320(A048679($n$)) $= \sum_i \lceil\ell_i/2 \rceil= a(n)$. Figure 3 follows the argument for $n = 595$.

Image not extracted

Formal verification

Theorems 1.4, 1.5 and 1.6 are formalized in Lean 4 [2] with Mathlib [6], version 4.34.1, and the formal proofs are checked by the Lean kernel. The formalization defines the sequences directly from their entries in the OEIS: $a$ by the greedy recursion over the positive Fibonacci and Lucas numbers, $z$ as the length of the Zeckendorf representation, $W$ and $V$ as sums over $1 \le i \le n$, A048679 by the rewriting of binary digits described in § 1, and A329320 by the displayed sum. It proves the bounds (1), the explicit formulas (2), the limit $V(n)/W(n) \to(5-\sqrt{5})/2$ together with $6/5 < (5-\sqrt{5})/2 < 7/5$, Theorem 1.5 for every $j$, and Theorem 1.6 for every $n \ge0$. In the formal proof of Theorem 1.6 the induction runs on the Zeckendorf representation through the recursion A329320($2^{Q+1}+u$) = A329320($2^{Q+1}+2^Q+u$) = $1+$A329320($u$) for $u < 2^Q$, in place of Lemma 5.3. The proofs depend only on the axioms of Lean’s logic, namely propositional extensionality, choice and the soundness of quotients; they have no unproved step and add no axiom.

Independent computations in exact integer arithmetic, from the definitions of the sequences, confirm (1.1) for $x \le10^8 + 1$, Lemma 3.1 and the formula of Lemma 3.2 for $F_k \le10^8 + 1$, Theorems 1.5 and 1.6 and Lemma 2.2 for $n \le10^8$, and Lemmas 2.1, 3.1 and 3.2 for $k \le400$; they agree with the terms of the sequences recorded in the OEIS. The ratio $V(n)/W(n)$ equals 1.3421 at $n = 10^6$ and 1.3588 at $n = 10^8$.

Acknowledgements

The authors used the generative AI tool Claude (Anthropic), through Claude Code, to assist with the proofs, the Lean formalization, the computations and the preparation of this article. The authors reviewed and edited the content and take full responsibility for it.

Disclosure statement

Competing interests: none.

Funding

None.

Data availability

Deep Bhattacharjee computed the Lean formalization and the Julia, C, C++, shell and Python computations with the help of AI assistance (Claude, Anthropic). The Lean formalization of the proofs in this paper is archived at Zenodo, doi:10.5281/zenodo.23385265. The paper is available at https://github.com/creelie/musical-rotary-phone/blob/main/preprintKimberlingConjecture/KimberlingConjecture.pdf.

References