Theta Self-Composition Modulo Four

Abstract

The positive coefficients of OEIS A378581 are two modulo four exactly at square degrees.

Paul D. Hanna’s entry hanna2025a378581 defines the integer series A by A(x*A(x))=theta_3(x), where theta_3(x) is one plus twice the sum of x^(j^2) over positive integers j. It conjectures that positive square degrees have coefficient two modulo four and all other positive degrees have coefficient divisible by four.

All indices are natural numbers. PowerSeries(Z) is the ring of integer formal power series, X is its indeterminate, coeff(n,F) extracts a coefficient, and mk constructs a series from its coefficient function. In the formulas subst(F,U) means F(U), with the outer series first. IsSquare(n) means that n is the square of a natural number. The map operation applies its ring homomorphism to every coefficient; all remainders in the final formula are integer remainders.

Definition 1.1 (The formal theta series).

$$\mathrm{thetaSeries}=\mathrm{mk}\left((n:\mathbb{N}\mapsto \mathrm{if}(n=0)\mathrm{then}1\mathrm{else}(\mathrm{if}(\mathrm{IsSquare}\left(n\right))\mathrm{then}2\mathrm{else}0))\right)$$

Formalization. D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.thetaSeries (✓ std3).

Source. Repository-derived.

Commentary.

The coefficient function includes the constant term separately from the positive square degrees.

Theorem 1.2 (The theta coefficients).

$$\forall n:\mathbb{N},\mathrm{coeff}\left(n,\mathrm{thetaSeries}\right)=\mathrm{if}(n=0)\mathrm{then}1\mathrm{else}(\mathrm{if}(\mathrm{IsSquare}\left(n\right))\mathrm{then}2\mathrm{else}0)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.coeff_thetaSeries (✓ std3). ∎

Source. Repository-derived.

Commentary.

Extracting a coefficient from mk gives the defining conditional expression.

Definition 1.3 (The stabilized integer coefficients).

$$\begin{array}{r}\forall n:\mathbb{N},a\left(n\right)=\mathrm{coeff}\left(n,\mathrm{approximation}\left(n+1\right)\right)\\ \mathrm{approximation}\left(0\right)=1\\ \forall d:\mathbb{N},\mathrm{approximation}\left(d+1\right)=(\mathrm{thetaSeries}+\mathrm{approximation}\left(d\right))-\mathrm{subst}\left(\mathrm{approximation}\left(d\right),X\cdot \mathrm{approximation}\left(d\right)\right)\end{array}$$

Formalization. D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.a (✓ std3).

Source. Repository-derived.

Commentary.

The auxiliary approximation starts at one and applies the displayed correction. Each approximation has constant coefficient one. Agreement below degree d improves to agreement below degree d+1, so the diagonal coefficient defines the sequence.

Definition 1.4 (The integer generating series).

$$\mathrm{generatingSeries}=\mathrm{mk}\left(a\right)$$

Formalization. D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.generatingSeries (✓ std3).

Source. Repository-derived.

Commentary.

The generating series has coefficient function a.

Theorem 1.5 (The defining functional equation).

$$(\mathrm{constantCoeff}\left(\mathrm{generatingSeries}\right)=1)\wedge (\mathrm{subst}\left(\mathrm{generatingSeries},X\cdot \mathrm{generatingSeries}\right)=\mathrm{thetaSeries})$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.generating_equation (✓ std3). ∎

Source. Repository-derived.

Commentary.

If F and G agree below degree d and G has constant coefficient one, then at every degree n at most d the difference between F(XF) and G(XG) equals the difference between their degree-n coefficients. The substitution arguments agree through degree d. In the remaining outer difference, lower terms vanish and the degree-n term has multiplier one. The correction therefore contracts coefficient agreement. Its stabilized series is a fixed point, giving the equation.

Theorem 1.6 (Uniqueness of the integer solution).

$$\forall B:\mathrm{PowerSeries}\left(\mathbb{Z}\right),(\mathrm{constantCoeff}\left(B\right)=1)⟹((\mathrm{subst}\left(B,X\cdot B\right)=\mathrm{thetaSeries})⟹(B=\mathrm{generatingSeries}))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.generating_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every solution is a fixed point of the correction. Induction on degree using the same contraction proves equality of all coefficients.

Theorem 1.7 (The full series identity modulo four).

$$\mathrm{map}\left(\mathrm{intCastRingHom}\left(\mathrm{ZMod}\left(4\right)\right),\mathrm{generatingSeries}\right)=\mathrm{map}\left(\mathrm{intCastRingHom}\left(\mathrm{ZMod}\left(4\right)\right),\mathrm{thetaSeries}\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.mod_four_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Write the reduced theta series as R=1+2S. In ZMod(4), twice XR equals twice X. More generally, cU=cV implies cU^k=cV^k by induction on k, and the coefficient formula for substitution then gives cF(U)=cF(V) for zero-constant U and V. Apply this with c=2 to obtain R(X*R)=R. Mapping the integer equation preserves substitution, and uniqueness over ZMod(4) identifies the two series.

Theorem 1.8 (Hanna’s A378581 conjecture).

$$\forall n:\mathbb{N},(0<n)⟹((((a\left(n\right)\mathrm{mod}4=2)⟺(\mathrm{IsSquare}\left(n\right)))\wedge ((a\left(n\right)\mathrm{mod}4=0)⟺(\neg (\mathrm{IsSquare}\left(n\right))))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.hanna_conjecture (✓ std3). ∎

Resolves. Problems/oeis-a378581-theta-self-composition-mod-four (proved) by D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.hanna_conjecture.

Citation. Paul D. Hanna (2025). OEIS A378581, g.f. satisfying A(xA(x)) = theta_3(x)*. URL: https://oeis.org/A378581.

Commentary.

At positive degree, the theta coefficient is two at a square and zero otherwise. The series identity and the integer-cast remainder equivalence give both biconditionals, as conjectured in hanna2025a378581.

References

• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.a
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.coeff_thetaSeries
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.generatingSeries
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.generating_equation
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.generating_unique
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.hanna_conjecture
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.mod_four_identity
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.thetaSeries