A General Approach to Proving Properties of Fibonacci Representations via Automata Theory

TL;DR

This paper introduces a automata-theoretic method to mechanically verify the correctness of various Fibonacci-based numeration systems, replacing complex proofs with automaton construction and computation.

Contribution

It presents a novel, automated approach to prove properties of Fibonacci representations using automata theory, applicable to multiple existing and new systems.

Findings

Successfully verified Brown's lazy representation

Validated Alpert's far-difference representation

Proved three new Fibonacci-based systems

Abstract

We provide a method, based on automata theory, to mechanically prove the correctness of many numeration systems based on Fibonacci numbers. With it, long case-based and induction-based proofs of correctness can be replaced by simply constructing a regular expression (or finite automaton) specifying the rules for valid representations, followed by a short computation. Examples of the systems that can be handled using our technique include Brown's lazy representation (1965), the far-difference representation developed by Alpert (2009), and three representations proposed by Hajnal (2023). We also provide three additional systems and prove their validity.