Hanna’s product-partition congruence

Abstract

Hanna’s OEIS A356508 product equation and its coefficient residues modulo four.

The source is P. D. Hanna’s OEIS A356508 entry. It states verbatim: G.f. A(x) satisfies: 2 = Product_{n>=1} (1 + x^nA(x)) * (1 + x^(n-1)/A(x)). Its comment conjectures verbatim: a(n) == 2 (mod 4) at n = 2k for all k > 0 that have an odd number of partitions (A052002), otherwise a(n) == 0 (mod 4) when n > 0.

PowerSeries is the formal power-series type, X is its indeterminate, coeff and constantCoeff read coefficients, and invOfUnit is the formal inverse determined by the nonzero constant coefficient. Products are coefficientwise finite windows; Nat.Partition and Fintype.card give the ordinary partition number.

Definition 1.1 (The coefficientwise product equation).

$$\forall A\in \mathrm{PowerSeries}\left(\mathbb{Q}\right),(\mathrm{IsGF}\left(A\right))\iff ((\mathrm{PowerSeries}.\mathrm{constantCoeff}\left(A\right)\ne 0)\wedge (\forall m\in Nat,\mathrm{PowerSeries}.\mathrm{coeff}\left(m,\mathrm{Finset}.\mathrm{prod}\left(\mathrm{Finset}.\mathrm{Icc}\left(1,m+1\right),(n:Nat\mapsto \left(1+(\mathrm{PowerSeries}.X\left(\right){)}^n\cdot A\right)\cdot \left(1+(\mathrm{PowerSeries}.X\left(\right){)}^{n-1}\cdot \mathrm{PowerSeries}.\mathrm{invOfUnit}\left(A,1\right)\right))\right)\right)=\mathrm{PowerSeries}.\mathrm{coeff}\left(m,2\right)))$$

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

Citation. Paul D. Hanna (2022). OEIS A356508, product-partition generating-function congruence. URL: https://oeis.org/A356508.

Commentary.

The displayed predicate is the source generating-function equation over rational formal power series, with each coefficient represented by the finite window through index m+1.

Definition 1.2 (Hanna’s coefficient-residue conjecture).

$$(\mathrm{claim}\left(\right))\iff ((\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))\Rightarrow (\forall n\in Nat,(0<n)\Rightarrow (\exists z\in Int,(\mathrm{PowerSeries}.\mathrm{coeff}\left(n,A\right)=\mathrm{Int}.\mathrm{cast}\left(z\right))\wedge (((\exists k\in Nat,(0<k)\wedge ((n=2\cdot k)\wedge (\mathrm{Odd}\left(\mathrm{Fintype}.\mathrm{card}\left(\mathrm{Nat}.\mathrm{Partition}\left(k\right)\right)\right))))\Rightarrow (\mathrm{Int}.\mathrm{ModEq}\left(4,z,2\right)))\wedge ((\neg (\exists k\in Nat,(0<k)\wedge ((n=2\cdot k)\wedge (\mathrm{Odd}\left(\mathrm{Fintype}.\mathrm{card}\left(\mathrm{Nat}.\mathrm{Partition}\left(k\right)\right)\right)))))\Rightarrow (\mathrm{Int}.\mathrm{ModEq}\left(4,z,0\right))))))))$$

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

Citation. Paul D. Hanna (2022). OEIS A356508, product-partition generating-function congruence. URL: https://oeis.org/A356508.

Commentary.

The displayed proposition includes existence of a rational solution and the source’s integer-coefficient and modulo-four assertions for every positive coefficient.

Theorem 1.3 (The A356508 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))\Rightarrow (\forall n\in Nat,(0<n)\Rightarrow (\exists z\in Int,(\mathrm{PowerSeries}.\mathrm{coeff}\left(n,A\right)=\mathrm{Int}.\mathrm{cast}\left(z\right))\wedge (((\exists k\in Nat,(0<k)\wedge ((n=2\cdot k)\wedge (\mathrm{Odd}\left(\mathrm{Fintype}.\mathrm{card}\left(\mathrm{Nat}.\mathrm{Partition}\left(k\right)\right)\right))))\Rightarrow (\mathrm{Int}.\mathrm{ModEq}\left(4,z,2\right)))\wedge ((\neg (\exists k\in Nat,(0<k)\wedge ((n=2\cdot k)\wedge (\mathrm{Odd}\left(\mathrm{Fintype}.\mathrm{card}\left(\mathrm{Nat}.\mathrm{Partition}\left(k\right)\right)\right)))))\Rightarrow (\mathrm{Int}.\mathrm{ModEq}\left(4,z,0\right)))))))$$

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

Resolves. Problems/oeis-a356508-hanna-product-partition-mod-four (proved) by D5/S1/Recurrence/Invariants/HannaProductPartitionModFour.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2022). OEIS A356508, product-partition generating-function congruence. URL: https://oeis.org/A356508.

Commentary.

Integral coefficient contraction gives the unique solution. Mapping the fixed-point equation to ZMod 4, the candidate 2 times the partition series in X squared minus one squares to one; the paired product therefore reduces to the reciprocal partition identity. Its coefficient formula is 2 times the ordinary partition number at n/2 for even n and zero for odd n, which gives the two residue cases.

References

• Truth anchor: D5/S1/Recurrence/Invariants/HannaProductPartitionModFour.IsGF
• Truth anchor: D5/S1/Recurrence/Invariants/HannaProductPartitionModFour.claim
• Truth anchor: D5/S1/Recurrence/Invariants/HannaProductPartitionModFour.result
• Dependency: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity
• Dependency: D5/S1/Recurrence/Invariants/UnitReversionSquareParity
• Dependency: D5/S1/Recurrence/Parity/BilateralQuarticPowerThetaModFour