Bilateral Quarter-Double-Shift Theta Congruence

Abstract

The integer solution of the A363184 bilateral equation is theta_3(x^2) modulo four.

Paul D. Hanna’s entry hanna2023a363184, dated May 20, 2023, defines A by 4 = sum over integer n of (-1)^nx^n(4A(x)+x^(2n-1))^(n+1). It conjectures the theta_3(x^2) congruence and the doubled-square classification of the positive coefficients modulo four.

The terms at n=0 and n=-1 contain opposite Laurent monomials x^(-1) and -x^(-1). They cancel, leaving 4*A and zero respectively. For n=-m-2 with m natural, factoring the negative power gives the displayed negativeTerm. The formal equation below uses exact finite coefficient windows; it does not assert a bilateral infinite-sum operation on formal power series.

All series are over the integers unless mapped to ZMod(4). The indices m, n in a(n), N, and d are natural; the index n in bilateralTerm is an integer. The function toNat sends negative integers to zero. Subtraction after toNat is natural truncated subtraction; the window endpoints and -n-2 use integer arithmetic. The operations div and mod are integer division and remainder on the integers; on natural-number arguments, as in n div 2, they are natural division and remainder. The operator mk builds a series from coefficients, and invOfUnit is the formal unit inverse. The symbols positiveTerm, negativeTerm, R, and P below are the private auxiliary definitions.

The imported thetaSeries and its coefficient formula are from D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.thetaSeries and D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.coeff_thetaSeries. Its constant coefficient is one, and each positive square coefficient is two; all other coefficients are zero. The operator expand(2,thetaSeries) replaces X by X^2, so its positive support consists exactly of n=2*k^2 with k>0.

Definition 1.1 (The reindexed bilateral terms).

$$\begin{array}{r}\forall A:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\forall n:\mathbb{Z},\mathrm{bilateralTerm}\left(A,n\right)=(\mathrm{if}(n=0)\mathrm{then}(4)\cdot (A)\mathrm{else}(\mathrm{if}(n=-(1))\mathrm{then}0\mathrm{else}(\mathrm{if}(0<n)\mathrm{then}\mathrm{positiveTerm}\left(A,\mathrm{toNat}\left(n\right)-(1)\right)\mathrm{else}\mathrm{negativeTerm}\left(A,\mathrm{toNat}\left(-(n)-(2)\right)\right))))\\ \forall A:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\forall m:\mathbb{N},\mathrm{positiveTerm}\left(A,m\right)=(((-(1){)}^{m+1})\cdot ((X{)}^{m+1}))\cdot (((4)\cdot (A)+(X{)}^{(2)\cdot (m)+1}{)}^{m+2})\\ \forall A:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\forall m:\mathbb{N},\mathrm{negativeTerm}\left(A,m\right)=(((-(1){)}^{m+2})\cdot ((X{)}^{(2)\cdot ((m{)}^2)+(6)\cdot (m)+3}))\cdot ((\mathrm{invOfUnit}\left(1+((4)\cdot (A))\cdot ((X{)}^{(2)\cdot (m)+5}),1\right){)}^{m+1})\end{array}$$

Formalization. D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.bilateralTerm (✓ std3).

Source. Repository-derived.

Commentary.

Positive index m+1 and negative index -m-2 use nonnegative exponents and an inverse whose constant coefficient is one.

Theorem 1.2 (Exact finite windows).

$$\forall A:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\forall N:\mathbb{N},\forall n:\mathbb{Z},((n<-(N)-(2))\vee (N<n))⟹(\mathrm{coeff}\left(N,\mathrm{bilateralTerm}\left(A,n\right)\right)=0)$$

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

Source. Repository-derived.

Commentary.

Both terms indexed by m contain at least X^(m+1). Every integer index outside [-N-2,N] therefore has zero coefficient at degree N.

Definition 1.3 (The stabilized integer coefficients).

$$\begin{array}{r}\forall n:\mathbb{N},a\left(n\right)=\mathrm{coeff}\left(n,P\left(n+1\right)\right)\\ P\left(0\right)=1\\ \forall d:\mathbb{N},P\left(d+1\right)=1-(\mathrm{mk}\left((N:\mathbb{N}\mapsto \mathrm{div}\left(\mathrm{coeff}\left(N,R\left(P\left(d\right)\right)\right),4\right))\right))\\ \forall B:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\forall N:\mathbb{N},\mathrm{coeff}\left(N,R\left(B\right)\right)=\sum _{m\in \mathrm{range}\left(N+1\right)}(\mathrm{coeff}\left(N,\mathrm{positiveTerm}\left(B,m\right)+\mathrm{negativeTerm}\left(B,m\right)\right))\end{array}$$

Formalization. D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.a (✓ std3).

Source. Repository-derived.

Commentary.

Each positive-negative pair vanishes at A=0. Differences of powers and the unit-inverse difference identity show that every pair is divisible by four. Thus the displayed division is exact over the integers. Agreement below degree d improves to agreement below degree d+1 under the iteration, so the selected coefficients stabilize.

Definition 1.4 (The integer generating series).

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

Formalization. D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.generatingSeries (✓ std3).

Source. Repository-derived.

Commentary.

The coefficient function of generatingSeries is a.

Theorem 1.5 (The defining bilateral equation).

$$(\mathrm{constantCoeff}\left(\mathrm{generatingSeries}\right)=1)\wedge (\forall N:\mathbb{N},\mathrm{coeff}\left(N,4\right)=\mathrm{coeff}\left(N,\sum _{n\in \mathrm{Icc}\left(-(N)-(2),N\right)}(\mathrm{bilateralTerm}\left(\mathrm{generatingSeries},n\right))\right))$$

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

Source. Repository-derived.

Commentary.

The stabilized series is fixed by the integral iteration. Rejoining the pairs restores the finite integer window. Its extra positive endpoint has zero coefficient, and the index-zero term gives 4*A.

Theorem 1.6 (Uniqueness of the solution).

$$\forall B:\mathrm{PowerSeries}\left(\mathbb{Z}\right),(\mathrm{constantCoeff}\left(B\right)=1)⟹((\forall N:\mathbb{N},\mathrm{coeff}\left(N,4\right)=\mathrm{coeff}\left(N,\sum _{n\in \mathrm{Icc}\left(-(N)-(2),N\right)}(\mathrm{bilateralTerm}\left(B,n\right))\right))⟹(B=\mathrm{generatingSeries}))$$

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

Source. Repository-derived.

Commentary.

Every series satisfying the same finite-window equation is fixed by the iteration. Degree contraction proves equality at every coefficient.

Theorem 1.7 (The constant coefficient).

$$a\left(0\right)=1$$

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

Source. Repository-derived.

Commentary.

Every paired term has positive order, so the iteration has constant coefficient one.

Theorem 1.8 (Cancellation over the integers).

$$\exists Q:\mathrm{PowerSeries}\left(\mathbb{Z}\right),1=(\mathrm{generatingSeries})\cdot (\mathrm{expand}\left(2,\mathrm{thetaSeries}\right))+(4)\cdot (Q)$$

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

Source. Repository-derived.

Commentary.

Modulo sixteen, (4A)^2 vanishes. Expanding each pair leaves its linear terms, whose weighted finite sum telescopes to eight times A times the positive doubled-square support series. Multiplication by eight removes the alternating signs modulo sixteen. Hence the difference between the remainder and 4A*(expand(2,thetaSeries)-1) is 16Q with integral Q. The generating equation gives 4=4(Aexpand(2,thetaSeries)+4Q); cancelling the nonzero factor four in the integer series ring gives the statement.

Theorem 1.9 (The series congruence).

$$\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{expand}\left(2,\mathrm{thetaSeries}\right)\right)$$

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

Source. Repository-derived.

Commentary.

The reduction of expand(2,thetaSeries) is 1+2*S, where S indicates the positive doubled squares. Its square is one over ZMod(4). Reducing the integer cancellation identity and multiplying by this self-inverse series identifies the reduction of generatingSeries.

Theorem 1.10 (Hanna’s A363184 conjecture).

$$\forall n:\mathbb{N},(1\le n)⟹((((a\left(n\right)\mathrm{mod}4=2)⟺((\exists k:\mathbb{N},(0<k)\wedge (n=(2)\cdot ((k{)}^2)))))\wedge ((a\left(n\right)\mathrm{mod}4=0)⟺(\neg ((\exists k:\mathbb{N},(0<k)\wedge (n=(2)\cdot ((k{)}^2))))))))$$

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

Resolves. Problems/oeis-a363184-bilateral-quarter-double-shift-theta-mod-four (proved) by D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.hanna_conjecture.

Citation. Paul D. Hanna (2023). OEIS A363184, g.f. satisfying 4 = Sum_{n in Z} (-1)^n x^n (4 A(x) + x^(2n-1))^(n+1). URL: https://oeis.org/A363184.

Commentary.

At a positive index, the expanded theta coefficient is two exactly at n=2*k^2 for k>0 and zero otherwise. Coefficient comparison and the integer-cast remainder equivalence prove both biconditionals in hanna2023a363184.

Theorem 1.11 (The nonsquare floor corollary).

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

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

Source. Repository-derived.

Commentary.

If n=2*k^2 with k>0, natural division gives n div 2=k^2. Thus a nonsquare floor excludes every doubled square, and the zero biconditional gives the conclusion.

References

• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.a
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.a_zero
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.bilateralTerm
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.bilateralTerm_coeff_eq_zero
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.cancellation_identity
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.generatingSeries
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.generating_equation
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.generating_unique
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.hanna_conjecture
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.hanna_conjecture_floor
• Truth anchor: D5/S1/Recurrence/Bilateral/BilateralQuarterDoubleShiftThetaModFour.mod_four_identity
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.coeff_thetaSeries
• Truth anchor: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour.thetaSeries
• Dependency: D5/S1/Recurrence/Parity/ThetaSelfCompositionModFour