Hanna’s pentagonal partition parity

Abstract

The literal pentagonal unit equation and Hanna’s ordinary-partition parity assertion.

Paul D. Hanna’s OEIS A361552 defines an integral formal unit A by 2x = sum over every integer k of x^(k(3k+1)/2) times (A^(3k)-A^(-(3*k+1))). The conjecture states that for every integer n at least one its coefficient is even, and its integer half has the parity of the ordinary partitions of n-1.

PowerSeries denotes formal series, X its variable, and the superscript unit group makes all negative powers defined. A coefficient window is an interval of integer summation indices. The topology is the product topology of coefficients; no analytic convergence is involved. The symbol val is Units.val, unit(F,G) is the unit with value F and inverse G after its two inverse laws have been supplied, mk builds a series from its coefficients, intCast casts a natural number to the integers, and ediv is integer division. NatPartition is Nat.Partition and card is Fintype.card. Integer coefficient division and remainder occur only after evenness has been proved.

Definition 1.1 (The exact pentagonal exponent).

$$\forall k:\mathbb{Z},\mathrm{exponent}\left(k\right)=\mathrm{pentagonal}\left(-(k)\right)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.exponent (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

Mathlib’s pentagonal number at -k is k*(3*k+1)/2. Its exact multiplication-by-two identity proves integrality; the natural value is nonnegative and is at least the absolute value of k.

Definition 1.2 (The complete integer-index summand).

$$\forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(R\right)\right),\forall k:\mathbb{Z},\mathrm{term}\left(A,k\right)=((X{)}^{\mathrm{exponent}\left(k\right)})\cdot ((\mathrm{val}\left((A{)}^{(3)\cdot (k)}\right))-(\mathrm{val}\left((A{)}^{-(((3)\cdot (k))+(1))}\right)))$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.term (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

Both powers are powers of the same integral unit. The exponent bound forces each monomial separately to vanish at degree N outside [-N,N].

Definition 1.3 (The full sum by coefficient windows).

$$\forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(R\right)\right),\mathrm{bilateral}\left(A\right)=\mathrm{mk}\left((n:\mathbb{N}\mapsto \sum _{k\in \mathrm{Icc}\left(-(\mathrm{intCast}\left(n\right)),\mathrm{intCast}\left(n\right)\right)}(\mathrm{coeff}\left(n,\mathrm{term}\left(A,k\right)\right)))\right)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.bilateral (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

At each degree this window contains every possibly nonzero integer summand. The HasSum clause below identifies it with the entire bilateral sum.

Definition 1.4 (The original equation).

$$\forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(R\right)\right),\mathrm{Original}\left(A\right)⟺\mathrm{bilateral}\left(A\right)=(2)\cdot (X)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.Original (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

The equation imposes no initial constant coefficient. Its degree-zero term is 1-A inverse, forcing that coefficient to be one.

Definition 1.5 (The constructed integral series).

$$\begin{array}{r}\forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(R\right)\right),\mathrm{nonzeroSum}\left(A\right)=\mathrm{mk}\left((n:\mathbb{N}\mapsto \sum _{k\in \mathrm{erase}\left(\mathrm{Icc}\left(-(\mathrm{intCast}\left(n\right)),\mathrm{intCast}\left(n\right)\right),0\right)}(\mathrm{coeff}\left(n,\mathrm{term}\left(A,k\right)\right)))\right)\\ \forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\mathrm{approximation}\left(R,0\right)=1\\ \forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall d:\mathbb{N},\mathrm{approximation}\left(R,(d)+(1)\right)=\mathrm{step}\left(\mathrm{approximation}\left(R,d\right)\right)\\ \forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(R\right)\right),\mathrm{step}\left(A\right)=\mathrm{unit}\left(\mathrm{invOfUnit}\left(((1)-((2)\cdot (X)))+(\mathrm{nonzeroSum}\left(A\right)),1\right),((1)-((2)\cdot (X)))+(\mathrm{nonzeroSum}\left(A\right))\right)\\ \forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\mathrm{generatingSeries}\left(R\right)=\mathrm{mk}\left((n:\mathbb{N}\mapsto \mathrm{coeff}\left(n,\mathrm{val}\left(\mathrm{approximation}\left(R,(n)+(1)\right)\right)\right))\right)\end{array}$$

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

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

Remove the zero-index term and call the rest S(A). The iteration sends a unit A to the reciprocal of 1-2*X+S(A), whose constant coefficient is one. Agreement through degree d-1 improves through degree d. The nth coefficient is read after n+1 iterations starting at the unit one. Stabilization proves the original equation and equality with every other original unit solution.

Definition 1.6 (The inhabited unit solution).

$$\forall R:\mathrm{Type},[\mathrm{CommRing}\left(R\right)]\mathrm{generatingUnit}\left(R\right)=\mathrm{unit}\left(\mathrm{generatingSeries}\left(R\right),\mathrm{invOfUnit}\left(\mathrm{generatingSeries}\left(R\right),1\right)\right)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.generatingUnit (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

The constructed series has constant coefficient one. Its inverse is the formal invOfUnit at that constant unit; both inverse laws are kernel proofs.

Definition 1.7 (Ordinary partitions).

$$\forall n:\mathbb{N},\mathrm{partitionCount}\left(n\right)=\mathrm{card}\left(\mathrm{NatPartition}\left(n\right)\right)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.partitionCount (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

Nat.Partition n consists of ordinary positive-part partitions of n. Its cardinality at zero is one.

Definition 1.8 (The partition generating function).

$$\mathrm{partitionSeries}=\mathrm{mk}\left((n:\mathbb{N}\mapsto \mathrm{intCast}\left(\mathrm{partitionCount}\left(n\right)\right))\right)$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.partitionSeries (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

The coefficients are these ordinary cardinalities cast to integers. The product supplier Nat.Partition.hasProd_powerSeriesMk_card_restricted is applied at predicate True. Euler’s pentagonal product and the geometric-factor inverse prove that this series is the reciprocal of pentagonalSeries over the integers.

Definition 1.9 (The integer-index coefficients).

$$\forall n:\mathbb{Z},a\left(n\right)=\mathrm{ifThenElse}\left(0\le n,\mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{generatingSeries}\left(\mathbb{Z}\right)\right),0\right)$$

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

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

At a nonnegative integer n this reads the coefficient at n.toNat. Negative indices are zero; the stated parity range starts at one.

Definition 1.10 (All clauses of the original-domain assertion).

$$\mathrm{LiteralResolution}⟺((\forall k:\mathbb{Z},(\mathrm{intCast}\left(\mathrm{exponent}\left(k\right)\right)=\mathrm{ediv}\left((k)\cdot (((3)\cdot (k))+(1)),2\right))\wedge ((0\le \mathrm{intCast}\left(\mathrm{exponent}\left(k\right)\right))\wedge ((2)\cdot (\mathrm{intCast}\left(\mathrm{exponent}\left(k\right)\right))=(k)\cdot (((3)\cdot (k))+(1)))))\wedge ((\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(\mathbb{Z}\right)\right),\forall N:\mathbb{N},\forall k:\mathbb{Z},(\neg (k\in \mathrm{Icc}\left(-(\mathrm{intCast}\left(N\right)),\mathrm{intCast}\left(N\right)\right)))⟹((\mathrm{coeff}\left(N,((X{)}^{\mathrm{exponent}\left(k\right)})\cdot (\mathrm{val}\left((A{)}^{(3)\cdot (k)}\right))\right)=0)\wedge (\mathrm{coeff}\left(N,((X{)}^{\mathrm{exponent}\left(k\right)})\cdot (\mathrm{val}\left((A{)}^{-(((3)\cdot (k))+(1))}\right))\right)=0)))\wedge ((\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(\mathbb{Z}\right)\right),\mathrm{HasSum}\left((k:\mathbb{Z}\mapsto \mathrm{term}\left(A,k\right)),\mathrm{bilateral}\left(A\right)\right))\wedge ((\mathrm{Original}\left(\mathrm{generatingUnit}\left(\mathbb{Z}\right)\right))\wedge ((\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(\mathbb{Z}\right)\right),(\mathrm{Original}\left(A\right))⟹((\mathrm{constantCoeff}\left(\mathrm{val}\left(A\right)\right)=1)\wedge ((A=\mathrm{generatingUnit}\left(\mathbb{Z}\right))\wedge (\forall n:\mathbb{Z},(1\le n)⟹((2\mid \mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{val}\left(A\right)\right))\wedge (\mathrm{ediv}\left(\mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{val}\left(A\right)\right),2\right)\mathrm{mod}2=\mathrm{intCast}\left(\mathrm{partitionCount}\left(\mathrm{toNat}\left((n)-(1)\right)\right)\right)\mathrm{mod}2))))))\wedge ((\mathrm{partitionCount}\left(0\right)=1)\wedge (\forall n:\mathbb{Z},(0\le n)⟹(a\left(n\right)=\mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{generatingSeries}\left(\mathbb{Z}\right)\right)))))))))$$

Formalization. D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.LiteralResolution (✓ std3).

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

The clauses give exponent validity, local finiteness of both monomials, the whole bilateral HasSum, integral unit existence, forced constant coefficient one, uniqueness among every original unit solution, all positive integer indices, the unique empty partition, and the signed-index correspondence.

Theorem 1.11 (The literal partition-parity assertion).

$$(\forall k:\mathbb{Z},(\mathrm{intCast}\left(\mathrm{exponent}\left(k\right)\right)=\mathrm{ediv}\left((k)\cdot (((3)\cdot (k))+(1)),2\right))\wedge ((0\le \mathrm{intCast}\left(\mathrm{exponent}\left(k\right)\right))\wedge ((2)\cdot (\mathrm{intCast}\left(\mathrm{exponent}\left(k\right)\right))=(k)\cdot (((3)\cdot (k))+(1)))))\wedge ((\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(\mathbb{Z}\right)\right),\forall N:\mathbb{N},\forall k:\mathbb{Z},(\neg (k\in \mathrm{Icc}\left(-(\mathrm{intCast}\left(N\right)),\mathrm{intCast}\left(N\right)\right)))⟹((\mathrm{coeff}\left(N,((X{)}^{\mathrm{exponent}\left(k\right)})\cdot (\mathrm{val}\left((A{)}^{(3)\cdot (k)}\right))\right)=0)\wedge (\mathrm{coeff}\left(N,((X{)}^{\mathrm{exponent}\left(k\right)})\cdot (\mathrm{val}\left((A{)}^{-(((3)\cdot (k))+(1))}\right))\right)=0)))\wedge ((\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(\mathbb{Z}\right)\right),\mathrm{HasSum}\left((k:\mathbb{Z}\mapsto \mathrm{term}\left(A,k\right)),\mathrm{bilateral}\left(A\right)\right))\wedge ((\mathrm{Original}\left(\mathrm{generatingUnit}\left(\mathbb{Z}\right)\right))\wedge ((\forall A:\mathrm{Units}\left(\mathrm{PowerSeries}\left(\mathbb{Z}\right)\right),(\mathrm{Original}\left(A\right))⟹((\mathrm{constantCoeff}\left(\mathrm{val}\left(A\right)\right)=1)\wedge ((A=\mathrm{generatingUnit}\left(\mathbb{Z}\right))\wedge (\forall n:\mathbb{Z},(1\le n)⟹((2\mid \mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{val}\left(A\right)\right))\wedge (\mathrm{ediv}\left(\mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{val}\left(A\right)\right),2\right)\mathrm{mod}2=\mathrm{intCast}\left(\mathrm{partitionCount}\left(\mathrm{toNat}\left((n)-(1)\right)\right)\right)\mathrm{mod}2))))))\wedge ((\mathrm{partitionCount}\left(0\right)=1)\wedge (\forall n:\mathbb{Z},(0\le n)⟹(a\left(n\right)=\mathrm{coeff}\left(\mathrm{toNat}\left(n\right),\mathrm{generatingSeries}\left(\mathbb{Z}\right)\right))))))))$$

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

Resolves. Problems/oeis-a361552-literal-partition-parity (proved) by D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.result.

Source. Repository-derived.

Acknowledgement. Paul D. Hanna (2023). OEIS A361552: implicit pentagonal unit series and partition parity. URL: https://oeis.org/A361552.

Commentary.

Map the original unit equation to characteristic two and use uniqueness to obtain A=1 there. Thus A=1+2B with integral B defined by exact coefficient division. In characteristic four this unit squares to one. Reducing integer powers modulo two and multiplying Euler signs by two gives 2(BpentagonalSeries-X)=0 modulo four. Coefficientwise integer divisibility 4 divides 2c implies 2 divides c; no nonunit cancellation is made in characteristic four. The ordinary-partition reciprocal then gives B=X*partitionSeries modulo two. The identity n.toNat=(n-1).toNat+1 for n at least one completes the integer-index coefficient statement.

References

• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.LiteralResolution
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.Original
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.a
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.bilateral
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.exponent
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.generatingSeries
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.generatingUnit
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.partitionCount
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.partitionSeries
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.result
• Truth anchor: D5/S1/Recurrence/Bilateral/HannaPentagonalPartitionParity.term