Sharp Bounds on the Winner's Bias under Independent and Nonnegatively Correlated Noise

• Evaluation designs can produce independent noise when candidates use their own items or typically positive correlation when all candidates use the same items.Neither class previously had a known closed-form sharp constant.Source: §1 · pp. 1–2
• The sharp constants are sqrt((M-1)/(2M)) for independent noise and (M-1)/M for pairwise nonnegative correlation, with both attained by explicit finite constructions.Source: §1 · p. 2
• The cross-validation estimator’s bias is bounded sharply within each dependence class.Source: §1 · p. 2
• At M = 4, the independent-class worst case is 19% above the Gaussian value; at large M, the gap is conservative by a factor of order sqrt(M/log M).Source: §1 · p. 2
• Across 448 language-model and classifier selection configurations, per-candidate designs realized a median 0.75 of the independent-class ceiling; shared items were 4.9 times less optimistic at fixed item budgets.The ceilings predict a factor of 2.1 for that comparison.Source: §1 · p. 2
• A shared master inequality handles the dependent classes, while the independent case requires different machinery; Lean 4 machine-checks every theorem, corollary, and lemma.Source: §1 · p. 2

• Alternatives have true means μ_i, unbiased score noise Z_i, and gaps g_i = μ* − μ_i; the selected winner maximizes μ_i + Z_i.Source: §2 · p. 2
• The cross-validation estimator’s bias is −E[g_I], between −E[max_i Z_i] and 0.Source: §2 · p. 3
• The transfer lemma gives E[g_I] ≤ E[max_j Z_j], linking the selection gap to the maximum noise.Source: §2 · p. 3
• Bounds on E[max_i Z_i]/sqrt(V) control max-estimator bias and absolute cross-validation bias; K-fold bounds apply fold-wise and average across folds.Source: §2 · p. 3

Master bound

• The master bound applies Aven’s inequality to deviations from the mean, and its covariance correction term separates the dependence classes.The proof uses Samuelson’s inequality pointwise, followed by Cauchy–Schwarz.Source: §3 · p. 3

Nonnegative correlation

• For pairwise nonnegative correlation, the bound is sharp in the uncorrelated subclass, with an explicit finite-parameter attaining law.With every covariance strictly positive, the bound is not attained; it remains sharp for the class as a whole.Source: §3 · p. 3

Independent noise

• For independent mean-zero noise, the sharp bound is attained exactly by an (M−1)-arm cascade together with one deterministic arm.The optimal role of one alternative is a deterministic floor; at M = 2, a deterministic arm is necessary for equality.Source: §3 · p. 4

Proof strategy

• The independent-noise proof reduces each arm to at most two atoms, then bounds the resulting problems using a recursion and a factored cubic.The reduction passes through a rank-2 linear program; equality occurs at the attaining configuration.Source: §3 · p. 4

Dependence-class comparison

• The constants form a strictly decreasing family down Table 1 for M ≥ 3; the nonnegative-correlation and independent constants coincide only at M = 2.The arbitrary-dependence constant coincides with neither of those constants.Source: §3 · p. 4, Table 1 · p. 4

Gaussian comparison

• At M = 2–5, the independent constant exceeds the i.i.d.-Gaussian comparator by 25.3%, 18.2%, 19.0%, and 21.6%, respectively.The comparator is i.i.d. Gaussian noise in every row, and the percentages are computed from exact values.Source: §3 · pp. 4–5, Table 2 · p. 4

4 The Bias of the Cross-Validation Estimator

• c = (M −1)/M under pairwise nonnegative correlation and c = (M −1)/(2M) under independence give sharp fold-wise bounds on Bias(CV).The Bias(CV) bound is approached along limiting configurations rather than attained.Source: §4 · p. 5
• The bound c = (M −1)/M < 1 settles van Hasselt (2013)'s Conjecture 1; the strict inequality fails only when every fold variance vanishes, when both sides are zero.Source: §4 · p. 5
• The general cross-validation result follows by applying Lemma 1 and Corollary 1a fold-wise; the same constants also bound Bias(ME).The Bias(CV) form is approached along limiting configurations in Appendix D.5 rather than attained.Source: §4 · p. 5
• At M = 2, the covariance-informed and nonnegative-correlation classes coincide at 1/2, but their constants separate for every M ≥3.The M = 2 result substitutes the sum of score variances for the variance of their difference under nonnegative covariance.Source: §4 · p. 6
• Standard K-fold usually uses shared held-out blocks, placing folds in the nonnegative-correlation class, while candidate-specific evaluation data gives the independent class.Within a fold, candidates scored on the same held-out block have selection scores that are typically positively correlated.Source: §4 · p. 6
• The i.i.d. constant lies strictly below the independent-class constant for every M ≥2, so i.i.d. noise does not govern that class.Source: §4 · p. 6

Designs and Definitions

• The evaluation resamples items with replacement: shared designs use the same items for every candidate, while per-candidate designs use independent draws that may overlap in content.Both designs have zero-mean scoring noise; independence comes from independent draws, not disjoint item sets.Source: §5 · p. 7

Validity of the Ceiling; Verifying the Class Hypothesis

• Measured E[max_i Z_i] stayed at or below its class ceiling in every cell, and the applicable class was determined by design and, for shared designs, pairwise covariance checks.All four language-model populations and four of five classifier pools had positive pairwise covariances; the 16-candidate wine pool had a pair at −0.031 and its eight-candidate shortlist had positive covariances.Source: §5 · pp. 7–8

Realized Fraction

• Across budgets and pool sizes, per-candidate designs realized a median 0.75 of their independent-class ceiling, while shared designs realized a median 0.37 of their own class ceiling.The respective maxima were 0.84 and 0.62; the medians span all pool sizes and budgets.Source: §5 · p. 7
• At M = 8 and eight items per candidate, independent-class fractions ranged from 0.71 to 0.76 in four pools with a candidate below 0.75, but were lower in pools with stronger candidates.The ordering across nine pools at one budget is not a general law; which pool feature predicts the fraction remains open.Source: §5 · p. 8

Design Effect at a Fixed Budget

• At equal budgets, shared evaluation incurred less optimism in all 220 resolved pairs; the measured per-candidate/shared ratio was 4.85 (IQR 3.14 to 8.63), versus predicted ratios of 1.41 to 2.92.The MMLU-Pro example had 3.09 points of optimism with shared items and 18.87 with split items, a factor of 6.1.Source: §5 · p. 8

Comparison with a Gaussian Model

• Matched-covariance Gaussian optimism differed from resampled optimism by a median factor of 0.89 across 444 cells, with the median rising from 0.60 at n = 16 to 0.96 at n = 1024.At small budgets it overstated optimism by up to sixteenfold; the direction reversed in 24 of 444 cells, by up to 1.5-fold at the largest budgets and extreme pass rates.Source: §5 · p. 8

Variance Heterogeneity

• The extremal laws for the independent-class bound require arm variances spanning a factor of order M, whereas measured pools spanned only 1.15 to 1.81.The authors therefore characterize the constants as computable ceilings, not predictions of observed optimism.Source: §5 · p. 9

Reporting Recipe

• The ceiling is 1.3 to 1.7 times E[max_i Z_i] for per-candidate designs and 2.4 to 3.2 times that quantity for shared designs, while its excess over reported-best optimism is larger.The corresponding factors against reported-best optimism are 1.5 to 3.3 and 4.5 to 11.7; the reporting recipe should distinguish these quantities.Source: §5 · p. 9

Classical Moment Bounds; Bounds for Samples from a Common Distribution

• Classical bounds cover the arbitrary-dependence and i.i.d. extremes, while the paper identifies independent non-identically distributed variables under per-variable variance information as a distinct untreated setting.The cited common-distribution results concern independent, identically distributed samples, with bounds in units of a common mean and standard deviation.Source: §6 · pp. 9–10

Bounds for Samples from a Common Distribution

• Prior dependent-marginal bounds and dependent-sample L-statistic results do not treat independent, non-identically distributed variables with per-variable variance information.That is the setting of Theorems 2 and 3.Source: §6 · p. 10

Convex-Optimization Bounds; The Open Covariance-Informed Problem

• Covariance-aware optimization gives tight per-instance bounds, but Papadatos (2016) left the general-M closed-form covariance-informed problem open; Corollary 1b answers its uncorrelated case.Bertsimas et al. (2006) use a semidefinite program, and Natarajan and Teo (2017) reduce such programs and apply them to expected range.Source: §6 · p. 10

Selection Bias in Model Evaluation; Post-Selection Inference; Estimating the Maximum of Means

• Earlier work measures or estimates selection bias in particular problems, whereas these results bound it in advance; post-selection inference is complementary because it gives distribution-dependent inference rather than distribution-free unconditional bias bounds.The cited post-selection methods use distributional assumptions and provide valid inference.Source: §6 · pp. 10–11

7 Limitations

• The independent-class extremizer’s deterministic-arm condition is proved only at M = 2 and remains a conjecture for general M.The conjecture is not used elsewhere in the paper.Source: §7 · p. 11
• The language-model pools vary one 7B model’s configuration, leaving mixed-model-scale pools untested; classifier pools use small models on standard-library datasets.The authors identify mixed model scales as the case whose variance profile could come closest to the extremal one.Source: §7 · p. 11
• Resampling makes scores mean-zero and per-candidate noise independent, while population scores are fixed and each candidate is scored once.The measurements therefore do not cover noise from retraining, data splits, or deployment distribution shift.Source: §7 · p. 11
• The 448-pipeline fractions describe only the tested pools and budgets, not typical-case guarantees; outside them, the paper makes no magnitude claim beyond Table 2.The explanation for the gap between ceilings and measurements is qualitative, and nine populations do not yield a quantitative predictor of ρ.Source: §7 · p. 11

AI Use Statement

• Generative AI assisted with writing the Lean formalization, editing text, modifying figures, and brainstorming the title, but not with developing theory, proofs, hypotheses, or experiments.Authors manually checked the formalization against the paper; Lean’s kernel checks the formal proofs, and authors checked the paper proofs line by line.Source: AI Use Statement · p. 11

Appendix

• Appendix E maps each theorem, corollary, and lemma to its Lean name, while the appendix also reports exact-arithmetic verification and planned release of the verification script.The formalization uses about 7,900 lines, with no sorry and no axioms beyond Lean’s standard three.Source: Appendix · p. 15

A.1 Setup and Notation

• The setup defines alternatives by true means and gaps, scores as unbiased estimates with variances, and the max and cross-validation estimators by the selected arm.For two-point mean-zero arms, the up value occurs with probability x_i and the down value with probability q_i = 1 − x_i.Source: §A.1 · p. 15

A.2 Lemma 1 (Transfer)

• E[g_I] ≤ E[max_j Z_j], so any upper bound on expected maximum noise also bounds the selected arm’s expected gap.The proof compares the selected noisy score with a fixed optimal arm and uses that arm’s zero-mean noise.Source: §A.2 · pp. 15–16
• Bounds on E[max_i Z_i]/√V therefore bound both |Bias(CV)| and Bias(ME), and the extremal constructions approach their constants in the gap form as well.In the limiting configurations, each gap approaches the largest noise lead its arm can take over the optimal arm.Source: §A.2 · p. 16
• For K-fold cross-validation, the transfer applies to each fold and then averages because averaging over folds does not change the estimator’s bias.The strict bound fails in the edge case where all fold variances vanish, when both sides are zero.Source: §A.2 · p. 16

B.1 Theorem 1 (Master Bound)

• The master bound has an equivalent formulation in pairwise-difference variances, with an exact slack expression for each fixed reference arm.For the reference-arm subfamily, equality holds exactly when some Z_j equals the mean noise almost surely.Source: §B.1 · pp. 16–17
• Theorem 1 applies Aven’s bound to centered deviations, using Samuelson’s inequality and Cauchy–Schwarz; the authors claim no novelty for the theorem itself.The covariance correction term is what separates the dependence classes below.Source: §B.1 · p. 17
• For a non-degenerate exchangeable law, including i.i.d. noise, the fixed-reference-arm ratio reaches 2; the general master bound’s equality conditions differ.Aven’s centered bound changes the equality case to require either zero mean noise almost surely or some arm equal to the mean noise almost surely.Source: §B.1 · p. 17

B.2 Corollary 1a (Arbitrary Dependence)

• At general M, the arbitrary-dependence constant is attained by a uniform-index one-up law; the anti-correlated pair attains it only at M = 2.The general construction has one value up and the rest equal in each realization, with the supremum attained at finite parameters.Source: §B.2 · p. 18

B.3 Corollary 1b (Pairwise Nonnegative Correlation; Sharp)

• A one-up law plus an independent common shock of variance d^2 gives mean-zero, pairwise uncorrelated arms and attains the bound exactly at every finite d.The one-up component has pairwise covariance −d^2, canceled by the common shock; the shock adds variance but nothing to the expected maximum.Source: §B.3 · p. 18
• The bound extends to pairwise nonnegatively correlated noise and is sharp already when the arms are uncorrelated.The extension uses E[Z̄^2] ≥ V/M^2; equality holds when all pairwise covariances vanish.Source: §B.3 · pp. 18–19
• The master variance bound cannot improve the constant for independent noise; the independent-class improvement requires a different mechanism.Independence gives the same E[Z̄^2] = V/M^2 as uncorrelatedness.Source: §B.3 · p. 19

C Theorem 2 (Independent Noise, Deterministic Best Arm)

• For m independent mean-zero alternatives, the sharp bound on E[T]^2/V is m/(2(m+1)), where T = max(0, Z1, . . . , Zm).With M = m + 1 arms and a deterministic best-arm estimate, this gives the corresponding sharp constant for the CV problem.Source: C Theorem 2 (Independent Noise,… · p. 19, §C.5 · p. 21

C.1 Step 1: Two-Point Reduction per Arm

• Each arm can be reduced to at most two atoms; an arm with no positive up-atom is a point mass at zero and can be dropped.The reduction uses Dinkelbach conjugation and linearity in each arm's law.Source: §C.1 · p. 19

C.2 Step 2: The Exact Formula

• Sorting the arms by up-value partitions T according to the first arm that is up, with T = 0 when all arms are down.Arms later in the order cannot change the maximum once an earlier arm is up.Source: §C.2 · p. 19

C.3 Step 3: The Cauchy–Schwarz Split

• The Cauchy–Schwarz split is tight at ui proportional to qisi, and that maximizing choice respects the assumed arm ordering.The ordering follows from si+1 = siqi.Source: §C.3 · p. 20

C.4 Step 4: The Recursion and Its Exact Solution

• The recursion is solved by induction, with Gm−1 = (m−1)/(2m) as the induction hypothesis and a concave quadratic objective in x.Setting the derivative to zero gives the maximizing x.Source: §C.4 · p. 20

C.5 Step 5: Attainment (The Cascade Law)

• A two-point cascade attains E[T]^2/V = m/(2(m+1)) exactly for every m.The construction uses arm k with up-value k/m and probability 1/(k+1) of that outcome; the survival factors telescope.Source: §C.5 · p. 21

D.1 The Two-Point Reduction

• The independent-noise supremum is unchanged when every arm is restricted to mean-zero laws with at most two atoms.A one-sweep sequence of exact per-arm replacements yields two-point laws without decreasing the joint objective.Source: §D.1 · p. 23

D.2 The Convexity Step

• The two-point objective is a maximum of M linear functionals, hence convex and homogeneous, enabling an upper bound after dropping the ordering constraint.The last sorted arm is bounded directly by the Theorem 2 constant with one fewer arm.Source: §D.2 · pp. 23–24

D.3 The Head Recursion

• The head-arm recursion is increasing and maps G_j to G_(j+1), reducing each bound to the Theorem 2 recursion and the tail inequality Φ_t ≤ G_t.Composing the recursion gives the bound G_(M−1).Source: §D.3 · p. 24

D.4 The Key Inequality Φt ≤Gt

• The constraint and trade-off curves touch at the always-firing-tail configuration, where both sides equal (t − 1)/(2t); the equality branch has x* = 1/(t + 1), with arm k acting as the deterministic floor.Source: §D.4 · p. 26

D Theorem 3 (Independent Noise, General)

• √((M −1)/(2M)) is the sharp constant for independent mean-zero noise, and the supremum is attained exactly.The construction uses the (M −1)-arm Theorem 2 cascade plus one deterministic-zero arm.Source: §D.4 · p. 26, §D.5 · p. 27

D.5 The Attainment Lemma

• The exact attaining construction adds a deterministic-zero arm to the (M −1)-arm cascade, making the maximum equal to the Theorem 2 quantity for m = M −1.For the bias-transfer form E[gI], gaps just below each cascade arm’s up-value approach the constant as ε → 0+ while variance stays unchanged.Source: §D.5 · p. 27
• As g approaches Md from below, E[gI] approaches (M − 1)d = E[max_i Zi], with V unchanged.The passage gives this limiting behavior for the attainment construction.Source: §D.5 · p. 27
• For M = 2, equality in E[max(Z1, Z2)] ≤ √(v1 + v2)/2 forces one independent arm to be deterministic.The passage states that equality holds iff |Z1 − Z2| is almost surely constant; for independent arms, this forces Z1 = 0 almost surely and Z2 = ±s, or vice versa.Source: §D.5 · p. 28
• For general M, the claim that every attaining configuration contains a deterministic arm remains a conjecture.The passage says Section 7 records the conjecture’s status.Source: §D.5 · p. 28

E Formal Verification in Lean 4

• The paper’s theorems, corollaries, and lemmas are formalized in Lean 4 with Mathlib, with no sorry and dependencies only on Lean’s standard axioms.The formalization uses toolchain and Mathlib v4.34.0-rc1 and comprises 11 files and about 7,900 lines; it builds with lake build.Source: E Formal Verification in Lean 4 · p. 28
• For Theorems 2 and 3, sharpness is formalized as a greatest element: the bound holds over admissible laws and some law attains it.Random variables are defined on an arbitrary probability space with finite variance and mean zero, and mutual independence where required.Source: E Formal Verification in Lean 4 · p. 28
• The formal proof uses shorter routes for two independent-case steps, including an arm-removal induction with a two-term Cauchy–Schwarz step.The two-point reduction uses a supporting-line lemma and Fubini’s theorem; the sum-of-squares certificate proves the stated bound, and the appendix’s separate ellipsoid-and-vertex-analysis route is also formalized.Source: E Formal Verification in Lean 4 · pp. 28–29