Hanna’s Half-Iterate Conjecture Modulo Three

Abstract

The normalized half-iterate of X + 4 X cubed has integral coefficients supported modulo three on powers of three.

PowerSeries denotes formal power series. The indeterminate is X, coeff(n,A) is its degree-n coefficient, and PowerSeries.subst(A,A) is composition. Indices are natural numbers. The integer m in the formulas is cast to the rationals when compared with a rational coefficient; Int.ModEq is integer congruence.

Definition 1.1 (The normalized odd half-iterate).

$$\forall A:\mathrm{PowerSeries}\left(\mathbb{Q}\right),\mathrm{IsGF}\left(A\right)=((\forall n:\mathbb{N},\mathrm{coeff}\left(2\cdot n,A\right)=0)\wedge ((\mathrm{coeff}\left(1,A\right)=1)\wedge (\mathrm{PowerSeries}.\mathrm{subst}\left(A,A\right)=X+4\cdot X^3)))$$

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

Citation. Paul D. Hanna (2005). OEIS A107099, compositional half-iterate of x + 4x^3*. URL: https://oeis.org/A107099.

Commentary.

The unpaginated OEIS A107099 Name states: “G.f. satisfies A(A(x)) = x + 4x^3, where A(x) = Sum_{n>=0} a(n)x^(2n+1).” The Example states: “A(x) = 1x + 2x^3 - 6x^5 + 36x^7 - 266x^9 + 2028x^11 - 13596x^13 +-…” The carrier is PowerSeries over the rationals; the even coefficients vanish and the linear coefficient is one, as in the offset-zero sequence.

Definition 1.2 (The coefficient congruence).

$$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},\exists m:\mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(m:\mathbb{Q}))\wedge ((\neg (\exists k:\mathbb{N},n=3^k))⟹(\mathrm{Int}.\mathrm{ModEq}\left(3,m,0\right))))))$$

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

Citation. Paul D. Hanna (2005). OEIS A107099, compositional half-iterate of x + 4x^3*. URL: https://oeis.org/A107099.

Commentary.

The unpaginated OEIS A107099 Comments state: “Coefficients [x^n] A(x) = 0 (mod 3) except at n = 3^k (conjecture).” Existence is asserted, and every IsGF series has integer coefficients. The exponent n ranges over all natural numbers. No nonvanishing assertion at powers of three is included.

Theorem 1.3 (Uniqueness of normalized compositional square roots).

$$\forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)][\mathrm{NoZeroDivisors}\left(R\right)],((2:R)\ne 0)⟹(\forall f:\mathrm{PowerSeries}\left(R\right),\forall g:\mathrm{PowerSeries}\left(R\right),\forall t:\mathrm{PowerSeries}\left(R\right),(\mathrm{constantCoeff}\left(f\right)=0)⟹((\mathrm{constantCoeff}\left(g\right)=0)⟹((\mathrm{coeff}\left(1,f\right)=1)⟹((\mathrm{coeff}\left(1,g\right)=1)⟹((\mathrm{PowerSeries}.\mathrm{subst}\left(f,f\right)=t)⟹((\mathrm{PowerSeries}.\mathrm{subst}\left(g,g\right)=t)⟹(f=g)))))))$$

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

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2005). OEIS A107099, compositional half-iterate of x + 4x^3*. URL: https://oeis.org/A107099.

Commentary.

Over a commutative ring with no zero divisors in which two is nonzero, two series with zero constant coefficient and linear coefficient one are equal whenever their compositional squares equal the same series.

Theorem 1.4 (Integrality and the congruence at every degree).

$$(\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},\exists m:\mathbb{Z},(\mathrm{coeff}\left(n,A\right)=(m:\mathbb{Q}))\wedge ((\neg (\exists k:\mathbb{N},n=3^k))⟹(\mathrm{Int}.\mathrm{ModEq}\left(3,m,0\right)))))$$

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

Resolves. Problems/hanna-a107099-half-iterate-mod-three (proved) by D5/S1/Recurrence/Invariants/HannaHalfIterateCubicModThree.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2005). OEIS A107099, compositional half-iterate of x + 4x^3*. URL: https://oeis.org/A107099.

Commentary.

Correct successive degrees of an integer series beginning with X. A series of the form X + 2B has compositional residual divisible by four, so each correction is even. The compatible coefficients define an integral solution. The degree-n change in the compositional square is twice the degree-n change in the series, proving uniqueness by induction. Reflection through minus X then proves oddness. Over ZMod(3), Frobenius preserves support on powers of three, and substitution preserves this support as well. Strong induction compares the solution with its truncation and forces every other coefficient to vanish. Rational uniqueness transfers these integer coefficients to every IsGF series.

References

• Truth anchor: D5/S1/Recurrence/Invariants/HannaHalfIterateCubicModThree.IsGF
• Truth anchor: D5/S1/Recurrence/Invariants/HannaHalfIterateCubicModThree.claim
• Truth anchor: D5/S1/Recurrence/Invariants/HannaHalfIterateCubicModThree.half_unique
• Truth anchor: D5/S1/Recurrence/Invariants/HannaHalfIterateCubicModThree.result
• Dependency: D5/S1/Recurrence/Invariants/CubicFifteenSubstitutionParity
• Dependency: D5/S1/Recurrence/Residue/CompositionalSquareDyadicDenominators