Show HN: Knowing What Matters is coNP-complete (Lean 4 formalized)

[trissim]

We prove that identifying decision-relevant coordinates in a decision problem is coNP-complete. Finding the minimum sufficient coordinate set is also coNP-complete.

Formally: given state space S = X_1 × ... × X_n and utility U : A × S → Q, a coordinate set I is sufficient if s_I = s'_I implies Opt(s) = Opt(s'). Checking whether I is sufficient reduces to TAUTOLOGY. Finding minimum I reduces to the same.

Main results:

SUFFICIENCY-CHECK is coNP-complete MINIMUM-SUFFICIENT-SET is coNP-complete (Sigma_2^P structure collapses) ANCHOR-SUFFICIENCY (fixed coordinates) is Sigma_2^P-complete Dichotomy: polynomial when |minimal set| = O(log |S|), exponential when Omega(n) Tractable cases: bounded |A|, separable U(a,s) = f(a) + g(s), tree-structured coordinates Engineering consequence: over-modeling is not laziness. Determining which configuration parameters matter requires solving coNP-complete problems. Including everything costs O(n). Minimizing costs Omega(2^n). For large n, over-specification is optimal.

This explains: config files that grow forever, heuristic feature selection (AIC/BIC/CV), absence of "find minimal config" tools. These are not tooling failures. They are optimal responses to intractability.

2760 lines of Lean 4 proofs. 106 theorems. Zero sorry.