bibkey: bala2022a221077 authors: Peter Bala year: 2022 title: “OEIS A221077, e.g.f. Sum_{n>=0} tanh(nx)^n” doi: null url: https://oeis.org/A221077 claim: “E.g.f.: Sum_{n>=0} tanh(nx)^n. Conjecture: Let p be prime. The sequence obtained by reducing a(n) modulo p for n >= 1 is purely periodic with period p - 1. For example, modulo 7 the sequence becomes [1, 1, 6, 1, 0, 4, 1, 1, 6, 1, 0, 4, 1, 1, 6, 1, 0, 4 …], with an apparent period of 6. - Peter Bala, Jun 01 2022” strata_touched:

• D5/S1/Recurrence/Periodic/TanhPowerPrimePeriod license: citation-only triage: anchor

OEIS A221077

The entry specifies the exponential generating function and records Peter Bala’s June 1, 2022 conjecture quoted above. Its initial data are 1, 1, 8, 160, 5888, 345856, 29677568, 3502489600, 544181977088. The quoted entry retains the conjecture without a proof note; no proof was located in the accompanying literature search. This is not a claim of exhaustive absence.

Finite formula and scope

Write S(n,m) for the Stirling number of the second kind. The Lean definition sets a(0)=1 and, for n>=1, takes the following derived finite formula as its definition:

a(n) = Sum_{m=1..n} 2^(n-m) m! (m-1)! S(n,m) S(n+1,m).       (9)

The e.g.f. identity linking this definition to the NAME is not formalized. The derivation below is mathematical prose, not an additional Lean theorem. The formal results prove the period for (9) at every odd prime and refute its p=2 instance. In particular, a(1)=1 and a(2)=8 have different residues modulo 2. The claimed period p-1 is not asserted to be minimal.

For the derivation at positive n, put y=exp(2kx)-1. For k>=1,

tanh(k*x)^k = (y/(2+y))^k
  = Sum_{m>=k} (-1)^(m-k) choose(m-1,k-1) 2^(-m) y^m.

The standard Stirling expansion gives

n! [x^n] (exp(2*k*x)-1)^m = (2*k)^n m! S(n,m).

The summands vanish for m>n; hence coefficient extraction uses finite sums. Interchanging the k and m sums leaves

a(n) = Sum_{m=1..n} 2^(n-m) m! S(n,m) D(m,n),
D(m,n) = Sum_{k=1..m} (-1)^(m-k) choose(m-1,k-1) k^n.

Multiplication by m, the identity mchoose(m-1,k-1)=kchoose(m,k), and Stirling inclusion-exclusion at exponent n+1 give m*D(m,n)=m!*S(n+1,m). Since m>=1, cancellation yields D(m,n)=(m-1)!*S(n+1,m), proving (9) in prose.

Formal period argument

Terms with m>=p vanish modulo p through m!, while terms with m>n vanish through S(n,m). This gives the fixed window 1<=m<p. For odd p, 2 is a unit. Inside this window m is also a unit, and (m-1)!=m^(-1)*m! in ZMod p. Two applications of the frozen Stirling inclusion-exclusion theorem give the fixed triple sum

a(n) = Sum_{1<=m<p} Sum_{0<=j<=m} Sum_{0<=k<=m}
  (2^(-m) m^(-1) (-1)^(m-j) choose(m,j)
    (-1)^(m-k) choose(m,k) k) (2*j*k)^n                 in ZMod p.

Here negative powers denote field inverses. The coefficients do not depend on n. The frozen positive-power period theorem applies to every base 2jk, including zero, and proves equality at n and n+(p-1) for every n>=1.

The named proposition bala_conjecture_two is the p=2 instance for (9). Its closed negation bala_conjecture_two_false supplies the refutation certificate; the finite calculation is used only to refute this named claim.

Verified locator

• URL: https://oeis.org/A221077