The OEIS A338632 Modulo-Four Congruence

Abstract

Hanna’s continued-fraction coefficients are two modulo four above degree one.

P. D. Hanna, OEIS A338632 revision 13 (no page), states verbatim: “G.f. A(x) satisfies: 1 = A(x) - x/(A(x) - 3x/(A(x) - 5x/(A(x) - 7x/(A(x) - 9x/(A(x) - …))))), a continued fraction relation.” Its formula line states verbatim: “a(n) = 2 (mod 4) for n > 1 (conjecture).” The formalization reads the relation through finite truncations, where tail(A,j,r) is a rational power series and coeff(n,A) is the degree-n coefficient. The operation smul is scalar multiplication, and val denotes the indicated rational cast.

Definition 1.1 (Finite tails of the continued fraction).

$$\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\forall j\in \mathbb{N},(\mathrm{tail}\left(A,j,0\right)=A)\wedge (\forall r\in \mathbb{N},\mathrm{tail}\left(A,j,r+1\right)=A-\mathrm{smul}\left(2\cdot (\mathrm{val}\left(j\right):\mathbb{Q})+1,X\right)\cdot \mathrm{inv}\left(\mathrm{tail}\left(A,j+1,r\right)\right))$$

Formalization. D5/S1/Recurrence/Invariants/HannaA338632.tail (✓ std3).

Citation. Paul D. Hanna (2026). OEIS A338632, continued-fraction generating function with odd numerators. URL: https://oeis.org/A338632.

Commentary.

For rational PowerSeries A, tail(A,j,0)=A and the successor tail subtracts the odd numerator (2j+1) times X divided by the next tail. The inverse is the formal power-series inverse supplied by the coefficient field.

Definition 1.2 (The coefficientwise continued-fraction relation).

$$\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsGF}\left(A\right)\iff (\forall n\in \mathbb{N},\exists R\in \mathbb{N},\forall r\in \mathbb{N},(R\le r)⟹(\mathrm{coeff}\left(n,\mathrm{tail}\left(A,0,r\right)\right)=\mathrm{coeff}\left(n,1\right)))$$

Formalization. D5/S1/Recurrence/Invariants/HannaA338632.IsGF (✓ std3).

Citation. Paul D. Hanna (2026). OEIS A338632, continued-fraction generating function with odd numerators. URL: https://oeis.org/A338632.

Commentary.

IsGF(A) says that for every degree n, some truncation depth R makes the degree-n coefficient of every later tail(A,0,r) equal to the constant series one.

Definition 1.3 (Hanna’s modulo-four conjecture).

$$(\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))⟹(\forall n\in \mathbb{N},(2\le n)⟹(\exists m\in \mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(\mathrm{val}\left(m\right):\mathbb{Q}))\wedge (m\mathrm{mod}4=2))))$$

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

Citation. Paul D. Hanna (2026). OEIS A338632, continued-fraction generating function with odd numerators. URL: https://oeis.org/A338632.

Commentary.

The claim asserts existence of a series satisfying IsGF and says that every such series has an integer coefficient congruent to two modulo four at each degree n at least two.

Theorem 1.4 (The modulo-four conjecture is proved).

$$(\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))⟹(\forall n\in \mathbb{N},(2\le n)⟹(\exists m\in \mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(\mathrm{val}\left(m\right):\mathbb{Q}))\wedge (m\mathrm{mod}4=2))))$$

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

Resolves. Problems/hanna-a338632-conjecture (proved) by D5/S1/Recurrence/Invariants/HannaA338632.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2026). OEIS A338632, continued-fraction generating function with odd numerators. URL: https://oeis.org/A338632.

Commentary.

The normalized fixed-point construction supplies a series satisfying IsGF. Reduction modulo four makes the odd numerators periodic with period two, giving a quadratic equation. Its normalized root is (1+X^2)/(1-X), whose coefficients from degree two onward are two modulo four.

References

• Truth anchor: D5/S1/Recurrence/Invariants/HannaA338632.IsGF
• Truth anchor: D5/S1/Recurrence/Invariants/HannaA338632.claim
• Truth anchor: D5/S1/Recurrence/Invariants/HannaA338632.result
• Truth anchor: D5/S1/Recurrence/Invariants/HannaA338632.tail
• Dependency: D5/S1/Recurrence/Residue/ContinuedFractionOddSquare