The optimizer quotient is the canonical object for exact decision-relevant information: it is the coarsest exact decision-preserving abstraction (Theorem 2.15). This paper proves that exact certification of this object's coordinate structure is subject to an impossibility trilemma: under $\mathrm{P} \neq \mathrm{coNP}$, no certifier can be simultaneously sound, complete on all in-scope instances, and polynomial-budgeted (Theorem 7.1). The cost of this impossibility varies by regime: coNP (static), PP-hard (stochastic decisiveness), PSPACE-complete (sequential). Six structural restrictions collapse certification to polynomial time. The finite reduction and verification core is mechanized in Lean 4.

翻译：优化商是精确决策相关信息的典范对象：它是能保留决策信息的最粗粒度精确抽象（定理2.15）。本文证明，对该对象的坐标结构进行精确认证面临一个不可能性三难困境：在 $\mathrm{P} \neq \mathrm{coNP}$ 假设下，不存在同时具备可靠性、对范围内实例的完备性以及多项式预算限制的认证器（定理7.1）。这一不可能性的代价因领域而异：coNP（静态）、PP-hard（随机决定性）、PSPACE-complete（序贯）。六种结构约束可将认证问题降为多项式时间可解。有限归约与验证核心已在 Lean 4 中实现机械化。