I'm not sure whether it would work in your case, but in order to show succinctness results in modal/temporal logic (e.g. the fact the two-variable logic over words in exponentially more succinct than unary temporal logic) one can employ formula size games or Adler-Immerman games.
Probably the most recent paper to read is by Lauri Hella and Miikka Vilander. ...
Your question is formally the same as this one: how many symbols $X$ are needed to write the polynomial $XX + XXXX + XXXXXX = XX(1 + XX(1 + XX))$?
Well, you obtained $6$ as an upper bound. It is also a lower bound because any expression involving less than $6$ symbols $X$ would define a polynomial of degree $< 6$.
For the general case, I would not be ...
Sorry to provide the same answer as for this question,
but this was proved in [1, Theorem 3.1].
 J. Cohen, D. Perrin and J.-É. Pin, On the expressive power of temporal logic for finite words, J. Comput. System Sci. 46 (1993), 271-294.
As mentioned in the comments, the translation is shown in:
Volker Diekert and Paul Gastin. "First-order definable languages." (2008)
And it goes via a characterization of $LTL$ as $FO[<]$.
An algebraic characterisation of the restricted temporal logic (fragment using only next and eventually, but not until) is given in .
The expressive power of this fragment is the set of regular languages whose syntactic monoid are locally $\cal L$-trivial.
I am not sure of the result you are looking for, but this article probably contains enough material ...