The same decision problem can be polynomial-time tractable or PP-hard depending on how the input is encoded. Not the problem. Not the algorithm. The encoding.
The Decision Quotient framework formalizes this. Given a decision problem and a candidate input, the “relevance certification” question asks: does this input actually affect the answer? Under explicit-state encoding — where every state of a system is listed — this certification is tractable. Under succinct encoding — where states are described by a compact rule that generates them — certification jumps to PP-hardness, which is at least as hard as any problem solvable by a probabilistic polynomial-time machine with unbounded error.
The phase transition between these regimes is sharp. There is no gradual degradation of tractability as the encoding becomes more compact. The problem flips from polynomial to exponentially hard at a specific boundary. The encoding determines the complexity class, not the combinatorial structure of the problem itself.
The framework is mechanically verified: 22,000+ lines of Lean 4 with zero unproven claims. Every theorem, every lemma, every case analysis is checked by the proof assistant. This is a complexity result that carries its own certificate of correctness — no reviewer needs to verify the proofs by hand.
The structural insight is about what “the problem” means. In classical complexity theory, a problem is a language — a set of yes-instances. But the same language can have multiple encodings, and the complexity of recognizing membership can differ radically between them. The Decision Quotient says: the right unit of analysis is not the problem but the problem-encoding pair.
The same question, asked differently, can be easy or impossible. The difficulty lives in the representation, not the mathematics.