Theorem: An exact finite witness algorithm with a stated promise

Suppose $Z\ne 0$ is a positive matrix with entries in $\mathbb{Q}+i\mathbb{Q}$, and its range is product-free. There is an exact-arithmetic procedure which terminates and outputs rational $ϵ>0$ and

as in Proposition prop:support-witness. It supplies a finite rational certificate for global product nonnegativity. No polynomial running-time bound is asserted.

Proof. Gaussian elimination selects a full-column-rank rational matrix $V$ spanning $\mathrm{ran}Z$. Therefore

have rational complex entries.

For integers $M\ge 2(a+b)$, use all nonzero complex grid vectors whose real and imaginary coordinates are integer multiples of $1/M$ in $[-1,1]$, and normalize them. They form unit-sphere nets ${\mathcal{N}}_a(M)$, ${\mathcal{N}}_b(M)$. Rounding and then normalizing gives covering radii at most $2a/M$, $2b/M$, respectively.

For unit vectors, $0⪯Q⪯I$ gives

where $q(x,y)=⟨x\otimes y,Q(x\otimes y)⟩$. Consequently, with

every unit product vector has $Q$-expectation at least ${ϵ}_M$.

Each grid expectation is rational. If $x=g/\Vert g\Vert$ and $y=h/\Vert h\Vert$, its value is

with rational numerator and denominator. Thus all comparisons are exact. Try successively doubled $M$ until ${ϵ}_M>0$. Because $m_M\ge {\delta }_{\ast }>0$, termination follows.

For a fixed $M$, at most

pairs are tested. Their rational values and the Lipschitz allowance certify the global lower bound. The potentially very small unknown ${\delta }_{\ast }$ prevents a claimed efficient complexity bound.