Hofstadter’s function is recursively defined via and then . Following Hofstadter, a family of similar functions is obtained by varying the number of nested recursive calls in this equation. We study here some Fibonacci-like sequences that are deeply connected with these functions . In particular, the Zeckendorf theorem can be adapted to provide digital expansions via sums of terms of these sequences. On these digital expansions, the functions are acting as right shifts of the digits. These Fibonacci-like sequences can be expressed in terms of zeros of the polynomial . Considering now the discrepancy of each function , i.e., the maximal distance between and its linear equivalent, we retrieve the fact that this discrepancy is finite exactly when . Thanks to that, we solve two twenty-year-old OEIS conjectures stating how close the functions and are from the integer parts of their linear equivalents. Moreover we establish that can coincide exactly with such an integer part only when , while is almost additive exactly when . Finally, a nice fractal shape a la Rauzy has been encountered when investigating the discrepancy of . Almost all this article has been formalized and verified in the Coq/Rocq proof assistant.

生成讲解博客的中文版本

生成AI智能校验的中文版本