Fibonacci Numbers and Model-Complete Axiomatization of Presburger Arithmetic Expanded with a Beatty Sequence

We introduce a recursive theory that completely axiomatizes the structure $⟨\mathbb{Z},<,+,f,0⟩$ where $f$ is the function that maps each $x$ to the integer part of $\phi x$, with $\phi$ the golden ratio. We prove that our axiomatization is model-complete in a language expanded with a function which we which we refer as the Fibonacci floor function.