slug: oeis-a380681-hanna-prime-bilateral-integrality
bibkey: hanna2025a380681
doi: null
url: https://oeis.org/A380681
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/Bilateral/HannaPrimeBilateralIntegrality.result

Hanna’s prime bilateral integrality conjecture

Problem

P. D. Hanna’s OEIS A380681, Comments section, states:

Conjecture: if F(x) satisfies px = Sum_{n=-oo..+oo} (-1)^n * x^(pn) * (F(x) + x^n)^(p*n) with F(0) = 1 for some fixed integer p, then F(x) is an integer series in x iff p is prime. The g.f. A(x) of this sequence is the case when p = 2; other cases include A380682 (p=3), A380683 (p=5), A380684 (p=7), A380685 (p=11), and A380686 (p=13).

Preregistration: #18831. The Library note records the source. The formal parameter is $p\in \mathbb{N}$ with $p\ge 2$, and $F\in \mathbb{Q}[[X]]$. Integer powers are taken in $\mathbb{Q}((X))$. At degree $N$, the bilateral sum means every symmetric window $[-K,K]$ with $K\ge N+1$.

Statement echo

The Lean namespace is D5.S1.Recurrence.Bilateral.HannaPrimeBilateralIntegrality.

No source clause within the preregistered interpretation is dropped. Both the claim and result Blueprint nodes display the complete proposition.

Motivation

The equation relates an infinite bilateral Laurent sum to an integral coefficient recursion. The settling GID is D5/S1/Recurrence/Bilateral/HannaPrimeBilateralIntegrality.result. It proves existence for every $p\ge 2$ and characterizes integrality by primality.

Gap

The source and literature screen in #18831 found no proof or refutation of the common conjecture in A380681–A380686. The screen includes the entries and their revisions, repository issues, LeanOpenProblems-results and formal-conjectures. The research reading of revisions is seat-reported in that issue. Completeness of the screen is ASSUMED-UNVERIFIED.

Route

For $n=-m<0$, factor the summand as $(-1{)}^m{X}^{pm(m-1)}(1+X^{m}F{)}^{-pm}$. Together with the positive summands this makes each coefficient a finite sum. At parameter one, the positive term indexed by $m$ with power $F^b$ pairs with the negative term indexed by $r=m-b+1$, $j=b$; their exponents and binomial coefficients agree and their signs are opposite. The remaining negative constant cancels the zero-index summand.

For prime $p$, Frobenius transfers this cancellation to divisibility by $p$. Removing the linear term gives a map that improves coefficient agreement by one degree. Compatible iterates construct the rational solution and retain integer coefficients. The proof applies the imported CubicFifteenSubstitutionParity.prime_power_subst and PowerSeriesNormalizedContraction.exists_unique_fixed. The shared HannaThetaFourModFour.symmetric_pair separates the symmetric window; NegativePowerDiagonalModPrime.inverse_difference gives the normalized inverse difference. The theorem BilateralProductModFour.ofSeries_inverse identifies inverses under the Laurent embedding.

Below degree $p$, the equation yields $r={\prod }_{j<r}(1+jp)$ for $r<p$. If $p$ is composite and $q$ is its least prime divisor, $q\mid q!$ but $q$ divides none of the numerator factors. An integer coefficient would contradict this divisibility obstruction.

Falsifier

A normalized rational solution at prime $p\ge 2$ with a noninteger coefficient, or one at composite $p\ge 2$ with every coefficient integral, contradicts result. A different convention for bilateral summation or nonpositive parameters changes the statement.

Evidence

D5.S1.Recurrence.Bilateral.HannaPrimeBilateralIntegrality.result proves the full claim. Its admission basis is open-problem-resolution (#18831; Proved). The public theorem is classified content; the cancellation, construction and coefficient obstruction are on its derivation path. The module has generality: I and utility: none.

The four-slot escape audit is unfinished under issue #19820 for this result, HannaThetaFourModFour.symmetric_pair and NegativePowerDiagonalModPrime.inverse_difference. The missing evidence is complete source reconstruction and lawful variation, sensitivity and observational dependence for their quantified series and group-valued function families. No declared_validated registration is claimed.

Reused public owners

• D5.S1.Recurrence.Bilateral.HannaThetaFourModFour.symmetric_pair: declaration statement_id sha256:ec2ce3acb9c693250b8c1744ab57b32dfa6f8e22a0268b5edce1f5d12206504e; unfinished audit #19820.
• D5.S1.Recurrence.Residue.NegativePowerDiagonalModPrime.inverse_difference: declaration statement_id sha256:de95009be8a3f6b4675b86334f6afe96cbcfe4cc07412482ab82bb4431065824; unfinished audit #19820.

Declaration judgement

Experiment

Published checker and data. Command in that pinned directory: python3 check.py; exit 0, RESULT PASS. The check.py SHA-256 is ec87bb1637d6a946d4e5fb43f078bc623ce327257ef53b9305c05c564ca154b5. For $p=2,3,4,5,6,7$, the computed solution includes coefficients through degree 11 and the equation through degree 12. For $p=8,9,10,11,13,15$, those degrees are 8 and 9. The prime cases match A380681–A380686 and have integral coefficients. For the tested composites the first noninteger coefficient is at $q-1$ and equals ${\prod }_{j<q}(1+jp)/q!$. Three integer series selected with seed 7 satisfy ${\Psi }_1(Y)=0$ and ${\Psi }_3(Y)\equiv 0(\mathrm{mod}3)$ through degree 12. These are finite computations, separate from the uniform kernel-checked settlement.

Triage

What the settlement shows

The decisive mechanism is bilateral cancellation followed by Frobenius and a coefficient contraction. The arbitrary-ring cancellation and low-degree coefficient identity specify how far the argument extends. The stronger first-failure assertion remains distinct from the proved integrality criterion. No further source result relying on the conjecture is identified by the literature screen; its completeness remains ASSUMED-UNVERIFIED.

ASSUMED-UNVERIFIED

Literature-search completeness and the absence of an external settlement outside the searched material are ASSUMED-UNVERIFIED. The uniform exact first-failure and reduced-denominator assertion is not formalized. Nonpositive parameters are outside the claim. The unfinished escape audit supplies no registration validation.