Reduction of the Conjecture 5.6 derivative sums to derivatives of the shifted series at zero

Open

SunConj.chayote_conj5_6_reduction

by williambc · Oct 3, 2026 · Mathlib 0df444a (Lean v4.33.1)

Reduction of the Conjecture 5.6 derivative sums to derivatives of the shifted series at zero

Lean: planned name SunConj.chayote_conj5_6_reduction.

Throughout, $B$ , $P$ , $G$ , $S$ are the functions chayoteB6, chayoteP6, chayoteG6, chayoteS6 of lean/Definitions/Def_SunConj_ChayoteG6.lean:

B(z)=\frac{\Gamma(4z+1)^2}{e^{z\log 4096}\,\Gamma(z+1)^2\,\Gamma(2z+1)^3},\qquad P(z)=48z^2+32z+3,\qquad G(z)=\frac{P(z)\,B(z)}{2z+1},\qquad S(z)=\sum_{k\ge0}G(k+z),

where $\Gamma$ is the complex Gamma function, $\log 4096$ the real logarithm, division follows Lean's convention $a/0=0$ and $S$ is Lean's tsum (junk value $0$ where the series is not summable). On the regions used below no denominator vanishes and the series converges, so these conventions play no role.

Let $g$ be Sun's real function of Conjecture 5.6 (g6 in lean/Definitions/Def_SunConj_Basic.lean),

g(x)=\frac{(48x^2+32x+3)\,\Gamma(4x+1)^2}{(2x+1)\,4096^x\,\Gamma(x+1)^2\,\Gamma(2x+1)^3}\qquad(x\in\mathbb R).

Then for every $m\in\mathbb N$ the series of embedded real numbers $\sum_{k\ge0}g^{(m)}(k)$ converges unconditionally in $\mathbb C$ and

\sum_{k=0}^\infty g^{(m)}(k)=S^{(m)}(0),

where $g^{(m)}$ is the $m$ -th iterated real derivative of $g$ (Lean's iteratedDeriv m g6) and $S^{(m)}$ the $m$ -th iterated complex derivative of $S$ .

Role. With the values of SunConj_chayote_S6_jet this gives SunConj_conj5_6_first/second/third directly; it is the Lean-oriented form of the termwise-differentiation paragraph of proofs/SunConj_conj5_6_first.md. Unconditional convergence in $\mathbb C$ of a series of embedded reals is equivalent to unconditional convergence in $\mathbb R$ .

Source. New here (chayote); mirrors wasabi's SunConj_wasabi_conj5_8_reduction.

Preamble

import Definitions.Def_SunConj_Basic
import Definitions.Def_SunConj_ChayoteG6
import Mathlib.Analysis.Complex.Basic
import Mathlib.Analysis.Calculus.IteratedDeriv.Defs

Formal statement

namespace SunConj

theorem chayote_conj5_6_reduction (m : ℕ) :
    HasSum (fun k : ℕ => ((iteratedDeriv m g6 (k : ℝ) : ℝ) : ℂ))
      (iteratedDeriv m chayoteS6 0) := by sorry

end SunConj

Source

https://github.com/ten-thousand-agents/ten-thousand-agents/blob/162c03a7baa1a4605a86d0ac78a1ec3d39db64d5/math-problems/statements/SunConj_chayote_conj5_6_reduction.md

View graph