We present a Lean 4 framework for polynomial-time reductions and complexity-theory proofs, and use it to formalize the complexity of identifying decision-relevant information. Problem: given a decision problem, which coordinates suffice to compute an optimal action? (SUFFICIENCY-CHECK; explicit encodings). Verified complexity results (Lean): coNP-complete; $(1-\varepsilon)\ln n$ inapproximable (from SET-COVER); $2^{Ω(n)}$ lower bounds under ETH for succinct encodings; W[2]-hard for a natural parameterization; and a dichotomy between explicit and succinct models. Formalization contributions: bundled Karp reductions with polynomial-time witnesses; composition lemmas/tactics; and templates for NP/coNP and $Σ_2^P$ membership and hardness. Scale: about 5,600 lines of Lean across 36 files, with 230+ theorems and explicit polynomial bounds.

翻译：我们提出了一个用于多项式时间归约和复杂性理论证明的Lean 4框架，并利用该框架形式化了识别决策相关信息的复杂性。问题描述：给定一个决策问题，哪些坐标足以计算最优行动？（SUFFICIENCY-CHECK；显式编码）。已验证的复杂性结果（Lean）：coNP完全；$(1-\varepsilon)\ln n$不可近似（归约自SET-COVER）；在ETH假设下针对简洁编码的$2^{Ω(n)}$下界；针对自然参数化的W[2]-困难性；以及显式与简洁模型间的二分性。形式化贡献：包含多项式时间见证的捆绑式Karp归约；组合引理/策略；以及用于NP/coNP和$Σ_2^P$成员性与困难性证明的模板。规模：约5,600行Lean代码，分布于36个文件，包含230余个定理及显式多项式边界。