Papers With

← All papers
First page of The Optimizer Quotient and the Certification Trilemma

The Optimizer Quotient and the Certification Trilemma

Tristan Simas

cs.CC Mar 16, 2026 · v1
formalization logic
Read PDF arXiv abstract Code
TL;DR
Mechanizes the finite reduction and verification core of the certification trilemma in Lean 4.
Abstract
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.
Problem

The optimizer quotient is the canonical object for exact decision-relevant information, but it is unknown whether its coordinate structure can be efficiently certified in various decision-theoretic regimes.

Approach

The authors prove that exact certification of the optimizer quotient's coordinate structure is subject to an impossibility trilemma: under P != coNP, no certifier can be simultaneously sound, complete, and polynomial-budgeted. They analyze complexity across three regimes (static, stochastic, sequential) and identify six structural restrictions that collapse certification to polynomial time. The finite reduction and verification core is mechanized in Lean 4.

Results

The certification trilemma is established (Theorem 7.1) with regime-specific costs: coNP for static, PP-hard for stochastic decisiveness, and PSPACE-complete for sequential. Six polynomial-collapse conditions are identified and the core finite-case reductions are verified in Lean 4.