Metadata

slug: h384819-primepower
bibkey: hanna2025a384819
doi: null
url: https://oeis.org/A384819
triage: theorem
motivation_gids:
  - D5/S3/Arith/Congruence/HannaPrimePowerCorrection.result

Hanna’s prime-power correction formula

Problem

Paul D. Hanna, OEIS A384819, approved revision 14, NAME:

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 conjecture is:

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

All series are formal over the rationals. The offset is 1,3; the unused value $a (0)$ is unconstrained. The conclusion quantifies over every integer sequence satisfying the defining condition, every natural prime $p$ , and every natural exponent $r \geq 1$ .

Statement echo

Source clause	Formal counterpart	Fidelity
Nonnegative numbers $a (n) < n$ for $n \geq 1$	`IsCorrection`: integer-valued sequence and both positive-index bounds	Literal
Integral coefficients of the specified formal exponential	`IsCorrection`: literal `PowerSeries.mk`, rational division, `PowerSeries.subst`, `PowerSeries.exp`, and reused `IntegralSeries`	Literal; the exponent’s constant coefficient is zero
$p$ prime	`claim`: `Nat.Prime p`	Includes 2
$n \geq 1$	`claim`: positive natural exponent $r$	Bound variable renamed
$a (p^{n}) = p - 1$	`result` proves `claim`	Unbounded in both parameters
Every solution; natural index zero	Universal sequence binder and an unused $a (0)$	No choice of a canonical solution and no added restriction

Motivation

The settling GID is D5/S3/Arith/Congruence/HannaPrimePowerCorrection.result. It resolves the source’s prime-power assertion rather than extending a finite table. Admission is open-problem-resolution (#21787; Proved). The arithmetic induction bounded_prime_powers is content and supplies the escape witness on the live derivation path of the content theorem result. The two ghost-identity adapters are consumed bind-only helpers. The literal exponent and exponential are inlined in IsCorrection; proofs reuse exponentialSum through definitional correspondence.

Gap

Preregistration #21787 records the source and literature screen on 2026-10-25. Its inspected OEIS revision retains the conjecture and links no source paper or arXiv identifier. The inspected Euler/Dold and Witt-vector sources supply classical background rather than this bounded square-correction conclusion. That screen found no settlement predating the preregistration; its completeness is ASSUMED-UNVERIFIED.

Independent later settlement

Congruences, Stirling Transforms, Meixner Fractions, and Euler Products in Integer Sequences, Zenodo DOI 10.5281/zenodo.23726063, was published on 2026-10-29, following preregistration #21787 on 2026-10-25.

Route

Put $b_{m} = m^{2} - a (m)$ . Formal integrality yields an integer Euler ledger $(e_{d})$ with $b_{m} = \sum_{d ∣ m} d e_{d}$ for positive $m$ . This is the necessary integrality direction in the reused integral_input_ledger, specialized by correction_ghost. The reused divisor_ghost_gauss, specialized by prime_power_difference, gives $p^{r} ∣ b_{p^{r}} - b_{p^{r - 1}}$ . The bound at 1 forces $a (1) = 0$ . At $p$ , the unique residue in $[0, p)$ is $p - 1$ . For $r \geq 2$ , both square terms are divisible by $p^{r}$ , so the two corrections are congruent modulo $p^{r}$ . Their bounds put them in the same representative interval, hence they agree. bounded_prime_powers performs this induction; result combines the three helpers.

Falsifier

A bounded integral correction and a prime $p$ with positive $r$ for which $a (p^{r}) \neq = p - 1$ would falsify the conjecture. A finite test or a failed registration is neither such a correction nor a refutation.

Evidence

The Lean source is D5/S3/Arith/Congruence/HannaPrimePowerCorrection.lean; its public theorem is D5.S3.Arith.Congruence.HannaPrimePowerCorrection.result. The Scribe gives the complete defining expression and expanded settling proposition. The reused owner publishes divisorGhost, GaussCondition, divisor_ghost_gauss and integral_input_ledger with their statements and proofs preserved; its frozen state requires a canonical owner re-pin.

Escape audit unfinished: #25058. The universal sequence and formal-integrality hypothesis have no delivered four-slot registration. The newly public owner theorems HannaDiagonalGhostPowerIntegrality.integral_input_ledger and HannaDiagonalGhostPowerIntegrality.divisor_ghost_gauss are additional audit targets under the same issue; the exact reconstruction, observational dependence, and variation/sensitivity evidence remain missing. No declared_validated registration is claimed.

Finite source checks

The pinned experiment is trureturing-experiments, hanna-a384819-primepower. Command: python3 /tmp/op-h384819/rework-round2/check.py; exit 0. Script SHA-256: f36ce92f3986ede4ecae3c75d79e10caf2bd083ddb5e5d7994412da3c92bc86b. The script is read from the linked immutable revision with git show; its bytes have the stated SHA-256. All 520 published A384819 terms ( $1 \leq n \leq 520$ ), all 41 displayed A384820 coefficients ( $0 \leq n \leq 40$ ), and all 340 prime-power indices at most 2048 match. The coefficient recurrence and divisor-ledger recursion agree through 2048; the divisor-sum ghost identity holds at every index from 1 through 2048. The signed-binomial Euler product agrees through degree 96 and the rational Taylor expansion through degree 32. At each index from 1 through 64, all allowed corrections are tested with the computed prior prefix fixed, and exactly the computed correction gives an integral next coefficient. Replacing $a (2)$ by zero gives the nonintegral coefficient $5/2$ . These are finite computations.

Triage

Item	Status and evidence kind	Evidence
Integrality alone supplies the necessary integer divisor-sum ghost identity; bounds are used only afterwards	Proved; kernel-checked owner	`HannaDiagonalGhostPowerIntegrality.integral_input_ledger` has only formal integrality as its premise; `correction_ghost` applies it to the integral component
All primes, including 2, and all positive exponents; $a (0)$ irrelevant	Proved; kernel-checked	Full statement of `HannaPrimePowerCorrection.result`
No nonnegative Euler exponents or positive exponential coefficients	Proved; kernel-checked	Complete hypotheses of `result`, and integer-valued ledger from `correction_ghost`
The bounded integral defining condition is inhabited by the quotient/remainder Euler-ledger construction	Proved in prose	The construction and formal-series argument below; no additional retained Lean theorem
520 source terms, 41 exponential coefficients, and 340 prime powers through 2048 match	Computed	Pinned experiment, command, exit 0 and SHA-256 in Evidence; no assertion beyond its stated ranges
Independent coefficient and divisor-ledger recursions agree, and the divisor-sum ghost identity holds, at indices 1 through 2048	Computed	Pinned experiment in Evidence, exit 0; exact integer and rational arithmetic
Signed-binomial Euler product through degree 96 and rational Taylor exponential through degree 32 match the coefficient recurrence	Computed	Pinned experiment in Evidence, exit 0; finite truncations only
At each index 1 through 64, given the computed prior prefix, exactly one allowed correction gives an integral next coefficient; $a (2) = 0$ gives $5/2$	Computed	Exhaustive correction test and negative control in the pinned experiment, exit 0
Analogous prime-power assertion for weights $m^{k}$ , $k \geq 2$	Open	Separate adjacent assertion; neither formalized nor settled here
Uniqueness on all positive indices and a closed composite-index formula as additional Lean results	Open	No such additional Lean results are delivered

What the settlement shows

The decisive mechanism is that integrality supplies divisibility, while the bounded representative interval upgrades congruence to equality. It covers all primes and positive exponents without positivity assumptions on either Euler exponents or exponential coefficients (result, kernel-checked). The source associates A384820 with the resulting integral series, and states no further theorem depending on its COMMENTS conjecture.

For nonvacuity, the following is a proof in prose. Recursively for $m \geq 1$ , let $S_{m} = \sum_{d ∣ m, d < m} d e_{d}$ and take $a (m)$ to be the least nonnegative residue of $m^{2} - S_{m}$ modulo $m$ . Then $e_{m} = (m^{2} - S_{m} - a (m)) / m$ is an integer and $0 \leq a (m) < m$ . The formal product $F = \prod_{d \geq 1} (1 - x^{d})^{- e_{d}}$ is well-defined over $Z [[x]]$ : integer powers and inverse powers have integral binomial coefficients, and each coefficient depends on finitely many factors. Its constant coefficient is 1 and its scaled logarithmic derivative $x F^{'} / F$ has coefficient $\sum_{d ∣ m} d e_{d} = m^{2} - a (m)$ at $x^{m}$ . The specified formal exponential has the same scaled logarithmic derivative and constant coefficient. Over $Q [[x]]$ , equality follows recursively from the differential equation $m F_{m} = \sum_{j = 1}^{m} b_{j} F_{m - j}$ . Thus this product is the required integral exponential and the defining condition is inhabited. This paragraph proves existence in prose; it is not an extra kernel-checked claim.

Weights $m^{k}$ for $k \geq 2$ , all-positive-index uniqueness as a retained Lean result, and a closed composite-index formula remain outside this settlement.

ASSUMED-UNVERIFIED

Completeness of the preregistration search for settlements predating 2026-10-25 is ASSUMED-UNVERIFIED. The preregistration’s OpenAlex and Semantic Scholar requests were rate-limited; global arXiv full-text discovery timed out, and bounded metadata screens do not constitute exhaustive search. No originality or first-publication priority is inferred. Four-slot audit evidence remains unfinished under #25058.

Keyboard shortcuts

trureturing — Discovering truth