Hanna’s A226838 congruence

Abstract

Every factorial-normalized coefficient of the original square-exponent rational EGF has an integral residue witness modulo six.

All series are formal power series over the rationals. The notation natval denotes the natural-to-rational cast, val the integer-to-rational cast, and coeff(n,f) the ordinary coefficient of degree n. The source is exp(sum over m>=1 of X^(m^2)/m^m): the exponent is a square and the denominator is a power, not a factorial. Natural division in innerIntegral is expressed by a floor. No analytic convergence or integrality hypothesis is imposed.

Definition 1.1 (The literal inner series).

$$H=\mathrm{PowerSeries}.\mathrm{mk}\left(n\mapsto \mathrm{finsum}\left((m:\mathbb{N})\mapsto \mathrm{ite}\left(0<m,\mathrm{coeff}\left(n,\mathrm{monomial}\left(m^2,\frac{1}{\mathrm{natval}{\left(m\right)}^m}\right)\right),0\right)\right)\right)$$

Formalization. D5/S1/Recurrence/Residue/HannaA226838Congruence.H (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2013). OEIS A226838 — E.g.f.: exp( Sum_{n>=1} x^(n^2) / n^n ).. URL: https://oeis.org/A226838.

Commentary.

This is the coefficientwise finsum over every natural m with the guard 0<m. For each degree n, coeff_H bounds its support by m<=n using le_square. Thus this definition represents the original unbounded positive-index formal sum, rather than a truncated generating function.

Definition 1.2 (The formal exponential).

$$A=\mathrm{PowerSeries}.\mathrm{subst}\left(\mathrm{PowerSeries}.\exp \left(\mathbb{Q}\right),H\right)$$

Formalization. D5/S1/Recurrence/Residue/HannaA226838Congruence.A (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2013). OEIS A226838 — E.g.f.: exp( Sum_{n>=1} x^(n^2) / n^n ).. URL: https://oeis.org/A226838.

Commentary.

The argument order is subst(exp(Q),H), namely substitution of H into exp(Q). The private H_zero supplies constantCoeff(H)=0 before eCoeff_composition is applied.

Definition 1.3 (The derived natural inner coefficients).

$$\forall n:\mathbb{N},\mathrm{innerIntegral}\left(n\right)=\sum _{m=0}^n\mathrm{ite}\left(0<m\wedge m^2=n,\lfloor \frac{n!}{m^m}\rfloor ,0\right)$$

Formalization. D5/S1/Recurrence/Residue/HannaA226838Congruence.innerIntegral (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2013). OEIS A226838 — E.g.f.: exp( Sum_{n>=1} x^(n^2) / n^n ).. URL: https://oeis.org/A226838.

Commentary.

The sum is over range(n+1), hence m=0 through n inclusive; all division here is in Nat. At m>0 and m^2=n, power_dvd_square_factorial gives m^m dividing n!. factorial_ratio uses that divisibility and a nonzero rational denominator to identify the quotient cast with n!/(m:Q)^m. Then eCoeff_H proves that innerIntegral(n), cast to Q, equals n! times coeff(n,H). Integrality is derived, not assumed.

Theorem 1.4 (The congruence for every natural index).

$$\forall n:\mathbb{N},\exists k:\mathbb{Z},\mathrm{natval}\left(n!\right)\cdot \mathrm{coeff}\left(n,A\right)=1+6\cdot \mathrm{val}\left(k\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Residue/HannaA226838Congruence.result (✓ std3). ∎

Resolves. Problems/oeis-a226838-square-egf-mod-six (proved) by D5/S1/Recurrence/Residue/HannaA226838Congruence.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2013). OEIS A226838 — E.g.f.: exp( Sum_{n>=1} x^(n^2) / n^n ).. URL: https://oeis.org/A226838.

Commentary.

OEIS A226838 revision #14 states: a(n) == 1 (mod 6) (conjecture - valid up to n=1024; if true for n>=0, why?). The existential integer witness proves integrality and the residue simultaneously for every n, including zero. For m>=2, six_power_dvd_square_factorial proves 6*m^m divides (m^2)!, treating m=2 and m=3 directly and using product-factorial divisibility for larger m. inner_mod_six therefore reduces the integral inner coefficient sequence to the identity sequence. The result uses eCoeff_H, H_zero, inner_mod_six and composition_unit_mod_six. The existing IntegralEGFComposition.eCoeff_composition, eCoeff_exp and composition_map, together with the original private QuarticEGFModFour.composition_identity_right, transfer that identity through the integral composition law. For m>=2, power_dvd_square_factorial follows from the stronger local six_power_dvd_square_factorial; the remaining positive case m=1 is immediate. The product-factorial step uses Nat.prod_factorial_dvd_factorial_sum. Only integers are reduced to ZMod(6); there is no rational-to-residue-ring map. The proof is repository-derived and is not attributed to OEIS.

References

• Truth anchor: D5/S1/Recurrence/Residue/HannaA226838Congruence.A
• Truth anchor: D5/S1/Recurrence/Residue/HannaA226838Congruence.H
• Truth anchor: D5/S1/Recurrence/Residue/HannaA226838Congruence.innerIntegral
• Truth anchor: D5/S1/Recurrence/Residue/HannaA226838Congruence.result
• Dependency: D5/S1/Recurrence/Residue/QuarticEGFModFour