An integer linear recurrence sequence (LRS) is given by an order d, integer coefficients a₁,…,a_d, and integer seeds x₀,…,x_{d-1}, extended by x_{n+d} = a₁x_{n+d-1} + … + a_d x_n. The Skolem Problem asks: given such data, is it decidable in finite time whether x_n = 0 for some n?
The classical Skolem–Mahler–Lech theorem already answers a weaker question unconditionally: the zero set of any LRS is a finite set together with finitely many full residue classes, and the period of those classes is computable. What is not known in general is where the finitely many exceptional zeros sit — the proof of that part is p-adic and non-constructive (Tao, 2007). Separately, the decision problem itself — does a zero occur at all — has a full answer only for recurrences with at most three dominant characteristic roots, which in practice covers order ≤ 4. For order 5 and above, no algorithm deciding the Skolem Problem in general has ever been proposed. The best unconditional result to date (2026) shows only that the "hard" instances are density-zero: an algorithm exists for almost all seeds, and full decidability at order ≥ 5 would follow from a strengthened Cramér–Granville conjecture on prime gaps, which is itself open.
Fibonacci is order 2, Tribonacci order 3, Tetranacci order 4 — all inside the decidable region. Pentanacci is order 5. Hexabonacci is order 6. Both are past the line.
This corpus's recurrence ladder chapter (Book 3, published with the corpus's own priority timestamp of 24 March 2026) already walks φ (Fibonacci) → η (Tribonacci) → Δ (Tetranacci) → Σ (Pentanacci) → Ω (Hexabonacci → τ = 2), by name, as instances of one operator chain. Separately, NbonacciLadder.lean proves, for every order k and every natural-number-seeded sequence satisfying the k-term recurrence a(n+k) = a(n) + a(n+1) + … + a(n+k-1) with seeds bounded by a(i) ≤ 2^i:
Quantified over k, this one theorem already covers order 5 and order 6 — and every order past them — without being reproved at each step. That is a real, kernel-checked, order-independent fact sitting exactly where the Skolem Problem becomes open.
NbonacciLadder.lean is a growth bound, not a zero-decidability result, and its own header says so. Its hypothesis — natural-number seeds, each bounded by 2^i — forbids exactly the behaviour that makes the Skolem Problem interesting: a sequence with mixed-sign integer seeds that can fall back toward zero. A sequence that is provably increasing (eventually strictly) cannot return to zero after it starts, so the theorem, read carefully, proves the Skolem Problem trivially true for the narrow family it covers — not because anyone solved the order-5 case, but because the hypothesis excludes the case that would make it hard. This is not a defect in the file; the file never claims otherwise. It is the reason this thread is marked open rather than closed.
Genuine contact with the open problem needs the same technique — a proved, order-uniform bound used as a termination certificate — applied to a family that is not excluded from being hard by construction: integer (not natural-number) seeds, allowed to be negative, for a specific, stated order-5 or order-6 recurrence. The honest, checkable project is not "decide the Skolem Problem" but: pick one concretely stated order-5 instance, and formalise a decision procedure for that single instance in Lean, using a growth-rate bound in the style of NbonacciLadder.lean as the argument that a finite search is exhaustive. That is a real result if carried out — modest, fully scoped, citable — and it is the kind of thing this corpus's existing machinery is actually positioned to attempt. It has not been started.
| claim | status |
|---|---|
| Pentanacci/Hexabonacci sit past the order-4 decidability line | verified against current literature, 2026-09-27 |
| NbonacciLadder.lean bound holds for every order k | kernel-checked, 2026-09-09 |
| The dominant root ηk of xk = xk-1 + … + 1 tends to 2 (NbonacciLimit.lean) | compiled by the author 2026-10-22 (Lean v4.32.0 + Mathlib, no errors); seven theorems axiom-checked, standard axioms only; numbers cross-checked in docs/nbonacci-limit-check.py |
| That bound resolves any instance of the Skolem Problem | false — the hypothesis excludes the hard case |
| A concrete order-5 decision procedure, Lean-formalised | not started |
sorryAx). Per R20: a clean axiom report is not a reading of the statement — §3 above states exactly what these two theorems do and do not establish about the Skolem Problem. Follow the link before citing either as evidence of more.