slug: ulg398064
bibkey: ulgenes2026a398064
doi: null
url: https://oeis.org/A398064
triage: theorem
motivation_gids:
  - D5/S3/Weil/ZetaGamma/HadamardTruncatedBinomialLimit.result

Ulgenes’s truncated-binomial Hadamard limit

Problem

OEIS A398064, revision 39, FORMULA:

Conjecture: H(x+1) = lim_{n->oo} n^{x+1} * Sum_{k=0..n} (-1)^k/(n+k) * binomial(x, k) such that H(1/4) = 0.79564036… . Changing the upper bound of the sum to oo yields Euler’s product representation of the Gamma function.

The binding interpretation in #22706 is over every $x\in \mathbb{C}$. Put

$$S_n(x)=\exp ((x+1)\log n)\sum _{k=0}^n\frac{(-1{)}^k}{n+k}\left(\genfrac{}{}{0ex}{}{x}{k}\right).$$

The logarithm is real for positive $n$. The entire source function satisfies $H(m+1)=m!$ and, away from positive integers,

$$H(y)=\frac{\psi (1-y/2)-\psi ((1-y)/2)}{2\Gamma (1-y)}.$$

The assertion includes existence of such an entire function and convergence $S_n(x)\to H(x+1)$ for every such function and every complex parameter. No existence assumption is substituted for this conclusion.

Statement echo

All local names below belong to D5.S3.Weil.ZetaGamma.HadamardTruncatedBinomialLimit; intermediate lemmas are private. The definitions retain the preregistered expressions. The all-complex domain and existence conjunct specify the source’s otherwise unstated conventions without restricting the parameter domain.

Motivation

This is the external named OEIS conjecture preregistered in #22706. Admission is open-problem-resolution (#22706; Proved). The settlement concerns a moving finite cutoff, distinct from the infinite Euler-beta sum. The module has generality: G and utility: none: its declarations concern arbitrary complex parameters and analytic functions, with no finite checker or isolated numerical instance delivered as Lean content.

Gap

No settlement was identified in the finite source screen recorded in #22706. Classical entire Hadamard interpolation and Nielsen-beta identities are background, not new priority claims. The related Ulgenes article, arXiv:2301.09699v4, DOI 10.5206/mt.v5i1.16090, states a different inverse-Gamma conjecture. Yin–Zhang arXiv:2502.15852v1 supplies the derivative form of the Hadamard quotient, not this moving finite-cutoff limit. No source arXiv identifier for A398064 was identified.

Route

Euler’s Gamma-sequence limit gives convergence of the scaled generalized-binomial coefficient. A weighted continuous Riemann sum identifies the truncated sum on $\Re x<-1$. The paired digamma series identifies the Nielsen-beta integral. A reciprocal-Gamma derivative construction supplies an entire interpolation, and an exact finite-sum shift propagates the left-half-plane limit to all complex parameters. The proof uses no omitted infinite-tail theorem.

Falsifier

Failure of entire-function existence, factorial interpolation, the quotient away from its removable singularities, or convergence at any complex parameter would contradict result. Finite-precision agreement alone would establish none of these universal assertions. Altered cutoff ratios and uniform convergence are separate assertions.

Evidence

The settling declaration is D5/S3/Weil/ZetaGamma/HadamardTruncatedBinomialLimit.result, with no atom. The source is Library/Weil/ulgenes2026a398064.md. The public theorem is conservatively classified bind-only, with no escape-witness claim; its admission basis is the external named settlement.

The four-slot escape audit is unfinished for result, D5.S3.Weil.Analytic.BaezDuarteNewton.signed_choose, CycleGeodesic.continuous_leftRiemann_tendsto, and CycleGeodesic.fin_fraction_mem_Icc, tracked together in #22862. No completed registration is asserted.

Independent exact-arithmetic computation

Experiment directory at a27fabe086719046be72af8662f7878559d7eac1.

The pinned check.py has computation command python3 /Users/auric/.sshx/7623922ff91e476230faa2e1/attempt-1/experiment-check.py, exit 0. Its SHA-256 is 0491389559e2f1e4d62ad2c3f062e210b9423401271aa0905e407f994935658e.

The computation verifies the exact quarter-value digamma/radical identity, symbolic limits for integer $x=-8,\dots ,8$, 548 nonnegative-integer finite-sum equalities, 512 negative-integer finite-sum equalities, 96 rational/complex finite-sum cross-checks, coefficient recurrence and Gamma-sequence product identities for $k=0,\dots ,12$, and rational $O(1/n)$ bounds at $x=-1,-2$ for $n=1,\dots ,128$. These are the tested scopes; the computation is not evidence for the full complex-plane theorem.

Triage

What the settlement shows

Proved (kernel-checked): an Euler coefficient limit, continuous weighted Riemann sums, and exact shift propagation suffice for pointwise convergence on the entire complex plane. The terminating natural parameters are included in coefficient_scaled_tendsto_all; arbitrary negative integers enter through the same left-half-plane mechanism and shifts. Existence and uniqueness of the specified entire source function are established rather than assumed. These are consequences within the module’s exact hypotheses, not uniform estimates.

Computed: the exact quarter-value identity and the finite and integer windows listed in Evidence agree with the source expression. Open: a separately formalized omitted-tail limit, convergence rates uniform in a varying parameter, other cutoff ratios, and other factorial interpolations. No further result relying on the conjecture was identified in the inspected source; no claim about an uninspected dependency is made.

ASSUMED-UNVERIFIED

Literature completeness and worldwide novelty remain ASSUMED-UNVERIFIED. The finite literature screen in #22706 includes OEIS, arXiv, related journal text, citation metadata, Zenodo, formal-conjecture collections, repository records, and mathematical question sites. OpenAlex list queries were unavailable; the full Alzer, Newton, and Srivastava–Choi texts were not read. The source-fidelity mapping and conservative proof-shape classification are semantic assessments. The independent computation has only the scopes explicitly stated above. Escape registration remains unfinished under #22862.