Tebni’s A364822 congruence at odd primes

Abstract

Integral hyperbolic EGF coefficients have residue two at every odd prime.

All indices are natural numbers. PowerSeries has rational coefficients. The inverse is the formal power-series inverse, and factorials and integer coefficients are cast to the displayed carrier. Natural subtraction in n-k is truncated subtraction. Finset.range n contains the indices k<n. Int.ModEq uses an integer modulus. The entry is unpaginated.

Definition 1.1 (The even Taylor series).

$$\cosh =\mathrm{PowerSeries}.\mathrm{mk}\left((n:\mathbb{N}\mapsto (\mathrm{if}(\mathrm{Even}\left(n\right))\mathrm{then}((\mathrm{Nat}.\mathrm{factorial}\left(n\right):\mathbb{Q}){)}^{-1}\mathrm{else}0))\right)$$

Formalization. D5/S1/Recurrence/Residue/TebniA364822.cosh (✓ std3).

Citation. M. Tebni (2023). OEIS A364822, Expansion of e.g.f. cosh(x) / (1 - 2sinh(x))*. URL: https://oeis.org/A364822.

Commentary.

OEIS A364822, Name (unpaginated): “Expansion of e.g.f. cosh(x) / (1 - 2*sinh(x)).” The series cosh has coefficient 1/n! at even indices and zero at odd indices.

Definition 1.2 (The odd Taylor series).

$$\sinh =\mathrm{PowerSeries}.\mathrm{mk}\left((n:\mathbb{N}\mapsto (\mathrm{if}(\mathrm{Even}\left(n\right))\mathrm{then}0\mathrm{else}((\mathrm{Nat}.\mathrm{factorial}\left(n\right):\mathbb{Q}){)}^{-1}))\right)$$

Formalization. D5/S1/Recurrence/Residue/TebniA364822.sinh (✓ std3).

Citation. M. Tebni (2023). OEIS A364822, Expansion of e.g.f. cosh(x) / (1 - 2sinh(x))*. URL: https://oeis.org/A364822.

Commentary.

OEIS A364822, Name (unpaginated): “Expansion of e.g.f. cosh(x) / (1 - 2*sinh(x)).” The series sinh has coefficient 1/n! at odd indices and zero at even indices.

Theorem 1.3 (The normalized odd Taylor coefficients).

$$\forall n:\mathbb{N},\mathrm{IntegralEGFComposition}.\mathrm{eCoeff}\left(\sinh ,n\right)=(\mathrm{if}(\mathrm{Even}\left(n\right))\mathrm{then}0\mathrm{else}1)$$

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

Source. Repository-derived.

Commentary.

Factorial normalization cancels the Taylor denominator. Every even index gives zero and every odd index gives one; this coefficient identity also determines the sign of sinh under substitution of -X.

Definition 1.4 (Factorial-scaled coefficients).

$$\forall n:\mathbb{N},a\left(n\right)=((\mathrm{Nat}.\mathrm{factorial}\left(n\right):\mathbb{Q}))\cdot (\mathrm{PowerSeries}.\mathrm{coeff}\left(n,(\cosh )\cdot ((1-(2)\cdot (\sinh ){)}^{-1})\right))$$

Formalization. D5/S1/Recurrence/Residue/TebniA364822.a (✓ std3).

Citation. M. Tebni (2023). OEIS A364822, Expansion of e.g.f. cosh(x) / (1 - 2sinh(x))*. URL: https://oeis.org/A364822.

Commentary.

OEIS A364822, Name (unpaginated): “Expansion of e.g.f. cosh(x) / (1 - 2*sinh(x)).” Thus a(n) is n! times the nth ordinary coefficient; the initial index is zero.

Definition 1.5 (The conjecture).

$$\mathrm{claim}⟺(\forall p:\mathbb{N},(\mathrm{Nat}.\mathrm{Prime}\left(p\right))⟹((2<p)⟹(\exists z:\mathbb{Z},((z:\mathbb{Q})=a\left(p\right))\wedge (\mathrm{Int}.\mathrm{ModEq}\left((p:\mathbb{Z}),z,2\right)))))$$

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

Citation. M. Tebni (2023). OEIS A364822, Expansion of e.g.f. cosh(x) / (1 - 2sinh(x))*. URL: https://oeis.org/A364822.

Commentary.

OEIS A364822, Comments (unpaginated): “Conjectures: For p prime (p > 2), a(p) == 2 (mod p).” The prime p is natural, z is integer, and z equals a(p) after the rational cast. The strict bound excludes p=2.

Theorem 1.6 (Every coefficient is an integer).

$$\forall n:\mathbb{N},(\mathrm{Rat}.\mathrm{num}\left(a\left(n\right)\right):\mathbb{Q})=a\left(n\right)$$

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

Source. Repository-derived.

Commentary.

Substituting 2 sinh into the geometric series preserves integral factorial-scaled coefficients. The binomial product formula then proves integrality after multiplication by cosh. The rational numerator therefore equals the rational coefficient after casting.

Theorem 1.7 (The integer binomial recurrence).

$$\forall n:\mathbb{N},\mathrm{Rat}.\mathrm{num}\left(a\left(n\right)\right)=(\mathrm{if}(\mathrm{Even}\left(n\right))\mathrm{then}1\mathrm{else}0)+(2)\cdot (\sum _{k\in \mathrm{Finset}.\mathrm{range}\left(n\right)}((((\mathrm{Nat}.\mathrm{choose}\left(n,k\right):\mathbb{Z}))\cdot (\mathrm{Rat}.\mathrm{num}\left(a\left(k\right)\right)))\cdot ((\mathrm{if}(\mathrm{Even}\left(n-k\right))\mathrm{then}0\mathrm{else}1))))$$

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

Source. Repository-derived.

Commentary.

Multiplication by 1-2 sinh gives the recurrence. The k=n endpoint summand vanishes because sinh has constant coefficient zero. This recurrence also proves the congruence at powers of two.

Theorem 1.8 (Residue two at every odd prime).

$$\forall p:\mathbb{N},(\mathrm{Nat}.\mathrm{Prime}\left(p\right))⟹((2<p)⟹(\exists z:\mathbb{Z},((z:\mathbb{Q})=a\left(p\right))\wedge (\mathrm{Int}.\mathrm{ModEq}\left((p:\mathbb{Z}),z,2\right))))$$

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

Resolves. Problems/tebni364822-cong (proved) by D5/S1/Recurrence/Residue/TebniA364822.result.

Source. Repository-derived.

Acknowledgement. M. Tebni (2023). OEIS A364822, Expansion of e.g.f. cosh(x) / (1 - 2sinh(x))*. URL: https://oeis.org/A364822.

Commentary.

At a prime p>2 the even Taylor coefficient is zero. Every interior binomial coefficient is divisible by p; only the constant-index term survives and contributes two.

References

• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.a
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.claim
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.cosh
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.eCoeff_sinh
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.num_cast
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.num_recurrence
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.result
• Truth anchor: D5/S1/Recurrence/Residue/TebniA364822.sinh
• Dependency: D5/S1/Recurrence/Residue/IntegralEGFComposition
• Dependency: D5/S1/Recurrence/Residue/QuarticEGFFixedPoint