The Optimizer Quotient and the Certification Trilemma

TL;DR

This paper introduces the optimizer quotient as a key decision-relevant abstraction and proves an impossibility trilemma for its exact certification under standard complexity assumptions.

Contribution

It establishes a fundamental impossibility result for certifying the optimizer quotient's structure, highlighting complexity barriers and conditions for polynomial-time certification.

Findings

Exact certification of the optimizer quotient faces an impossibility trilemma.

Complexity of certification varies across different regimes, from coNP to PSPACE.

Mechanization of the core in Lean 4 demonstrates practical verification approaches.

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.