Divisibility at Multiples of Four

Abstract

A roots-of-unity filter collapses the surviving binomial sum, which is the step the two published facts leave open.

Two facts are taken as hypotheses rather than reproved: a finite formula for the even-indexed terms, and the residues of the Euler secant numbers modulo five. Both are published; neither implies the conclusion. What is proved is the implication, so nothing here asserts that a particular sequence satisfies the hypotheses.

Theorem 1.1 (A roots-of-unity filter).

$$\forall n\in \mathbb{N},1\le n\Rightarrow \sum _{j\in \mathrm{range}\left(4\cdot n+1\right)}[j\mathrm{mod}4=2]\mathrm{choose}\left(4\cdot n,j\right)=1(\mathrm{mod}5)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A380056.binomial_residue_two (✓ std3). ∎

Source. Repository-derived.

Commentary.

Two and three have order four modulo five, so the indicator of an index congruent to two modulo four is a combination of four powers. The binomial theorem then turns each power sum into a closed form, and the four closed forms leave one. The finite checks are confined to fixed residue facts and do not range over the index.

Theorem 1.2 (The surviving terms cancel).

$$\forall n\in \mathbb{N},1\le n\Rightarrow \sum _{k\in \mathrm{Icc}\left(1,2\cdot n\right)}[k=2\cdot n\vee \left(2\cdot n-k\right)\mathrm{mod}2=1]\mathrm{choose}\left(4\cdot n,2\cdot k\right)\cdot 4^{2\cdot n-k}=0(\mathrm{mod}5)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A380056.surviving_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reducing by the Euler residues leaves the terms whose Euler index is odd, together with the endpoint. Reindexing sends those to exactly the arguments the filter selects, so their weighted sum is the filtered one, and the endpoint contributes the one that cancels it.

Theorem 1.3 (The conjecture, from the two published facts).

$$\forall a,E:\mathbb{N}\to \mathbb{N},(\forall m,1\le m\Rightarrow a\left(2\cdot m\right)=\sum _{k\in \mathrm{Icc}\left(1,m\right)}\mathrm{choose}\left(2\cdot m,2\cdot k\right)\cdot E\left(m-k\right)\cdot 4^{m-k}\wedge E\left(0\right)=1\wedge \forall r,0<r\Rightarrow E\left(r\right)\mathrm{mod}5=(1\mathrm{if}r\mathrm{mod}2=1,0\mathrm{otherwise}))\Rightarrow \forall n,1\le n\Rightarrow 5\mid a\left(4\cdot n\right)$$

Proof. Machine-checked in Lean as D5/S3/Factorization/A380056.a380056_div_five (✓ std3). ∎

Resolves. Problems/oeis-a380056-fourth-index-divisible-by-five (proved) by D5/S3/Factorization/A380056.a380056_div_five.

Source. Repository-derived.

Acknowledgement. OEIS Foundation Inc. (2025). OEIS A380056. URL: https://oeis.org/A380056.

Commentary.

Substituting the printed formula at twice the index and reducing modulo five leaves the surviving sum, which vanishes. The hypotheses are the literature’s contribution; the cancellation is not among them.

The other conjecture printed on the same entry is untouched, and no claim is made about the generating function itself.

References

• Truth anchor: D5/S3/Factorization/A380056.a380056_div_five
• Truth anchor: D5/S3/Factorization/A380056.binomial_residue_two
• Truth anchor: D5/S3/Factorization/A380056.surviving_sum