An order-six instance of the Skolem Problem has no zeros

In a recent survey, Bacik, Karimov, Luca, Nieuwveld, Ouaknine, Purser and Worrell consider the order-six integer linear recurrence sequence u_n = 2(−4+7i)^n + 2(−4−7i)^n + 4(8+i)^n + 4(8−i)^n + n, which has a zero modulo every integer m ≥ 2, and state that whether it has a zero is open. We show by an elementary 23-adic argument that u_n ≠ 0 for every n ≥ 0. In fact, 24 divides u_n only when n ≡ 12 (mod 24), and on that residue class the 23-adic valuation of u_n equals that of n. We explain why the prime 23 works. We also deduce that the unique 2-adic zero of the natural interpolation of (u_{4m}) is irrational, and we extend the argument to an infinite family of sequences. The accompanying Python script re-checks the numerical facts with exact integer arithmetic. The record also contains a Lean 4 project with a formal proof of the main theorem (Theorem 1.1), checked with the Mathlib library.