We characterize the computational complexity of coordinate sufficiency in decision problems within the formal model. Given action set $A$, state space $S = X_1 \times \cdots \times X_n$, and utility $u: A \times S \to \mathbb{R}$, a coordinate set $I$ is sufficient if $s_I = s'_I$ implies $\mathrm{Opt}(s) = \mathrm{Opt}(s')$. The landscape in the formal model: - General case: SUFFICIENCY-CHECK is coNP-complete; ANCHOR-SUFFICIENCY is $Σ_2^P$-complete. - Tractable cases: Polynomial-time for bounded action sets under the explicit-state encoding; separable utilities ($u = f + g$) under any encoding; and tree-structured utility with explicit local factors. - Encoding-regime separation: Polynomial-time under the explicit-state encoding (polynomial in $|S|$). Under ETH, there exist succinctly encoded worst-case instances witnessed by a strengthened gadget construction (mechanized in Lean) with $k^* = n$ for which SUFFICIENCY-CHECK requires $2^{Ω(n)}$ time. The tractable cases are stated with explicit encoding assumptions. Together, these results answer the question "when is decision-relevant information identifiable efficiently?" within the stated regimes. The primary contribution is theoretical: a complete characterization of the core decision-relevant problems in the formal model (coNP/$Σ_2^P$ completeness and tractable cases under explicit encoding assumptions). The practical corollaries follow from these theorems. The reduction constructions and key equivalence theorems are machine-checked in Lean 4 ($\sim$5,000 lines, 200+ theorems); complexity classifications follow by composition with standard results

翻译：我们在形式化模型中刻画了决策问题中坐标充分性的计算复杂性。给定动作集 $A$、状态空间 $S = X_1 \times \cdots \times X_n$ 以及效用函数 $u: A \times S \to \mathbb{R}$，若 $s_I = s'_I$ 蕴含 $\mathrm{Opt}(s) = \mathrm{Opt}(s')$，则坐标集 $I$ 是充分的。形式化模型中的复杂性图景如下：- 一般情况：SUFFICIENCY-CHECK 是 coNP 完全的；ANCHOR-SUFFICIENCY 是 $Σ_2^P$ 完全的。- 可处理情况：在显式状态编码下，对于有界动作集可在多项式时间内求解；在任何编码下，对于可分离效用函数（$u = f + g$）可在多项式时间内求解；对于具有显式局部因子的树结构效用函数可在多项式时间内求解。- 编码机制分离：在显式状态编码下（复杂度为 $|S|$ 的多项式）可在多项式时间内求解。在指数时间假设（ETH）下，存在通过强化构件构造（在 Lean 中实现）生成的、具有 $k^* = n$ 的最坏情况简洁编码实例，使得 SUFFICIENCY-CHECK 需要 $2^{Ω(n)}$ 的时间。可处理情况的陈述均附有明确的编码假设。这些结果共同回答了“在何种情况下可高效识别决策相关信息？”这一问题。主要贡献是理论性的：对形式化模型中核心决策相关问题（在显式编码假设下的 coNP/$Σ_2^P$ 完全性及可处理情况）进行了完整刻画。实际推论均源自这些定理。归约构造与关键等价定理已在 Lean 4 中实现机器验证（约 5,000 行代码，200+ 条定理）；复杂性分类通过与标准结果复合推导得出。