Hanna’s theta-four congruences

Abstract

Hanna’s A379764 theta-four coefficient conjectures.

Paul D. Hanna’s OEIS A379764 states: “G.f. A(x) satisfies Sum_{n=-oo..+oo} (4^nA(x)^n - 4A(x))^(n+1) = 2theta_4(x) = 2Sum_{n=-oo..+oo} (-x)^(n^2).” The same entry states: “Conjecture: for n > 0, a(n) is odd iff n is a square.” It also states: “Conjecture: for n > 0, a(n) == (-1)^(n-1) (mod 4) iff n is a square, otherwise a(n) is divisible by 4 if n is nonsquare.”

PowerSeries and LaurentSeries are formal series over the displayed coefficient rings. The bilateral sum is coefficientwise over the finite interval Icc(-(K:Z), K) with N+1 <= K. The coefficient of theta4 is defined by the same finite symmetric window. Int.ModEq is congruence modulo its first argument; divisibility is in Z.

Theorem 1.1 (Pairing a symmetric integer window).

$$\forall T:\mathrm{Type},[\mathrm{AddCommMonoid}\left(T\right)]\forall f\in \mathbb{Z}\to T,\forall K\in \mathbb{N},\sum _{j:\mathbb{Z}\in \mathrm{Finset}.\mathrm{Icc}\left(-((K:\mathbb{Z})),(K:\mathbb{Z})\right)}(f\left(j\right))=f\left(0\right)+\sum _{k:\mathbb{N}\in \mathrm{Finset}.\mathrm{range}\left(K\right)}(f\left((k:\mathbb{Z})+1\right)+f\left(-((k:\mathbb{Z}))-1\right))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.symmetric_pair (✓ std3). ∎

Source. Repository-derived.

Commentary.

In an additive commutative monoid, a symmetric finite sum is its central term plus the pairs with indices k+1 and -k-1. This decomposition separates the positive and negative summands in the bilateral equations.

Definition 1.2 (The coefficientwise theta-four series).

$$theta4\left(\right)=\mathrm{PowerSeries}.\mathrm{mk}\left((N:\mathbb{N}\mapsto \sum _{n:\mathbb{Z}\in \mathrm{Finset}.\mathrm{Icc}\left(-((N:\mathbb{Z})),(N:\mathbb{Z})\right)}((\mathrm{if}((n{)}^2=(N:\mathbb{Z}))\mathrm{then}(-(1){)}^N\mathrm{else}0)))\right)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.theta4 (✓ std3).

Citation. Paul D. Hanna (2025). OEIS A379764, theta-four bilateral generating function and coefficient congruences. URL: https://oeis.org/A379764.

Commentary.

The coefficient at N sums the terms indexed by integer n in the symmetric interval from -(N:Z) to N.

Definition 1.3 (The Laurent-series summand).

$$\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\forall n\in \mathbb{Z},\mathrm{term}\left(A,n\right)=((4{)}^n\cdot (\mathrm{HahnSeries}.\mathrm{ofPowerSeries}\left(\mathbb{Z},\mathbb{Q},A\right){)}^n-4\cdot \mathrm{HahnSeries}.\mathrm{ofPowerSeries}\left(\mathbb{Z},\mathbb{Q},A\right){)}^{n+1}$$

Formalization. D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.term (✓ std3).

Citation. Paul D. Hanna (2025). OEIS A379764, theta-four bilateral generating function and coefficient congruences. URL: https://oeis.org/A379764.

Commentary.

The integer exponent n is used in LaurentSeries Q after embedding A with HahnSeries.ofPowerSeries.

Definition 1.4 (The normalized generating-function equation).

$$\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))\iff ((\mathrm{constantCoeff}\left(A\right)=0)\wedge ((\mathrm{coeff}\left(1,A\right)=1)\wedge (\forall N\in \mathbb{N},\forall K\in \mathbb{N},(N+1\le K)\Rightarrow (\sum _{j:\mathbb{Z}\in \mathrm{Finset}.\mathrm{Icc}\left(-((K:\mathbb{Z})),(K:\mathbb{Z})\right)}(\mathrm{coeff}\left((N:\mathbb{Z}),\mathrm{term}\left(A,j\right)\right))=2\cdot \mathrm{coeff}\left(N,theta4\left(\right)\right)))))$$

Formalization. D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.IsGF (✓ std3).

Citation. Paul D. Hanna (2025). OEIS A379764, theta-four bilateral generating function and coefficient congruences. URL: https://oeis.org/A379764.

Commentary.

Normalization is constantCoeff A = 0 and coeff 1 A = 1; every coefficient window with N+1 <= K equals twice the theta-four coefficient.

Definition 1.5 (Hanna’s two coefficient conjectures).

$$(\exists A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsGF}\left(A\right))\wedge (\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))\Rightarrow (\forall n\in \mathbb{N},(0<n)\Rightarrow (\exists m\in \mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(m:\mathbb{Q}))\wedge (((\mathrm{Odd}\left(m\right))\iff (\mathrm{IsSquare}\left(n\right)))\wedge (((\mathrm{Int}.\mathrm{ModEq}\left(4,m,(-(1){)}^{n-1}\right))\iff (\mathrm{IsSquare}\left(n\right)))\wedge ((\neg (\mathrm{IsSquare}\left(n\right)))\Rightarrow (4\mid m)))))))$$

Formalization. D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.claim (✓ std3).

Citation. Paul D. Hanna (2025). OEIS A379764, theta-four bilateral generating function and coefficient congruences. URL: https://oeis.org/A379764.

Commentary.

For every normalized solution and every positive n, an integer coefficient witness has the two square biconditionals and the nonsquare divisibility conclusion.

Theorem 1.6 (The two A379764 conjectures).

$$(\exists A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsGF}\left(A\right))\wedge (\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))\Rightarrow (\forall n\in \mathbb{N},(0<n)\Rightarrow (\exists m\in \mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(m:\mathbb{Q}))\wedge (((\mathrm{Odd}\left(m\right))\iff (\mathrm{IsSquare}\left(n\right)))\wedge (((\mathrm{Int}.\mathrm{ModEq}\left(4,m,(-(1){)}^{n-1}\right))\iff (\mathrm{IsSquare}\left(n\right)))\wedge ((\neg (\mathrm{IsSquare}\left(n\right)))\Rightarrow (4\mid m)))))))$$

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

Resolves. Problems/oeis-a379764-hanna-theta-mod-four (proved) by D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2025). OEIS A379764, theta-four bilateral generating function and coefficient congruences. URL: https://oeis.org/A379764.

Commentary.

The integral fixed-point construction gives a normalized solution. Its coefficient congruence is the theta-four source modulo four, and uniqueness identifies every normalized rational solution with it.

References

• Truth anchor: D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.IsGF
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.claim
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.result
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.symmetric_pair
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.term
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaThetaFourModFour.theta4
• Dependency: D5/S1/Recurrence/Bilateral/BilateralProductModFour
• Dependency: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction
• Dependency: D5/S1/Recurrence/Invariants/UnitReversionSquareParity
• Dependency: D5/S1/Recurrence/Parity/BilateralQuarticPowerThetaModFour
• Dependency: D5/S1/Recurrence/Parity/ScaledQuadraticReversionModSixteen