bibkey: bala2022a000071 authors: Peter Bala year: 2022 title: “OEIS A000071: Bala’s strong divisibility conjecture for Fibonacci minus one at odd-base powers” doi: null url: https://oeis.org/A000071 claim: “Conjecture: for k a positive odd integer, the sequence {a(k^n): n >= 1} is a strong divisibility sequence; that is, for n, m >= 1, gcd(a(k^n), a(k^m)) = a(k^gcd(n,m)).” strata_touched:

• D5/S1/Recurrence/BalaFibonacciPowerStrongDivisibility license: citation-only triage: anchor

A000071: odd-base strong divisibility

Verified locator

Source: https://oeis.org/A000071, COMMENTS, Peter Bala, Dec 05 2022. The entry’s NAME is a(n) = Fibonacci(n) - 1. Its offset field is 1,4, so the first sequence index is 1. The conjecture is quoted verbatim in claim above. The author field attributes the conjecture to Bala, not the entire sequence entry.

The OEIS JSON source check on 2026-09-21 (Asia/Singapore) confirmed NAME, the complete conjecture comment, offset 1,4, revision 493, and modification time 2026-05-30T04:28:26-04:00.

Scope and attribution

The full formal target has natural k, n, m, Odd k, n>0 and m>0. It includes k=1, all index parities, and the primes 2 and 5. Natural subtraction is faithful because positive Fibonacci indices have value at least one. No offset change or additional hypothesis is imposed.

The bounded source investigation recorded in issue #9152 on 2026-09-21 inspected cited passages in arXiv:1701.06722v2, 2402.19301v1, 2408.14632v2 and 2503.11055v1 without finding this exact settlement. These are the investigation’s recorded findings; the paper readings were not repeated during report and documentation preparation. The checked OEIS revision still labels the clause Conjecture. The search is bounded to the inspected sources and does not establish worldwide priority.

The external Lean search recorded in the same investigation found a sequence definition in sequencelib and a shifted golden-orbit result in rwst/lean-code, neither supplying the exact target theorem. The implementation directly uses the verified frozen Lucas recurrence, companion-power shape and determinant suppliers and the pinned Mathlib periodic-point and prime-power divisibility contracts. The resulting proof is a repository derivation of Bala’s conjecture; Bala is credited with the statement, and the proof uses the suppliers detailed in the problem dossier.