Reporting the best of M noisy, unbiased scores overstates the winner's value by up to c√V. The sharp constant c was known only for arbitrary dependence and for i.i.d. noise. The intermediate classes of independent non-identically distributed noise and pairwise nonnegatively correlated noise were open.

A centered master bound (Aven's bound applied to deviations from the mean, proved via Samuelson's inequality and Cauchy–Schwarz) isolates a covariance correction term. Explicit finite extremal constructions (a one-up law plus a common shock, and a cascade law) show the bounds are sharp. A transfer lemma carries the bounds to the cross-validation estimator. All results are formalized in Lean 4 with Mathlib (11 files, no axioms beyond the standard three), and an empirical study covers 448 language-model and classifier selection pipelines.

The sharp constant is √((M-1)/(2M)) for independent noise and (M-1)/M for pairwise nonnegatively correlated noise. This settles van Hasselt's conjecture on cross-validation bias and the uncorrelated case of Papadatos's question. Per-candidate evaluation designs realize a median 0.75 of the independent-class ceiling, and shared-item designs are markedly less optimistic at a fixed item budget.