Metadata

slug: a156216-diagonalghost
bibkey: hanna2009a156216
doi: null
url: https://oeis.org/A156216/internal
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/Witt/HannaDiagonalGhostPowerIntegrality.result

Hanna’s diagonal ghost-power integrality conjecture

Problem

Paul D. Hanna’s second comment in OEIS A156216, internal revision #3, reads:

More generally, if exp( Sum_{n>=1} C(n) * x^n/n ) equals a power series in x with integer coefficients, then exp( Sum_{n>=1} C(n)^n * x^n/n ) also equals a power series in x with integer coefficients (conjecture).

For a characteristic-zero field $K$ and $C : N \to K$ , put $H_{C} = \sum_{n \geq 1} C_{n} X^{n} / n$ and $F_{C} = exp (H_{C})$ , interpreted formally. The assertion is $F_C\in\mathbb Z[[X]]\Rightarrow F_{(C_n^n)}\in\mathbb Z[[X]]$, with the rings of integer series understood through the canonical embedding into $K [[X]]$ .

Statement echo

Source clause	Lean counterpart	Scope
The sequence $C (n)$	`claim` quantifies $K$ , its field and characteristic-zero structures, and $C : N \to K$	Every binding field and sequence
$\sum_{n \geq 1} C_{n} X^{n} / n$	`logarithmicInput` has coefficient zero at zero and $C_{n} / (n : K)$ otherwise	Entry $C_{0}$ is unused
The formal exponential	`exponentialSum` substitutes the logarithmic input into `PowerSeries.exp K`	Ordinary coefficients; no analytic condition
Integer input coefficients	The antecedent is the existing `HannaLogarithmicPowerClosure.IntegralSeries`	Canonical integer image
$C (n)^{n}$	The consequent uses the sequence $n \mapsto C_{n}^{n}$	Index-dependent natural power
Integer output coefficients	The consequent uses the same `IntegralSeries`	No positivity or nonzero restriction

The existing HannaDiagonalDerivativeParity.step a 0 is used in the private differential-equation proofs; the public claim retains the literal formal exponential. No source clause is dropped.

Motivation

The named external problem is preregistered in https://github.com/the-omega-institute/trureturing/issues/21407. The settling declaration is D5/S1/Recurrence/Witt/HannaDiagonalGhostPowerIntegrality.result. The source note is Library/RecurrenceComposition/hanna2009a156216.md. The admissible settlement is Proved, with admission_basis: open-problem-resolution (#21407; Proved). There is no theory atom or coverage edge for this external problem.

Gap

The integer Euler ledger of an integral input supplies signed divisor ghosts. A fixed Hadamard power does not directly address the simultaneous change of base and exponent from $C_{m p^{s}}^{m p^{s}}$ to $C_{m p^{s + 1}}^{m p^{s + 1}}$ . The proof handles this operation by local prime-power congruences and reconstructs the literal output exponential.

Route

Write the input’s Euler ledger as $(b_{d})_{d \geq 1}$ . The reused PrimitiveEulerLedger.unique_primitive_euler_ledger gives its integer coefficients and stable finite products. Formal differentiation identifies $C_{n} = \sum_{d ∣ n} d b_{d}$ for positive $n$ .

For every prime $p$ , $s \geq 0$ and $m > 0$ , the new divisors in $m p^{s + 1}$ are divisible by $p^{s + 1}$ . Hence $p^{s + 1} ∣ C_{m p^{s + 1}} - C_{m p^{s}}$ , even when $p ∣ m$ . Mathlib’s SModEq.pow_pow_add_one, applied in the private fermat_lift, lifts Fermat’s congruence. Base congruence and this lift give $p^{s + 1} ∣ C_{m p^{s + 1}}^{m p^{s + 1}} - C_{m p^{s}}^{m p^{s}}$ .

For an integer sequence $a$ satisfying these local congruences, prime pairing in the Moebius numerator proves $n ∣ \sum_{d ∣ n} μ (d) a_{n / d}$ . Its integer quotient is the output Euler ledger. The coefficient recurrence for $X f^{'} = L f$ , with prescribed constant coefficient, is unique in characteristic zero and identifies the integer Euler series with the literal formal exponential. All manipulations are finite in each coefficient.

Falsifier

A counterexample would be a binding characteristic-zero field and sequence whose input exponential has embedded integer coefficients while an output coefficient does not. The universal theorem result : claim excludes that case within Lean’s accepted axiom closure. Numerical prefixes alone do not exclude a counterexample beyond their bounds.

Evidence

The kernel statement is HannaDiagonalGhostPowerIntegrality.result in D5/S1/Recurrence/Witt/HannaDiagonalGhostPowerIntegrality.lean. Its only public definitions are logarithmicInput, exponentialSum and claim. The Blueprint displays the full statement and the source expressions.

Independent finite computation

Published experiment directory. The immutable script is docs/reports/oeis-a156216-hanna-diagonal-power-integrality/check.py; its SHA-256 is 4a8078da8433455f65e9d9d52a52e0b1d35ee98ae09611d5d098317826a7f1f9. Python 3 execution of those immutable bytes exits 0 with final result ALL_CHECKS_OK. The exact tested scopes are: all 14 displayed A156216 coefficients in degrees $0 \dots 13$ ; Lucas ghosts in degrees $1 \dots 40$ ; all $3125$ degree-five integer input polynomials with coefficients in ${- 2, - 1, 0, 1, 2}$ through degree 24; all $625$ signed Euler ledgers on indices $1, \dots, 4$ with exponents in that set through degree 40; 12 signed inputs with an independent literal exponential computation through degree 24; and Fermat lifting for $- 30 \leq z \leq 30$ , $p \in {2, 3, 5, 7, 11}$ and $1 \leq r \leq 4$ . These are computed results, not an unbounded proof.

Escape audit

The unfinished audit is https://github.com/the-omega-institute/trureturing/issues/21518. Its targets are the settling result and the published owner lemmas PrimitiveEulerLedger.ledgerProduct_succ and PrimitiveEulerLedger.coeff_mul_eulerFactor_of_lt, and the published owner definition HannaDiagonalDerivativeParity.step (an additional audit target under this delivery’s brief; definitions are exempt from the theorem-only SL-031 delta check). No Reg registration or declared_validated status is asserted. The missing evidence is a faithful typed realization and equivalence bridge, variation, sensitivity and observational dependence for the exact statements.

Triage

Item	Status and evidence kind	Evidence
The premise forces every positive-index $C_{n}$ to be an embedded integer divisor ghost	Proved; kernel-checked private lemma	`integral_input_ledger` constructs $b$ with $C_{n} = \sum_{d ∣ n} d b_{d}$ in $K$ for every $n > 0$
Arbitrary signed divisor ghosts satisfy local Gauss congruences for every $m > 0$ , including $p ∣ m$ ; diagonal self-powers preserve them	Proved; kernel-checked private lemmas	`divisor_ghost_gauss` and `diagonal_congruence`, composed in `result`
Every integer sequence satisfying the stated local Gauss condition has an integral literal exponential and an integer Moebius ledger	Proved; kernel-checked private lemmas	`gauss_moebius_divisible`, `gauss_has_ledger`, `gauss_exponential_integral`
Zero and negative ghosts and all binding characteristic-zero fields are included without positivity or analytic assumptions	Proved; kernel-checked theorem	The full statement of `result`; its only premise is input integrality
The finite checker ends `ALL_CHECKS_OK`	Computed	The immutable experiment and exact scopes in Evidence; exit 0 and matching script SHA-256
Exhaustive literature priority, including the unread Du-Huang-Li paper	Open; literature reading boundary	The bounded literature screen in #21407; completeness is `ASSUMED-UNVERIFIED`
General index-dependent exponent transforms beyond $n$	Open	No classification is asserted by `result`

What the settlement shows

Proved (kernel-checked result): the local congruence mechanism suffices for the whole source claim and therefore includes its Lucas-sequence example. Proved (kernel-checked private integral_input_ledger): integrality of the ghosts is a consequence of input integrality; it need not be assumed. Proved (kernel-checked private divisor_ghost_gauss): the local formulation needs no coprimality condition on the positive multiplier $m$ .

Open: a classification of other exponent sequences. The present theorem settles no additional named conjecture. The OEIS coefficient recurrence and its Lucas example are compatible with the proved universal assertion; no other source theorem is claimed to depend on it. The finite OEIS values listed in Evidence are computed, rather than separate Lean theorems.

ASSUMED-UNVERIFIED

Literature completeness and worldwide priority are ASSUMED-UNVERIFIED. The inspected source and the bounded screen in #21407 do not constitute an exhaustive priority determination. The Du-Huang-Li 2003 original, DOI 10.1016/S0022-314X(02)00025-2, and the Newton-Euler paper, DOI 10.1016/J.JNT.2005.05.004, remain unread boundaries. The supporting Dold-sequence survey is Byszewski-Graff-Ward, arXiv:2007.04031v4, DOI 10.1112/blms.12531; it is not the source of Hanna’s conjecture.

Keyboard shortcuts

trureturing — Discovering truth