Blackwell dominance between statistical experiments is characterized in the finite square case and tested against Mu, Pomatto, Strack, and Tamuz's conjectured many-state sufficiency conditions for large-sample dominance.

A finite simplex theorem characterizes dominance via a barycentric-coordinate nonnegativity condition when states equal source signals and ratio vectors form a simplex. A closed-form countable-state diagnostic-monitor theorem is proved analytically. A three-state, two-signal pair is constructed satisfying all of Mu's necessary conditions but failing dominance at every sample size. The finite theorem, obstruction, and continuum inequalities are verified in Lean 4.30 with Mathlib (file MuMGFNegative.lean, theorem mu_appendixK_premises).

The finite simplex theorem gives an iff characterization of Blackwell dominance. The explicit counterexample satisfies normalization, positivity, pairwise genericity, all ordered KL inequalities, and both MGF comparisons yet fails dominance at every positive sample size, refuting the universal sufficiency conjecture.