We study physical information sufficiency as a decision-theoretic meta-problem. For $\mathcal{D}=(A,S,U)$ with factored state space $S=X_1\times\cdots\times X_n$, a coordinate set $I$ is sufficient when $$s_I=s'_I \implies \operatorname{Opt}(s)=\operatorname{Opt}(s').$$ This asks whether projected information preserves the full optimal-action correspondence. Complexity landscape. - SUFFICIENCY-CHECK is coNP-complete; MINIMUM-SUFFICIENT-SET is coNP-complete; ANCHOR-SUFFICIENCY is $Σ_{2}^{P}$-complete. - Under explicit-state encoding, polynomial-time algorithms hold for bounded actions, separable utility, and tree-structured utility. - Under succinct encoding, hardness is regime-dependent: with ETH, there are worst-case families with $k^*=n$ requiring $2^{Ω(n)}$ time. - Under query access, the finite-state core has worst-case Opt-oracle complexity $Ω(|S|)$, with Boolean value-entry and state-batch refinements preserving the obstruction. Physical grounding. The paper formalizes a physical-to-core encoding $E:\mathcal{P}\to\mathcal{D}$ and a transport rule: declared physical assumptions transfer to core assumptions, and core claims lift back to encoded physical instances. Encoded physical counterexamples induce core failures on the encoded slice. Discrete-time interface semantics (decision event = one tick) and budgeted thermodynamic lifts (bit lower bounds to energy/carbon lower bounds under declared constants) are formalized in the same assumption-typed framework. All theorem-level claims are machine-checked in Lean 4 (13969 lines, 609 theorem/lemma statements). Complexity-class completeness follows by composition with standard complexity results; regime-dependent and physical-transport consequences are proved as assumption-explicit closures.

翻译：我们研究物理信息充分性这一决策论元问题。对于具有因子化状态空间$S=X_1\times\cdots\times X_n$的$\mathcal{D}=(A,S,U)$，坐标集$I$是充分的当且仅当$$s_I=s'_I \implies \operatorname{Opt}(s)=\operatorname{Opt}(s').$$ 该问题探究投影信息是否保留了完整的优化行动对应关系。复杂性图景：- SUFFICIENCY-CHECK是coNP完全的；MINIMUM-SUFFICIENT-SET是coNP完全的；ANCHOR-SUFFICIENCY是$Σ_{2}^{P}$完全的。- 在显式状态编码下，对于有界行动、可分离效用及树结构效用存在多项式时间算法。- 在简洁编码下，困难性取决于具体机制：在ETH假设下，存在最坏情况族$k^*=n$需要$2^{Ω(n)}$时间。- 在查询访问下，有限状态核心的最坏情况Opt-预言机复杂度为$Ω(|S|)$，布尔值条目与状态批量优化均无法规避该障碍。物理基础。本文形式化了物理到核心的编码$E:\mathcal{P}\to\mathcal{D}$及传输规则：声明的物理假设转移为核心假设，核心结论可提升至编码后的物理实例。编码的物理反例会在编码切片上引发核心失效。离散时间接口语义（决策事件=一个时钟周期）与预算化热力学提升（在声明常数下将比特下界转换为能量/碳排放下界）均在同一假设类型框架中形式化。所有定理级声明均通过Lean 4进行机器验证（13969行代码，609项定理/引理陈述）。复杂性类完全性通过标准复杂性结果的复合推导得出；机制依赖性与物理传输推论均以假设显式闭包的形式证明。