Hanna’s power-of-two residue theorem

Abstract

Hanna’s binomial-square generating function has the asserted residues at every coefficient.

Definition 1.1 (The rational summand).

$$\forall n:\mathbb{N},\mathrm{term}\left(n\right)=((\mathrm{PowerSeries}.X{)}^n\cdot ((1-3\cdot \mathrm{PowerSeries}.X{)}^{2\cdot n+1}{)}^{-1}\cdot (\sum _{k\in \mathrm{Finset}.\mathrm{range}\left(n+1\right)}\mathrm{PowerSeries}.C\left(((\mathrm{Nat}.\mathrm{choose}\left(n,k\right):\mathbb{Q}){)}^2\cdot (2{)}^k\right)\cdot (\mathrm{PowerSeries}.X{)}^k)\cdot (\sum _{k\in \mathrm{Finset}.\mathrm{range}\left(n+1\right)}\mathrm{PowerSeries}.C\left(((\mathrm{Nat}.\mathrm{choose}\left(n,k\right):\mathbb{Q}){)}^2\cdot (3{)}^k\right)\cdot (\mathrm{PowerSeries}.X{)}^k):\mathrm{PowerSeries}\left(\mathbb{Q}\right))$$

Formalization. D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.term (✓ std3).

Citation. Paul D. Hanna (2014). OEIS A246056 and A246423, two binomial-square generating functions. URL: https://oeis.org/A246056.

Commentary.

OEIS A246423, unpaginated Name: “G.f.: Sum_{n>=0} x^n / (1-3x)^(2n+1) * [Sum_{k=0..n} C(n,k)^2 * 2^k * x^k] * [Sum_{k=0..n} C(n,k)^2 * 3^k * x^k].” The variable is the formal power-series variable and both sums include indices zero through n.

Definition 1.2 (The generating function).

$$A=\mathrm{PowerSeries}.\mathrm{mk}\left(\mathrm{fun}(m:\mathbb{N})\mapsto \mathrm{PowerSeries}.\mathrm{coeff}\left(m,\sum _{n\in \mathrm{Finset}.\mathrm{range}\left(m+1\right)}\mathrm{term}\left(n\right)\right)\right)$$

Formalization. D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.A (✓ std3).

Citation. Paul D. Hanna (2014). OEIS A246056 and A246423, two binomial-square generating functions. URL: https://oeis.org/A246056.

Commentary.

OEIS A246423, unpaginated Name: “G.f.: Sum_{n>=0} x^n / (1-3x)^(2n+1) * [Sum_{k=0..n} C(n,k)^2 * 2^k * x^k] * [Sum_{k=0..n} C(n,k)^2 * 3^k * x^k].” Its coefficient at m uses n from zero through m, because term n has order at least n.

Definition 1.3 (The residue conjecture).

$$(claim)\iff ((\mathrm{PowerSeries}.\mathrm{coeff}\left(0,A\right)=1)\wedge (\forall n:\mathbb{N},(0<n)\Rightarrow (\exists z:\mathbb{Z},(\mathrm{PowerSeries}.\mathrm{coeff}\left(n,A\right)=(z:\mathbb{Q}))\wedge (((z\equiv 2(\mathrm{mod}4))\iff (\exists k:\mathbb{N},(2\le k)\wedge (n=(2{)}^k)))\wedge ((\neg (\exists k:\mathbb{N},(2\le k)\wedge (n=(2{)}^k)))\Rightarrow (z\equiv 0(\mathrm{mod}4)))))))$$

Formalization. D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.claim (✓ std3).

Citation. Paul D. Hanna (2014). OEIS A246056 and A246423, two binomial-square generating functions. URL: https://oeis.org/A246056.

Commentary.

OEIS A246423, unpaginated Comments: “a(n) == 2 (mod 4) iff n = 2^k for k>=2, and a(n) == 0 (mod 4) elsewhere except at a(0)=1 (conjecture).” The letter n ranges over all natural indices and z is the integer equal to the rational coefficient. The constant coefficient is one and the residue assertion begins at n positive.

Theorem 1.4 (The conjecture holds).

$$(\mathrm{PowerSeries}.\mathrm{coeff}\left(0,A\right)=1)\wedge (\forall n:\mathbb{N},(0<n)\Rightarrow (\exists z:\mathbb{Z},(\mathrm{PowerSeries}.\mathrm{coeff}\left(n,A\right)=(z:\mathbb{Q}))\wedge (((z\equiv 2(\mathrm{mod}4))\iff (\exists k:\mathbb{N},(2\le k)\wedge (n=(2{)}^k)))\wedge ((\neg (\exists k:\mathbb{N},(2\le k)\wedge (n=(2{)}^k)))\Rightarrow (z\equiv 0(\mathrm{mod}4))))))$$

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

Resolves. Problems/hanna-a246423-legendre-central-binomial (proved) by D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2014). OEIS A246056 and A246423, two binomial-square generating functions. URL: https://oeis.org/A246056.

Commentary.

The integer lift allows coefficientwise reduction. The alternating transform plus twice its first moment reduces to powers of two; the first-moment term cancels the degree-two residue.

References

• Truth anchor: D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.A
• Truth anchor: D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.claim
• Truth anchor: D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.result
• Truth anchor: D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialModFour.term
• Dependency: D5/S1/Recurrence/Invariants/HannaLegendreCentralBinomialTransform