On the lower bondary for time complexity of a decidability problem of a theory of integers with a successor function and the least fixed point operator

We show that any decision procedure for the theory of integers with a successor function and a least fixed point operator for a formula with $n$ nested operators has at least hyperexponential time complexity.
There are two stages in the proof. First of all we show that an exponential shift can be represented using short formulas. We construct least fixed point operator which enumerates binary codes of initial segment of natural numbers.
Then we show that cellular automation with hyperexponential time complexity can be modeled using least fixed point operator. We also note that the final formula length is linear dependent on the input data length.