Absolute Reciprocal Cubes and Binomial Parity

Abstract

The coefficients of OEIS A380709 have Hanna’s conjectured binomial parity.

The generating equation and conjecture are recorded in hanna2025a380709. Write A for generatingSeries. The series A, B, F, and P(r) have integer coefficients, X is the indeterminate, and n and r are natural numbers. The auxiliary series Q and H used in the proof have coefficients in ZMod(2).

The operator mk forms a power series from its coefficient function, coeff(n,F) extracts its degree-n coefficient, and abs is integer absolute value. The operator invOfUnit(F,1) is Mathlib’s power-series inverse with unit parameter 1. The operator map applies a ring homomorphism coefficientwise; intCast(ZMod(2)) denotes Int.castRingHom(ZMod(2)). The operator choose is Nat.choose, with natural subtraction in its upper index. The operator ofNat denotes Int.ofNat and embeds a natural number into the integers, while zmodCast embeds it into ZMod(2). Remainders in lucas_recursion_q are natural remainders; those in hanna_conjecture are integer remainders.

Definition 1.1 (Coefficientwise absolute value).

$$\forall F:\mathrm{PowerSeries}\left(\mathbb{Z}\right),\mathrm{absSeries}\left(F\right)=\mathrm{mk}\left((n:\mathbb{N}\mapsto \mathrm{abs}\left(\mathrm{coeff}\left(n,F\right)\right))\right)$$

Formalization. D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.absSeries (✓ std3).

Source. Repository-derived.

Commentary.

Absolute value is applied to each reciprocal coefficient before cubing.

Definition 1.2 (The stabilized coefficient sequence).

$$\begin{array}{r}P\left(0\right)=1\\ \forall r:\mathbb{N},P\left(r+1\right)=1+X\cdot (\mathrm{absSeries}\left(\mathrm{invOfUnit}\left(P\left(r\right),1\right)\right){)}^3\\ \forall n:\mathbb{N},a\left(n\right)=\mathrm{coeff}\left(n,P\left(n+1\right)\right)\end{array}$$

Formalization. D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.a (✓ std3).

Source. Repository-derived.

Commentary.

The auxiliary approximations P start at one. Inversion of series with constant coefficient one, coefficientwise absolute value, and cubing preserve coefficient agreement. Multiplication by X increases the degree of agreement, so coefficient n stabilizes by step n+1.

Definition 1.3 (The generating series).

$$A=\mathrm{mk}\left(a\right)$$

Formalization. D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.generatingSeries (✓ std3).

Source. Repository-derived.

Commentary.

The series A has the stabilized integer coefficients a(n).

Theorem 1.4 (The exact functional equation).

$$(\mathrm{constantCoeff}\left(A\right)=1)\wedge (A=1+X\cdot (\mathrm{absSeries}\left(\mathrm{invOfUnit}\left(A,1\right)\right){)}^3)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.generating_equation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Stabilization proves the functional equation with constant coefficient one. The inverse is therefore the reciprocal of A.

Theorem 1.5 (Uniqueness of the normalized solution).

$$\forall B:\mathrm{PowerSeries}\left(\mathbb{Z}\right),(\mathrm{constantCoeff}\left(B\right)=1)⟹((B=1+X\cdot (\mathrm{absSeries}\left(\mathrm{invOfUnit}\left(B,1\right)\right){)}^3)⟹(B=A))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.generating_unique (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two fixed-point equations extend agreement by one degree. Induction gives agreement in every degree and hence equality.

Theorem 1.6 (Three Lucas recursions).

$$\forall r:\mathbb{N},(\mathrm{choose}\left(4\cdot \left(4\cdot r+1\right)+1,4\cdot r+1\right)\mathrm{mod}2=\mathrm{choose}\left(4\cdot r+1,r\right)\mathrm{mod}2)\wedge ((\mathrm{choose}\left(4\cdot \left(4\cdot r+3\right)+1,4\cdot r+3\right)\mathrm{mod}2=0)\wedge (\mathrm{choose}\left(4\cdot 2\cdot r+1,2\cdot r\right)\mathrm{mod}2=(\mathrm{if}(r=0)\mathrm{then}1\mathrm{else}0)))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.lucas_recursion_q (✓ std3). ∎

Source. Repository-derived.

Commentary.

Mathlib’s binary Lucas congruence gives the two odd-index formulas. For a positive even index, repeated halving reduces choose(4r,r) to a binomial coefficient with even upper and odd lower index, which vanishes modulo two.

Theorem 1.7 (Identification with the binomial parity series).

$$\mathrm{map}\left(\mathrm{intCast}\left(\mathrm{ZMod}\left(2\right)\right),A\right)=\mathrm{mk}\left((n:\mathbb{N}\mapsto (\mathrm{if}(n=0)\mathrm{then}1\mathrm{else}\mathrm{zmodCast}\left(\mathrm{choose}\left(4\cdot n-1,n\right),\mathrm{ZMod}\left(2\right)\right)))\right)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.mod_two_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Absolute values disappear modulo two. If f is the reduction of A and U its reciprocal, the equation gives U=1+XU^4 and f=f^2+XU^2. The Lucas recursions and Frobenius give Q=1+XQ^4 when coefficient n of Q is choose(4n+1,n) modulo two. Factoring the difference of the quartic equations gives Q=U by cancellation of a series with unit constant coefficient. The two Lucas recursions for the displayed binomial series H give H=H^2+XQ^2. Thus (1-f-H)*(f-H)=0. The first factor has constant coefficient -1 and is a unit, proving f=H.

Theorem 1.8 (The constant coefficient).

$$a\left(0\right)=1$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.a_zero (✓ std3). ∎

Source. Repository-derived.

Commentary.

The exact equation gives a(0)=1. This represents the convention binomial(-1,0)=1 without using natural subtraction at index zero.

Theorem 1.9 (Hanna’s A380709 conjecture).

$$\forall n:\mathbb{N},(0<n)⟹(a\left(n\right)\mathrm{mod}2=\mathrm{ofNat}\left(\mathrm{choose}\left(4\cdot n-1,n\right)\right)\mathrm{mod}2)$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.hanna_conjecture (✓ std3). ∎

Resolves. Problems/oeis-a380709-absolute-reciprocal-cube-parity (proved) by D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.hanna_conjecture.

Citation. Paul D. Hanna (2025). OEIS A380709, g.f. satisfying A(x) = 1 + xabs(1/A(x))^3*. URL: https://oeis.org/A380709.

Commentary.

At each positive index, coefficient extraction from the reduction identity gives equality in ZMod(2). Mathlib identifies this equality with equality of the two integer remainders modulo two.

References

• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.a
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.a_zero
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.absSeries
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.generatingSeries
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.generating_equation
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.generating_unique
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.hanna_conjecture
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.lucas_recursion_q
• Truth anchor: D5/S1/Recurrence/Parity/AbsoluteReciprocalCubeParity.mod_two_identity