bibkey: zizka2025a390871
authors: Ctibor O. Zizka
year: 2025
title: A390871 — square differences of Mersenne form
doi: null
url: https://oeis.org/A390871
claim: The entry conjectures the binary exponent interval for non-power-of-two terms greater than eight.
strata_touched:
  - D5/S3/Arith/Mersenne/GapExponentBounds
license: citation-only
triage: anchor

A390871

Verified locator

Canonical entry URL: https://oeis.org/A390871

Canonical entry URL: https://oeis.org/A390871 The entry has no DOI. Revision 48 of its internal page is dated 2025-12-11. Zizka submitted the entry on 2025-11-22. Its exponent interval comment says “I conjecture”. Robert Israel’s comments dated 2025-12-01 establish divisibility by four and a factor construction; they do not prove that exponent interval.

Statement and repository proof

For natural numbers k, r, m with k greater than eight, k not a power of two, r less than k, m at most k, and k squared plus one equal to r squared plus 2 to the m, the conjectured interval is floor(log base 2 of k) + 3 ≤ m ≤ 2 floor(log base 2 of k) + 1. The addition form avoids truncated natural subtraction.

The repository proof first rules out exponent zero. A gap k−r equal to one forces k to be a power of two; a gap equal to two contradicts parity. Thus r+3≤k, and comparison with (k−3) squared gives 6k≤2^m+8. The two defining inequalities for the integer logarithm then give the claimed interval. The argument also covers r=0 and does not need m≤k, although that defining restriction is retained in the theorem statement. The example (12,9,6) attains the lower bound; it is not separately frozen.

Proof scope

The Lean derivation uses Mathlib’s logarithm and power comparison lemmas. It is repository work. No publication priority or exhaustive literature coverage is claimed.