Linear Recurrence Sequences (LRS) are a fundamental mathematical primitive for a plethora of applications such as the verification of probabilistic systems, model checking, computational biology, and economics. Positivity (are all terms of the given LRS non-negative?) and Ultimate Positivity (are all but finitely many terms of the given LRS non-negative?) are important open number-theoretic decision problems. Recently, the robust versions of these problems, that ask whether the LRS is (Ultimately) Positive despite small perturbations to its initialisation, have gained attention as a means to model the imprecision that arises in practical settings. However, the state of the art is ill-equipped to reason about imprecision when its extent is explicitly specified. In this paper, we consider Robust Positivity and Ultimate Positivity problems where the neighbourhood of the initialisation, expressed in a natural and general format, is also part of the input. We contribute by proving sharp decidability results: decision procedures at orders our techniques are unable to handle for general LRS would entail significant number-theoretic breakthroughs.

翻译：线性递归序列（LRS）是诸多应用领域中的基础数学工具，涵盖概率系统验证、模型检测、计算生物学及经济学等。正性（给定LRS的所有项是否非负？）与最终正性（给定LRS除有限项外的所有项是否非负？）是重要的开放性数论决策问题。近年来，这些问题的鲁棒版本——询问LRS在初始化存在微小扰动时是否（最终）保持正性——作为建模实际场景中不确定性的一种手段而备受关注。然而，当前技术水平尚不足以在不确定性范围被明确指定时对其进行有效推理。本文研究鲁棒正性与最终正性问题，其中初始化邻域（以自然且通用的格式表示）亦作为输入的一部分。我们通过证明尖锐的可判定性结果作出贡献：若现有技术能处理一般LRS在更高阶数下的决策过程，则将意味着数论领域的重大突破。