Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: karp-sitnik-2009-luke-upper-bound
bibkey: karpsitnik2009luke
doi: 10.1016/j.jat.2008.10.002
triage: theorem
motivation_gids:
  - D5/S3/Analytic/KarpSitnikLuke/UpperResult.result
url: https://arxiv.org/abs/math/0703084

Refutation of the sum-condition Luke upper bound

Problem

D. Karp and S. M. Sitnik, Inequalities and monotonicity of ratios for generalized hypergeometric function, J. Approx. Theory 161 (2009), 337–352, DOI 10.1016/j.jat.2008.10.002, arXiv:math/0703084v2, Conjecture 2, printed p. 14, equation (38):

For 0 < σ ≤ min(a₁, a₂, . . . , a_q), ∑ᵢ₌₁ᵠ (bᵢ − aᵢ) > 0 and x > 0:

The preceding sentence reads:

The asymptotic formula (16) and numerical experiments suggest the following

Formula (16), printed p. 5, is preceded by:

It follows that for σ < min(a₁, a₂, . . . , a_q) we will have

The quotation transcribes the extracted display, which places a next to the Gamma product. Write . Separately, the asymptotically precise reading via (16) is : the inner exponent makes its leading asymptotic coefficient agree with (16). The counterexample has , where both readings coincide.

Formal reading

Lean names below have prefix D5.S3.Analytic.KarpSitnikLuke.UpperResult, except where their frozen owner is specified.

Source objectLean nameCorrespondence
Rising-factorial ratioD5.S3.Analytic.HypergeometricShiftTuran.TwoBlockResult.pochRatioQuotient of the products for a and b.
Summand of (1)D5.S3.Analytic.KarpSitnikLuke.Result.hyperTermExtra upper parameter σ, factorial denominator and zⁿ.
Series valueD5.S3.Analytic.KarpSitnikLuke.Result.hyperReal infinite sum of these summands.
Gamma product in (38)gammaProductExactly K defined above, with finite index type Fin q.
Restricted Conjecture 2claimPositive parameters, positive sum(b−a), 0<σ≤aᵢ, 0<x<1, summability, K>0 and the strict upper bound.
RefutationresultExactly ¬ claim.

Each additional condition weakens the universal assertion: restricts to the power-series disk, summability restricts to convergent series, and restricts the parameter set. The latter, with , makes the real-power base positive. Refuting the weaker assertion refutes the conjecture. The positive-sum assumption is impossible.

Motivation

The settling declaration is D5/S3/Analytic/KarpSitnikLuke/UpperResult.result. The source note is D5/L/Asymptotics/karpsitnik2009luke. The sum condition permits an individual denominator parameter smaller than its numerator partner, destroying the first-order comparison required by the upper expression.

Gap

The sum-condition upper assertion is false. Its witness is , , , , . All entries are positive, , , and . The Gamma product is . The proposed upper expression is , and the convergent hypergeometric series exceeds . The first denominator parameter is smaller than the corresponding numerator parameter; the componentwise case is not contradicted.

Route

At the witness the defining series is

The magnitudes are nonnegative and

The inequality follows from . Geometric comparison gives summability and monotonicity. The six-term alternating lower bracket gives

The Gamma recurrence and positivity of give , and . Hence the two factors in are and , giving and the upper expression .

Falsifier

A single parameter choice satisfying all hypotheses of claim with the function above its proposed upper bound contradicts that universal assertion. An error in the Gamma evaluation, summand identity, summability or alternating-series enclosure would invalidate this refutation.

Evidence

PROVED. D5.S3.Analytic.KarpSitnikLuke.UpperResult.result states ¬ claim without additional hypotheses. The private helpers witness_gamma, witness_summable and witness_lower establish K=1, convergence and the strict comparison with 2/3 at the exact witness.

COMPUTED. The immutable experiment directory contains ks2-upper-cert.py. Command python3 ks2-upper-cert.py, exit code 0; SHA-256 c5126bff3504c30dc22f27626d62e430135922a7c04f3cfd9b40c98523c063d2. The exact rational enclosure uses 40 successive-term checks and the alternating bracket with the uniform ratio bound. Both printed endpoints are 0.692994117069, above the bound 2/3. The decimal endpoints are approximations; the comparisons use exact fractions.

The supplied literature scope is the 56 citing works listed by OpenAlex for the source DOI. Karp, arXiv:1409.3071, and Karp–Prilepkina, arXiv:1609.02340, impose stronger structural conditions and do not state a settlement of Conjecture 2 in that bounded check. No settlement was found in the supplied Formal Conjectures and conjectures.io scope. These supplied readings do not establish exhaustive coverage or priority.

COMPUTED. The immutable experiment directory contains ks2-upper-scan.py. Command python3 ks2-upper-scan.py, exit code 0; SHA-256 014a74b262865cd087356a336ea9d9c143f53df1c8db534fee0acc39a0d876f6. With mpmath mp.dps = 30, , , and , all 18 output lines report F<bound False. These are finite numerical observations of the hypergeometric function and the proposed upper expression, not a continuous-interval inequality or a Lean result.

Triage

What the settlement shows

The first-order Taylor comparison at forces . The function has expansion , whereas the proposed upper expression has expansion . Thus their difference, function minus upper expression, is . If , positivity of this coefficient violates the upper bound for every sufficiently small positive . At with all , the Gamma recurrence gives . Componentwise implies , because the difference has numerator and positive denominator . For the witness . This is an explanatory Taylor derivation; the Lean theorem proves the exact , counterexample.

  • PROVED. D5.S3.Analytic.KarpSitnikLuke.UpperResult.result refutes the universal restricted upper assertion. Its counterexample meets and has positive Gamma product.
  • COMPUTED. The exact certificate above refines the strict formal lower bound to approximately 0.692994117069.
  • COMPUTED. The numerical scan ks2-upper-scan.py, command python3 ks2-upper-scan.py, exit code 0, SHA-256 014a74b262865cd087356a336ea9d9c143f53df1c8db534fee0acc39a0d876f6, uses mpmath mp.dps = 30, , , and . All 18 lines report F<bound False. This is numerical evidence only; it proves neither an inequality over a continuous interval nor a Lean result.
  • OPEN. The componentwise case with is not settled. Avoiding the first-order obstruction does not prove the upper inequality.
  • OPEN. Conjecture 1’s remaining componentwise case is not settled by this result. The frozen sibling’s sum-condition lower counterexample remains a separate result. No positive conclusion for other source results follows from this refutation.

ASSUMED-UNVERIFIED

Exhaustive literature coverage, citation-index completeness and priority are unverified; no new network search is asserted. The asymptotic motivation uses continuation, whereas the formal witness is strictly inside the power-series disk. The Taylor explanation is not a Lean formalization of a parameter family. Finite numerical continuation values do not establish uniform inequalities on continuous intervals.