A remark about the positivity problem problem of fourth order linear recurrence sequences (Q2875913)

From the text: Consider a fourth order linear recurrence with integer coefficients whose characteristic polynomial has two distinct real and a complex conjugate pair of roots. A new proof showing that its Positivity Problem is decidable is given for the case where there is exactly one real root having the same absolute value as the two complex conjugate roots.NEWLINENEWLINEThe Positivity Problem for sequences satisfying a second order linear recurrence relation was shown to be decidable by \textit{V. Halava, T. Harju} and \textit{M. Hirvensalo} [Discrete Appl. Math. 154, No. 3, 447--451 (2006; Zbl 1158.11305)]. The Positivity Problem for sequences satisfying third and fourth order linear recurrences was shown to be decidable in [the authors, Discrete Appl. Math. 157, No. 15, 3239--3248 (2009; Zbl 1209.11020)], [the authors and N. Punnim, Colloq. Math. 128, No. 1, 133--142 (2012; Zbl 1284.11023), East-West J. Math. 14, No. 2, 185--200 (2012; Zbl 1307.11021)], respectively, see also [\textit{J. Ouaknine} and \textit{J. Worrell}, (*) Reachability problems -- RP 2012, Lect. Notes Comput. Sci. 7550, 21--28 (2012; Zbl 1298.11015), (**) Positivity Problem for low-order linear recurrence sequences. In: Proceedings of the 25th annual ACM-SIAM symposium on discrete algorithms, SODA 2014, Philadelphia, PA: SIAM); New York, NY: ACM, 366--379 (2014), see Zbl 1287.68005]. As pointed out by Professor J. Ouaknine in a private communication, there is a gap in the proof of Claim 2 on page 141 of [(*)]. Our objective here is to repair this gap and a few loose arguments by giving a new proof, supplementing the works in [(*), (**)],