bibkey: hanna2025a384819
authors: Paul D. Hanna
year: 2025
title: "OEIS A384819: bounded integral square-weight corrections"
doi: null
url: https://oeis.org/A384819
claim: "Conjecture: a(p^n) = p - 1 when p is prime for n >= 1."
strata_touched:
  - D5/S3/Arith/Congruence/HannaPrimePowerCorrection
license: citation-only
triage: anchor

Bounded square-weight corrections

Verified locator

https://oeis.org/A384819

The source is Paul D. Hanna’s OEIS A384819, approved revision 14. There is no source arXiv identifier or linked source paper.

The NAME states verbatim:

Nonnegative numbers a(n) < n for n >= 1 such that exp( Sum_{n>=1} (n^2 - a(n))*x^n/n ) is a power series with integral coefficients.

The sole COMMENTS line states verbatim:

Conjecture: a(p^n) = p - 1 when p is prime for n >= 1.

OEIS has no page number; these locators are the NAME and COMMENTS fields. The offset is 1,3. The integer sequence starts at index one. All series and exponentials are formal over the rationals, with ordinary coefficients. The exponent has zero constant coefficient. The unused value a(0) imposes no constraint. The positive source exponent n is renamed r, and the prime p ranges over every natural prime, including two.

The integer-coefficient condition uses the existing IntegralSeries predicate. The formal sum and its exponential agree definitionally with logarithmicInput and exponentialSum in HannaDiagonalGhostPowerIntegrality for the sequence m ↦ m² − a(m). The source formulas are expanded in the correction predicate.

Mathematical mechanism

The integral exponential has an integer Euler ledger. Its scaled logarithmic derivative $x{F}^{\prime }/F$ has coefficients given by the integer divisor sum. At successive powers of a prime, subtracting the two divisor sums leaves one ledger term divisible by the larger prime power. The bound 0 ≤ a(m) < m selects the unique residue and forces stabilization at p − 1. Neither positivity of exponential coefficients nor nonnegative Euler exponents is needed. A384820 is the associated integral series; the source states no additional theorem depending on the conjecture.

Finite computation

The independent checker is in the private repository https://github.com/the-omega-institute/trureturing-experiments, commit 0916ed2028a0f5b6655667b45b620902fe84fcd4, at docs/reports/hanna-a384819-primepower/check.py, SHA-256 f36ce92f3986ede4ecae3c75d79e10caf2bd083ddb5e5d7994412da3c92bc86b. The preregistration https://github.com/the-omega-institute/trureturing/issues/21787 records exit 0 and ALL_CHECKS_OK: 520 published sequence terms, 41 displayed exponential coefficients, and 340 prime-power indices at most 2048. These finite checks concern source fidelity; the universal assertion is the separate Lean theorem.

Literature boundary

The literature screen in issue 21787 found no exact prior settlement in its inspected sources. It includes primary OEIS revision history and the classical Euler/Dold and Witt-vector background. OpenAlex and Semantic Scholar were rate-limited, global arXiv full-text search timed out, and other bounded or blocked discovery surfaces remain disclosed there. Comprehensive literature completeness is ASSUMED-UNVERIFIED. No mathematical originality follows from the absence of a located prior proof.