The Fabius function is a smooth monotone function $F:[0,1]\to[0,1]$, satisfying functional equations $$F(0)=0, \quad F(1-x)=1-F(x)\tag1$$ and $$F'(x) = 2 \,F(2 x) \quad \text{for} \,\, 0<x<1/2.\tag2$$

The function $F$ assumes rational values at dyadic rational arguments. In particular, it is known $\!^{[1]}$$\!^{[2]}$ that $$F\left(2^{-n}\right) = 2^{-\frac{n(n+1)}{2}}\left[\frac1{n!}+\sum_{m=1}^{\lfloor n/2\rfloor}\frac{(-1)^m \, c_m}{(n - 2 m)!}\right],\tag3$$ where $$c_m = \frac1{4^m - 1}\left[\frac{(-1)^m}{(2m+1)!}+\sum_{k=1}^{m-1} \frac{(-1)^k \, c_{m-k}}{(2 k + 1)!}\right],\tag4$$ and empty sums are assumed to be zero as usual. The values $F\left(2^{-n}\right) $ appear as A272755/A272757 in the OEIS.

Let $$a_n = F\left(2^{-n}\right) \, 2^{\binom {n-1}2} \, (2n)! \, \prod_{m=1}^n\left(2^m - 1\right)\tag5$$ This sequence appears as A277471 in the OEIS. It looks like all its terms are integers (meaning that the additional factors grow fast enough to cancel all denominators). How can we prove that?