Hanna’s A377100 mod-three conjecture

Abstract

The normalized generating equation has an integral solution, and every positive coefficient of every normalized solution is one modulo three.

Definition 1.1 (The normalized generating equation).

$$\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))⟺((\mathrm{constantCoeff}\left(A\right)=0)\wedge ((\mathrm{coeff}\left(1,A\right)=1)\wedge ((A:\mathrm{LaurentSeries}\left(\mathbb{Q}\right))=(\frac{(\mathrm{subst}\left((X{)}^3,A\right):\mathrm{LaurentSeries}\left(\mathbb{Q}\right))}{(\mathrm{subst}\left((X{)}^2,A\right):\mathrm{LaurentSeries}\left(\mathbb{Q}\right))})+(((A:\mathrm{LaurentSeries}\left(\mathbb{Q}\right)){)}^2))))$$

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

Citation. Paul D. Hanna (2024). OEIS A377100, a generating-function coefficient conjecture. URL: https://oeis.org/A377100.

Commentary.

OEIS A377100, Name (unpaginated): “G.f. A(x) satisfies A(x) = A(x^3)/A(x^2) + A(x)^2.” The series has rational coefficients, constant coefficient zero and coefficient one at X. The quotient is taken in LaurentSeries Q.

Definition 1.2 (Hanna’s coefficient conjecture).

$$(\mathrm{claim})⟺((\exists A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsGF}\left(A\right))\wedge (\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))⟹(\forall n:\mathbb{N},(1\le n)⟹(\exists m:\mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(m:\mathbb{Q}))\wedge (\mathrm{Int}.\mathrm{ModEq}\left(3,m,1\right))))))$$

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

Citation. Paul D. Hanna (2024). OEIS A377100, a generating-function coefficient conjecture. URL: https://oeis.org/A377100.

Commentary.

OEIS A377100, Comments (unpaginated): “Conjecture: a(n) == 1 (mod 3) for n >= 1, which has been verified for the initial 2305 terms.” Here a(n) is coeff n A, n starts at one, and the integer m is coerced into Q in the coefficient equality. The proposition also asserts existence.

Theorem 1.3 (Every positive coefficient is one modulo three).

$$(\exists A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsGF}\left(A\right))\wedge (\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))⟹(\forall n:\mathbb{N},(1\le n)⟹(\exists m:\mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(m:\mathbb{Q}))\wedge (\mathrm{Int}.\mathrm{ModEq}\left(3,m,1\right)))))$$

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

Resolves. Problems/hanna-a377100-mod-three (proved) by D5/S1/Recurrence/Invariants/HannaCubeSquareQuotientModThree.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2024). OEIS A377100, a generating-function coefficient conjecture. URL: https://oeis.org/A377100.

Commentary.

Writing the solution as X times a normalized series gives a coefficient contraction over every commutative ring. The integral fixed point reduces to the geometric series over ZMod 3. Injectivity into Laurent series identifies the polynomial equation with the displayed quotient.

References

• Truth anchor: D5/S1/Recurrence/Invariants/HannaCubeSquareQuotientModThree.IsGF
• Truth anchor: D5/S1/Recurrence/Invariants/HannaCubeSquareQuotientModThree.claim
• Truth anchor: D5/S1/Recurrence/Invariants/HannaCubeSquareQuotientModThree.result
• Dependency: D5/S1/Recurrence/Invariants/AbsoluteReciprocalGeometricParity
• Dependency: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction
• Dependency: D5/S1/Recurrence/Invariants/ScaledReversionCongruence
• Dependency: D5/S1/Recurrence/Invariants/UnitReversionSquareParity