slug: wei-guo-2014-exponential-derivative-ratio-complete-monotonicity
bibkey: weiguo2014completemonotonicity
doi: 10.1155/2014/851213
triage: theorem
motivation_gids:
  - D5/S3/Analytic/ExpRatioCM/Result.result
url: https://doi.org/10.1155/2014/851213

Refutation and exact classification of exponential derivative ratios

Problem

Section 5 of the source identified by D5/L/Asymptotics/weiguo2014completemonotonicity states:

Conjecture 12. For given i ∈ {0} ∪ ℕ, the functions ℱ_i(t) and 𝒢_i(t) defined in (10) or (27) are completely monotonic on (0, ∞).

Equation (6) defines

$$F_i(t)=(-1{)}^i{\left(\frac{1}{e^t-1}\right)}^{(i)},G_i(t)=(-1{)}^i{\left(\frac{1}{1-e^{-t}}\right)}^{(i)},$$

and equation (10) defines

$${\mathcal{F}}_i(t)=\frac{F_{i+1}(t)}{F_i(t)},{\mathcal{G}}_i(t)=\frac{G_{i+1}(t)}{G_i(t)}.$$

The source verifies $i=0,1$ in (30). Complete monotonicity means smoothness on $(0,\infty )$ and $(-1{)}^k{h}^{(k)}(t)\ge 0$ for every nonnegative integer $k$ and every $t>0$.

Formal reading

All Lean names below have prefix D5.S3.Analytic.ExpRatioCM.

The globally defined derivatives agree with derivatives of the smooth restrictions on the open positive half-line by neighborhood equality. No derivative value at zero is used.

Motivation

The refutation declaration is D5/S3/Analytic/ExpRatioCM/Result.result. Decreasingness controls the first derivative; complete monotonicity requires simultaneous sign constraints at every order. Exponential coefficients provide a way to distinguish these requirements.

Gap

Status: PROVED (refutation). The exact completely monotone indices for each family are $\{0,1,2\}$. At every index $i\ge 3$, both families have a negative alternating derivative on every interval $(T,\infty )$. The smallest order producing any negative value, as a function of the index, is not determined here.

Route

For $t>0$, termwise differentiation gives

$$F_i(t)=\sum _{n\ge 1}{n}^i{e}^{-nt},G_0(t)=1+F_0(t),G_i(t)=F_i(t)(i\ge 1).$$

Write $z=e^{-t}$ and $D_i(z)={\sum }_{n\ge 0}(n+1{)}^i{z}^n$. Then ${\mathcal{F}}_i=D_{i+1}/D_i$. Its coefficients satisfy

$$b_0=1,b_n=(n+1{)}^{i+1}-\sum _{j=1}^n(j+1{)}^i{b}_{n-j}(n\ge 1).$$

For $B=2^{i+2}$, strong induction gives $|b_n|\le B^n$. The coefficient convolution and absolute convergence give, for $t>\log B$ and $k\ge 1$,

$$(-1{)}^k{\mathcal{F}}_i^{(k)}(t)=\sum _{n\ge 1}{b}_n{n}^k{e}^{-nt}.$$

Put $a_n=(49/32)n(4/7{)}^n$. The normalized derivative at $t_k=k\log (7/4)$ is ${\sum }_n{b}_n{a}_n^k$. Here $a_1=7/8$, $a_2=1$, and $a_{n+3}\le (6/7)(16/21{)}^n$. For $k\ge 1$ satisfying $B(16/21{)}^k\le 1/2$, the explicit bound is

$$\left|\sum _n{b}_n{a}_n^k-b_2\right|\le |b_1|(7/8{)}^k+2B^3(6/7{)}^k.$$

Consequently,

$${\left(\frac{49}{32}\right)}^k(-1{)}^k{\mathcal{F}}_i^{(k)}\left(k\log \frac{7}{4}\right)⟶b_2=2\cdot 3^i-4^i.$$

This limit is negative for every $i\ge 3$. The normalization is positive and $t_k\to \infty$, so both ratio families have negative alternating derivatives arbitrarily far to the right.

For the remaining indices the closed forms are

$${\mathcal{F}}_0=\frac{1}{1-z},{\mathcal{F}}_1=\frac{1+z}{1-z},{\mathcal{F}}_2=\frac{1+4z+z^2}{1-z^2},{\mathcal{G}}_0=\frac{z}{1-z}.$$

Their exponential coefficients are nonnegative. In particular, ${\mathcal{F}}_2=1+4F_0(t)-2F_0(2t)$ has coefficient four at positive odd frequencies and coefficient two at positive even frequencies. The formal sign argument uses the even-subseries inequality $2^k{F}_k(2t)\le F_k(t)$. The positive-index ratios of the two families coincide, completing the positive range; Result.failure_on_every_tail excludes every index at least three.

Falsifier

One index and one positive argument with a negative alternating derivative refute the universal assertion. Index three supplies such values. A completely monotone ratio at any index at least three would contradict Result.failure_on_every_tail. The decreasing property alone does not imply the higher-order sign conditions.

Evidence

D5/S3/Analytic/ExpRatioCM/Result.result proves exactly result : ¬ claim. It specializes Result.failure_on_every_tail to index three and threshold zero, then contradicts the complete-monotonicity sign conditions using both negative alternating derivatives at the supplied positive point. The failure theorem uses Extraction.quotient_extraction_limit, whose limit decomposition uses Extraction.extraction_limit. The extraction uses Series.abs_quotCoeff_le and Series.iteratedDeriv_ratioF; negativity follows from Series.quotCoeff_two.

The positive cases are an independently proved component: Positive.cm_of_le_two uses the moment expansion and the low-index closed forms, reusing Interpolation.LogOneSubExpDerivatives.log_one_sub_exp_derivatives for the first two signed moment identities. This component is not a dependency of Result.result. The axiom closure of the result is exactly {propext, Classical.choice, Quot.sound}.

The refutation route was derived with the assistance of the ChatGPT Pro model. Guo–Qi, arXiv:2201.06970, Section 5, Proposition 5.1, strengthens the decreasing property to the range $(1,\infty )$ and does not address complete monotonicity of the ratios. No proof or refutation was found in the searched scope consisting of the title, DOI and conjecture queries; Proskurnikov–Runvik–Medvedev, arXiv:2302.01364, Appendix B; Formal Conjectures; conjectures.io; and the corresponding repository mathematical, bibliographic and problem entries. The cited appendix uses another theorem of the source. This scope does not establish exhaustive citation-index coverage or priority.

Triage

• PROVED. ${\mathcal{F}}_i$ and ${\mathcal{G}}_i$ are completely monotonic on $(0,\infty )$ for $i\le 2$ by Positive.cm_of_le_two, and fail complete monotonicity for $i\ge 3$ by Result.failure_on_every_tail.
• PROVED. For every $i\ge 3$, failure occurs on every interval $(T,\infty )$, by Result.failure_on_every_tail; the two families have negative alternating derivatives at the same order and point.
• PROVED in prose. For a function agreeing with $h(t)={\sum }_{n\ge 0}{b}_n{e}^{-nt}$ on a right half-line and satisfying $|b_n|\le B^n$ for some $B>0$, $(49/32{)}^k(-1{)}^k{h}^{(k)}(k\log (7/4))\to b_2$. Locally uniform termwise differentiation and the geometric tail estimate in the route apply to arbitrary such coefficients, detecting the sign of the second exponential coefficient.
• COMPUTED. With 80-digit arithmetic, $(-1{)}^k{\mathcal{F}}_3^{(k)}(k\log (7/4))$ is approximately $-0.0039$ at $k=12$. For ${\mathcal{F}}_4$ the sampled alternating derivatives are negative from $k=16$ onward among the evaluated orders $k\in \{16,17,20,24\}$. The quotient coefficients for $i=3$ begin $b_1,b_2,b_3,b_4=8,-10,56,-190$. These numerical values are separate from the formal proof and do not determine the smallest negative derivative order.
• OPEN. The smallest order $k$ at which $(-1{)}^k{\mathcal{F}}_i^{(k)}$ first takes a negative value somewhere on $(0,\infty )$, as a function of $i\ge 3$.

ASSUMED-UNVERIFIED

Exhaustive citation-index coverage and priority are unverified. The bounded literature conclusions do not assert the absence of a proof or refutation outside that scope. The numerical evaluations have no certified rounding bounds; the sign and classification conclusions instead follow from the formal derivative and limit arguments.