The source audit through 2026-07-28 found no unconditional decision procedure for arbitrary-order integer linear recurrence sequences and no undecidability reduction. Bacik proves decidability for algebraic linear recurrence sequences of order at most four. Bacik, Ouaknine, and Worrell place the bounded problem for every fixed order in coRP and obtain the same upper bound for the unrestricted order-four problem. A restricted family reaches higher order: Kenison gives an alternative proof of decidability for reversible integer LRS of order at most seven.

The 2026 p-adic algorithm has unconditionally correct output whenever it terminates. Its termination proof assumes the p-adic Schanuel Conjecture. The July 2026 preprint obtains general decidability under a strengthened Cramér-type conjecture and proves unconditionally that the possible large-zero indices have density zero. These results narrow the search without deciding the general target. The first order outside the unconditional general frontier is five.

Let the recurrence have order \(d\), final coefficient \(c_d\in\{-1,1\}\), and companion state \[ X_n=(u_n,u_{n+1},\ldots,u_{n+d-1})^{\mathsf T}. \] Its companion matrix \(A\) has determinant \((-1)^{d-1}c_d\). Hence \(A\) is invertible over \(\mathbb Z\) and modulo every integer \(m\ge2\). The initial data therefore has a unique bi-infinite integer extension.

Fix a negative index \(j<0\) with \(u_j=0\). Modulo \(m\), the map \(X\mapsto AX\) permutes the finite state space \((\mathbb Z/m\mathbb Z)^d\). The state \(X_j\) lies on a finite cycle, so some \(P\ge1\) satisfies \(A^P X_j=X_j\pmod m\). Choose \(q\) with \(j+qP\ge0\). Then \[ u_{j+qP}\equiv u_j\equiv0\pmod m. \] This holds for every modulus.

For a simple order-two example, take \(u_0=u_1=1\) and \(u_{n+2}=u_{n+1}+u_n\). Its bi-infinite extension is \(u_n=F_{n+1}\), so \(u_{-1}=0\). Every term with \(n\ge0\) is positive. Thus the one-sided sequence has no integer zero, while every modulus has a zero at a nonnegative index. The characteristic polynomial \(x^2-x-1\) has distinct roots.

The conclusion concerns a sieve that seeks one modulus with no nonnegative modular zero. It says nothing about general Skolem decidability. It also agrees with the published Exponential Local-Global Principle, whose integer-index formulation sees the zero at \(n=-1\).

The audit ran on 2026-07-28. It searched arXiv, Dagstuhl DROPS, DOI records, and TheoremDB using the exact phrases “Skolem Problem,” “linear recurrence zero,” “order 5,” “reversible sequence,” “p-adic Skolem,” and “local-global,” together with equivalent orbit-problem wording. It inspected the complete canonical target, its acceptance conditions, its qualification review, and every attached record. Production held no attached research object for this target.

TheoretiCS records unconditional decidability through order four. The SODA 2026 paper gives a coRP algorithm for the bounded problem at every fixed order and a coRP upper bound at order four. Kenison gives an alternative proof that the reversible integer subclass is decidable through order seven and identifies order eight as its next open frontier. STACS 2026 gives p-adic zero algorithms with unconditional correctness and conjectural termination. LICS 2026 still describes the hyperplane Orbit Problem, equivalent to general Skolem, as open. The arXiv preprint submitted on 2026-07-16 gives conditional general decidability and an unconditional null-density theorem for possible large-zero indices.

Exact target and equivalent-wording searches found no second canonical problem. TheoremDB global search returned unrelated uses of Skolem choice and linear-recurrence library declarations. Production orient returned the exact canonical problem 2836 and zero attached research records. Both plan checks reported low duplicate risk and advised proceeding with explicit scope.

A zero-free orbit modulo one integer \(m\ge2\) is a sound certificate that an integer LRS has no zero. The attempted complete method searches for such a modulus whenever direct zero search finds nothing.

The Fibonacci shift \(u_n=F_{n+1}\) ends this route as a general one-sided procedure. Positivity proves \(u_n\ne0\) for every \(n\ge0\). Its recurrence is reversible, and its bi-infinite extension has \(u_{-1}=0\). The companion-state proof shows that the negative state returns at a nonnegative time modulo every \(m\). Exact replay finds the first modular zero and the full pair-state period for all 511 moduli through 512.

This failed route does not challenge the Exponential Local-Global Principle in STACS 2026. That conjecture concerns simple rational linear recurrent bi-sequences and zeros indexed by all integers. The Fibonacci shift has the integer zero \(u_{-1}=0\), exactly matching its local zeros. Any modular approach to the TheoremDB target must retain the one-sided index condition.

Define an order-\(d\) companion state over \(\mathbb Z\) and \(\mathbb Z/m\mathbb Z\). Under \(c_d=\pm1\), construct the inverse update and the bi-infinite extension. Prove that every state modulo \(m\) is periodic. Transport a negative-index zero to a nonnegative congruent zero.

State the broader coprime-modulus variant as a separate lemma. For \(c_d\ne0\), the backward extension lies in \(\mathbb Z[1/c_d]\). Reduction modulo \(m\) is defined when \(\gcd(c_d,m)=1\), and the same finite-permutation proof applies. Keep the all-modulus conclusion as the \(c_d=\pm1\) corollary.

Specialize the statement to \(u_0=u_1=1\) and \(u_{n+2}=u_{n+1}+u_n\). Prove \(u_n=F_{n+1}\), positivity for \(n\ge0\), and \(u_{-1}=0\). Use the selected replay rows only as tests. The formal theorem should preserve the distinction between \(\mathbb Z\)-indexed and \(\mathbb N\)-indexed zero predicates.

The repository replay has two exact parts. For \(u_n=F_{n+1}\), it enumerates the complete pair-state cycle modulo every integer \(m\) between 2 and 512. All 511 moduli have a nonnegative modular zero. The ordered row digest is `6eb196a28c2cac0d194ce1af150c99bdc5e64591ef0c163d3c4d79f43a76d082`.

The second part exhausts every tuple \((a,b,u_0,u_1)\in[-3,3]^4\) for \(u_{n+2}=au_{n+1}+bu_n\). It checks exact integer terms through index 1000. For a row without a witnessed zero, it searches moduli 2 through 64. Each modular check follows the deterministic pair state until a repeat, so a zero-free completed orbit is a proof that no integer zero exists at any nonnegative index.

The partition has 841 witnessed rows, 1,508 rows with a modular nonzero certificate, and 52 inconclusive rows. Every certificate found already uses a modulus at most 11. Forty inconclusive rows have \(b=\pm1\) and a checked negative zero within eight backward steps. The boundary lemma proves that such a negative zero blocks this certificate form for every modulus. The census makes no claim about an unwitnessed integer zero in an inconclusive row.