Proving Properties of $φ$-Representations with the Walnut Theorem-Prover

1. Problem Statement

The paper addresses the complexity of analyzing $\phi$-representations (base-$\phi$ expansions), where $\phi = (1+\sqrt{5})/2$ is the golden ratio. While George Bergman (1957) established that non-negative real numbers can be expanded in base $\phi$ using digits $\{0, 1\}$, and Frougny and Sakarovitch (2006) proved that the canonical $\phi$-representation of an integer can be computed by a finite automaton, the original construction of this automaton was implicit and difficult to utilize for deriving further properties.

The specific challenges addressed are:

• Lack of Explicit Automata: The Frougny-Sakarovitch automaton was not explicitly constructed in a way that allowed for easy manipulation or extension.
• Complexity of Proofs: Existing results regarding $\phi$-representations (e.g., by Dekking and Van Loon) often rely on complex, tedious mathematical inductions to count representations, determine digit sums, or characterize specific patterns (like palindromes).
• Need for Automation: There is a need for a uniform, "automatic" method to prove theorems, enumerate expansions, and discover new properties without manual case-by-case analysis.

2. Methodology

The author employs Walnut, a free theorem-prover software developed by Hamoon Mousavi, which utilizes decision procedures for extensions of Presburger arithmetic to reason about automatic sequences.

Core Workflow:

1. Representation Systems: The paper utilizes two integer representation systems:
   • Zeckendorf System: Canonical representation of non-negative integers using Fibonacci numbers ($F_n$) without consecutive 1s.
   • NegaFibonacci System: Representation of integers (positive, negative, zero) using negative-indexed Fibonacci numbers ($F_{-n}$).
2. Automaton Construction: Instead of manually designing a complex state machine, the author constructs the Frougny-Sakarovitch automaton by composing smaller, modular automata in Walnut. These modules handle:
   • Normalization (converting arbitrary binary strings to canonical Zeckendorf/NegaFibonacci forms).
   • Shifting (left/right shifts of representations).
   • Bit extraction (last, second-to-last bits).
   • Conversion between Zeckendorf and NegaFibonacci systems.
3. Logical Formulation: The relationship $n = [x.y]_\phi$ is expressed in first-order logic. Using the identity $\phi^k = F_k\phi + F_{k-1}$, the paper derives that the integer $n$ and the $\phi$-expansion $x.y$ satisfy specific linear equations involving shifted representations.
4. Automated Verification: Walnut computes the intersection of these logical conditions to produce a finite automaton (specifically, one with 116 states, reducible to 39 for canonical forms).
5. Deriving Results: Once the automaton is built, it is used to:
   • Compute linear representations (matrix morphisms) for counting functions.
   • Verify properties by checking if specific logical formulas evaluate to TRUE.
   • Enumerate specific types of expansions (e.g., Knott expansions, palindromes) by intersecting the main automaton with condition-specific automata.

3. Key Contributions

• Explicit Construction of Frougny-Sakarovitch Automaton: The paper provides the first explicit, modular construction of the automaton that accepts the folded $\phi$-representation of integers, reducing it from a theoretical existence proof to a computational tool.
• Unified Proof Framework: Demonstrates that a wide variety of results concerning $\phi$-representations can be proven uniformly using automata theory, eliminating the need for ad-hoc induction proofs.
• Automatic Enumeration: Shows how to automatically count the number of specific types of expansions (e.g., Knott expansions) and compute their asymptotic behavior.
• New Discoveries: Identifies and proves new theorems regarding digit sums, lengths of representations, vertical runs of 1s, and antipalindromic expansions.

4. Key Results

The paper derives numerous results, many of which are new or provide simpler proofs for existing conjectures:

• Canonical Representations of Fibonacci and Lucas Numbers:
  • Provides explicit formulas for the $\phi$-expansion of $F_{4i}, F_{4i+1}, F_{4i+2}, F_{4i+3}$ and $L_{2i}, L_{2i+1}$.
  • Proves that the $\phi$-representation of $F_n$ follows a periodic pattern modulo 4.
• Digit Sums:
  • Theorem 3.1: Proves a 2012 conjecture by Dale Gerdemann: The sum of digits in the Zeckendorf representation of $n$ is always less than or equal to the sum of digits in the canonical base-$\phi$ representation.
  • Computes linear representations for the sum of digits in the left and right parts of the expansion.
• Length of Representations:
  • Characterizes the length of the left part of $(n)_\phi$. Proves that the difference $\ell(n) - \ell(n-1)$ is 1 if and only if $n$ is a Lucas number or related to them.
• Individual Bits and Vertical Runs:
  • Connects specific bits of the $\phi$-expansion to Sturmian sequences and Lucas representations.
  • Theorem 5.4: Determines the exact length of "vertical runs" of 1s in the $\phi$-expansion, providing a closed form involving Lucas numbers, contradicting a previous claim by Dekking and Van Loon that "there is no such regularity."
• Palindromic and Antipalindromic Expansions:
  • Constructs automata to recognize integers with palindromic and antipalindromic $\phi$-representations (both canonical and non-canonical).
• Knott Expansions:
  • Recovers and simplifies results by Dekking and Van Loon regarding "Knott expansions" (those not ending in 011).
  • Derives a linear representation to compute the total number of Knott expansions, $Tot_\kappa(n)$, in $O(\log n)$ time.
  • Proves asymptotic results for the average number of Knott expansions in intervals $[F_i, F_{i+1})$.
• Dekking-Van Loon (DVL) Expansions:
  • Adapts the automaton to handle "DVL-expansions" (allowing 11 only in specific positions), recovering their results on vertical runs automatically.
• Algebraic Integers:
  • Extends the method to compute $\phi$-representations for algebraic integers of the form $m\phi + n$ where $m, n \in \mathbb{Z}$.

5. Significance

• Computational Number Theory: The paper bridges the gap between theoretical automata results and practical computation. It demonstrates that complex number-theoretic properties of base-$\phi$ expansions can be reduced to finite automata operations.
• Elimination of Induction: By using the Walnut theorem-prover, the author replaces long, error-prone inductive proofs with algorithmic verification. This suggests a paradigm shift in how such problems might be approached in the future.
• Generalizability: While focused on $\phi$, the author notes that these techniques apply to any $\beta$-expansion where $\beta$ is a quadratic Pisot number, provided the necessary arithmetic automata can be constructed.
• OEIS Contributions: The paper identifies and defines numerous new integer sequences (e.g., A362970, A362716, A362780) related to $\phi$-representations, enriching the On-Line Encyclopedia of Integer Sequences.

In summary, this paper serves as a powerful demonstration of how automated theorem proving can be used to revisit classic problems in number theory, yielding both simplified proofs of known results and the discovery of new structural properties of $\phi$-representations.