OEIS A193237: congruences modulo five and seven

Abstract

Bala’s unbounded modulo-five and modulo-seven coefficient congruences.

All indices are natural numbers. Nat.div is natural-number division. The finite coefficient sum expresses the infinite triangular series: j*(j+1)/2=m implies j≤m. PowerSeries coefficients are rational unless stated otherwise.

Definition 1.1 (The source series).

$$F=\mathrm{PowerSeries}.\mathrm{mk}\left((\lambda (m:\mathbb{N})\mapsto \sum _{j\in \mathrm{Finset}.\mathrm{range}\left(m+1\right)}\mathrm{if}\mathrm{Nat}.\mathrm{div}\left(j\cdot \left(j+1\right),2\right)=m\mathrm{then}(2\cdot j+1:\mathbb{Q})\cdot (3{)}^j\cdot (-1{)}^{\mathrm{Nat}.\mathrm{div}\left(j\cdot \left(j+1\right),2\right)}\mathrm{else}0)\right)$$

Formalization. D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.F (✓ std3).

Citation. Peter Bala; Paul D. Hanna (2021). OEIS A193237 and A193236, congruences for triangular reciprocal cube roots. URL: https://oeis.org/A193237/internal.

Commentary.

Expansion of g.f.: ( Sum_{n>=0} (2n+1)3^n(-x)^(n(n+1)/2) )^(-1/3). OEIS A193237, NAME line (unnumbered web entry; no page number). The coefficient at degree m sums exactly the terms of triangular degree m.

Definition 1.2 (The normalized reciprocal cube root).

$$\forall (A:\mathrm{PowerSeries}\left(\mathbb{Q}\right)),\mathrm{IsGF}\left(A\right)=\left((\mathrm{constantCoeff}\left(A\right)=1)\wedge ((A{)}^3\cdot F=1)\right)$$

Formalization. D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.IsGF (✓ std3).

Citation. Peter Bala; Paul D. Hanna (2021). OEIS A193237 and A193236, congruences for triangular reciprocal cube roots. URL: https://oeis.org/A193237/internal.

Commentary.

The source’s constant-one expansion means constantCoeff(A)=1 and A^3*F=1.

Definition 1.3 (Bala’s two conjectures).

$$claim=\left((\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))\Rightarrow (\exists (a:\mathbb{N}\to \mathbb{Z}),(\forall (m:\mathbb{N}),\mathrm{coeff}\left(m,A\right)=(a\left(m\right):\mathbb{Q}))\wedge (\forall (n:\mathbb{N}),((5:\mathbb{Z})\mid a\left(5\cdot n+4\right))\wedge ((7:\mathbb{Z})\mid a\left(7\cdot n+5\right)))))\right)$$

Formalization. D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.claim (✓ std3).

Citation. Peter Bala; Paul D. Hanna (2021). OEIS A193237 and A193236, congruences for triangular reciprocal cube roots. URL: https://oeis.org/A193237/internal.

Commentary.

Conjectures: a(5n+4) == 0 (mod 5) and a(7n+5) == 0 (mod 7) (both checked up to n = 200). - Peter Bala, Feb 26 2021 OEIS A193237, FORMULA line (unnumbered web entry; no page number). The statement asserts existence and covers every normalized rational solution, an integer coefficient sequence, both primes, and every natural index.

Definition 1.4 (Weighted triangular series).

$$\forall (R:Type)[\mathrm{Semiring}\left(R\right)],\forall (w:\mathbb{N}\to R),\mathrm{triangular}\left(w\right)=\mathrm{PowerSeries}.\mathrm{mk}\left((\lambda (m:\mathbb{N})\mapsto \sum _{j\in \mathrm{Finset}.\mathrm{range}\left(m+1\right)}\mathrm{if}\mathrm{Nat}.\mathrm{div}\left(j\cdot \left(j+1\right),2\right)=m\mathrm{then}(2\cdot j+1:R)\cdot w\left(j\right)\mathrm{else}0)\right)$$

Formalization. D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.triangular (✓ std3).

Source. Repository-derived.

Commentary.

For any semiring R and weight function w, the coefficient at degree m is the sum of (2*j+1)*w(j) over the triangular indices of degree m.

Theorem 1.5 (Weighted triangular reciprocal cube roots).

$$\forall (F:\mathrm{PowerSeries}\left(\mathbb{Q}\right)),\forall (w:\mathbb{N}\to \mathbb{Z}),(w\left(0\right)=1)\Rightarrow ((\forall (j:\mathbb{N}),(0<j)\Rightarrow ((9:\mathbb{Z})\mid (2\cdot j+1:\mathbb{Z})\cdot w\left(j\right)))\Rightarrow ((F=\mathrm{PowerSeries}.\mathrm{map}\left(\mathrm{Int}.\mathrm{castRingHom}\left(\mathbb{Q}\right),\mathrm{triangular}\left(w\right)\right))\Rightarrow ((\exists (A:\mathrm{PowerSeries}\left(\mathbb{Q}\right)),(\mathrm{constantCoeff}\left(A\right)=1)\wedge ((A{)}^3\cdot F=1))\wedge (\forall (A:\mathrm{PowerSeries}\left(\mathbb{Q}\right)),((\mathrm{constantCoeff}\left(A\right)=1)\wedge ((A{)}^3\cdot F=1))\Rightarrow (\exists (a:\mathbb{N}\to \mathbb{Z}),(\forall (m:\mathbb{N}),\mathrm{coeff}\left(m,A\right)=(a\left(m\right):\mathbb{Q}))\wedge (\forall (n:\mathbb{N}),((5:\mathbb{Z})\mid a\left(5\cdot n+4\right))\wedge ((7:\mathbb{Z})\mid a\left(7\cdot n+5\right))))))))$$

Proof. Machine-checked in Lean as D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.resolve (✓ std3). ∎

Source. Repository-derived.

Commentary.

Weights with w(0)=1 and nine dividing every positive triangular coefficient give an integral normalized reciprocal cube root. Its coefficients satisfy both congruences, independently of the remaining weights.

Theorem 1.6 (Both unbounded congruences).

$$(\exists (A:\mathrm{PowerSeries}\left(\mathbb{Q}\right)),(\mathrm{constantCoeff}\left(A\right)=1)\wedge ((A{)}^3\cdot F=1))\wedge (\forall (A:\mathrm{PowerSeries}\left(\mathbb{Q}\right)),((\mathrm{constantCoeff}\left(A\right)=1)\wedge ((A{)}^3\cdot F=1))\Rightarrow (\exists (a:\mathbb{N}\to \mathbb{Z}),(\forall (m:\mathbb{N}),\mathrm{coeff}\left(m,A\right)=(a\left(m\right):\mathbb{Q}))\wedge (\forall (n:\mathbb{N}),((5:\mathbb{Z})\mid a\left(5\cdot n+4\right))\wedge ((7:\mathbb{Z})\mid a\left(7\cdot n+5\right)))))$$

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

Resolves. Problems/bala193237 (proved) by D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.result.

Source. Repository-derived.

Acknowledgement. Peter Bala; Paul D. Hanna (2021). OEIS A193237 and A193236, congruences for triangular reciprocal cube roots. URL: https://oeis.org/A193237/internal.

Commentary.

The positive-degree coefficients of F are multiples of nine. Coefficient contraction constructs an integral cube root of F, whose inverse is integral. Modulo five the triangular series is supported in residues 0 and 1, so its cube misses residue 4. Modulo seven it is supported in residues 0, 1 and 3, so its square misses residue 5. Frobenius transfers these missing residues to the reciprocal cube root. Uniqueness identifies every normalized rational solution.

References

• Truth anchor: D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.F
• Truth anchor: D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.IsGF
• Truth anchor: D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.claim
• Truth anchor: D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.resolve
• Truth anchor: D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.result
• Truth anchor: D5/S1/Recurrence/Residue/BalaA193237ModFiveSeven.triangular
• Dependency: D5/S1/Recurrence/Invariants/PowerSeriesNormalizedContraction