Hanna’s OEIS 386657 congruence

Abstract

Integrality and a period-six congruence for Hanna’s Lambert W exponential coefficients.

Definition 1.1 (OEIS A386657).

$$\forall m:\mathbb{N},a\left(m\right)=\mathrm{egf}\left(4,m\right)$$

Formalization. D5/S3/Combinatorics/HannaLambertW/OeisA386657LambertWEgfModSix.a (✓ std3).

Citation. Paul D. Hanna (2025). OEIS A386655–A386658, Lambert W exponential generating functions. URL: https://oeis.org/A386655.

Commentary.

The entry NAME reads verbatim: E.g.f.: Sum_{n>=0} (4^n*x + LambertW(x))^n / n!. Here egf is the rational coefficient function of OeisA386655LambertWEgfModSix.

Definition 1.2 (The proposed six-term pattern).

$$\mathrm{claim}=(\forall n:\mathbb{N},(6\le n)⟹(\exists z:\mathbb{Z},((z:\mathbb{Q})=a\left(n\right))\wedge (z\mathrm{mod}6=\mathrm{getD}\left([1,2,3,2,3,4],(n-6)\mathrm{mod}6,0\right))))$$

Formalization. D5/S3/Combinatorics/HannaLambertW/OeisA386657LambertWEgfModSix.claim (✓ std3).

Citation. Paul D. Hanna (2025). OEIS A386655–A386658, Lambert W exponential generating functions. URL: https://oeis.org/A386655.

Commentary.

Conjecture: for n >= 6, a(n) (mod 6) equals [1, 2, 3, 2, 3, 4] repeating. This is the COMMENTS sentence of OEIS A386657 (unpaginated). The integer z has rational cast a(n); getD uses the zero-based index (n-6) mod 6 and default zero. Both remainder operations and natural subtraction are Lean integer or natural operations, respectively.

Theorem 1.3 (Hanna’s congruence).

$$\forall n:\mathbb{N},(6\le n)⟹(\exists z:\mathbb{Z},((z:\mathbb{Q})=a\left(n\right))\wedge (z\mathrm{mod}6=\mathrm{getD}\left([1,2,3,2,3,4],(n-6)\mathrm{mod}6,0\right)))$$

Proof. Machine-checked in Lean as D5/S3/Combinatorics/HannaLambertW/OeisA386657LambertWEgfModSix.result (✓ std3). ∎

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2025). OEIS A386655–A386658, Lambert W exponential generating functions. URL: https://oeis.org/A386655.

Commentary.

The integral closed form and its six-term periodicity reduce the assertion to the six indices from six through eleven, which give the displayed pattern.

References

• Truth anchor: D5/S3/Combinatorics/HannaLambertW/OeisA386657LambertWEgfModSix.a
• Truth anchor: D5/S3/Combinatorics/HannaLambertW/OeisA386657LambertWEgfModSix.claim
• Truth anchor: D5/S3/Combinatorics/HannaLambertW/OeisA386657LambertWEgfModSix.result
• Dependency: D5/S3/Combinatorics/HannaLambertW/OeisA386655LambertWEgfModSix