Some Fibonacci-Related Sequences

TL;DR

This work analyzes the Fibonacci-recursive sequence $a(n)$ (OEIS $A105774$) through Zeckendorf (Fibonacci) representations, finite automata, and the Walnut theorem-prover to establish a rich set of properties. By building and verifying both standard and synchronized automata, the authors prove inequalities, parity, fixed points, and transform relations (including distinctness and sorting), and they derive Carlitz-style recurrences and compositions with Fibonacci mappings. A key contribution is demonstrating decidability and constructibility of automata-based proofs for complex number-theoretic sequences, along with new results on synchronized sequences and multiple generalizations (including Lucas-number variants and two-parameter families). The methodology showcases how automated reasoning over Fibonacci-automatic structures yields rigorous, verifiable insights into intricate fractal sequences and their interrelations, providing a template for exploring similar recurrences. The combination of automata-theoretic techniques, linear representations, and first-order reasoning via Walnut enables precise, checkable results that would be difficult to obtain by manual derivation alone.

Abstract

We discuss an interesting sequence defined recursively; namely, sequence A105774 from the On-Line Encyclopedia of Integer Sequences, and study some of its properties. Our main tools are Fibonacci representation, finite automata, and the Walnut theorem-prover. We also prove two new results about synchronized sequences.

Figures (13)

• Figure 1: Graph of $a(n)$.
• Figure 2: Fibonacci automaton for the set of even numbers.
• Figure 3: Fibonacci DFAO computing $n \bmod 3$.
• Figure 4: Synchronized Fibonacci automaton computing $\lfloor n/2 \rfloor$.
• Figure 5: Synchronized Fibonacci automaton for $a(n)$.

Theorems & Definitions (49)

• Proposition 1
• proof
• Proposition 2
• proof
• Proposition 3
• proof
• Proposition 4
• proof
• Proposition 5
• proof