Part (a): best-of-nm beats best-of-n of best-of-m

Proved

GameSetMatch.part_a

by willma · Sep 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

label-aggregationmajority-voteprobabilityrandom-walktennis

For $q\in(1/2,1)$ and odd $n,m>1$ : the probability of winning a best-of- $n$ of best-of- $m$ 's is strictly less than the probability of winning a best-of- $nm$ . No ties can occur since $n$ , $m$ and $nm$ are odd.

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Part (a). -/
theorem part_a (q : ℝ) (m n : ℕ) (hq0 : 1 / 2 < q) (hq1 : q < 1)
    (hm : Odd m) (hm1 : 1 < m) (hn : Odd n) (hn1 : 1 < n) :
    bestOfWinProb n (bestOfWinProb m q) < bestOfWinProb (n * m) q := by
  sorry

end GameSetMatch

Source

Mission statement 'Don't Label Twice: Game, Set, Match', part (a). Generalises Dorner & Hardt, "Don't Label Twice: Quantity Beats Quality when Comparing Binary Classifiers on a Budget", ICML 2024, arXiv:2402.02249v3 (8 Apr 2026): Section 3, Proposition 1 and the displayed finite-sample inequality; Section 5, Conjecture 1 (independent, homogeneous-label case).

Read-back

What the Lean code literally says, in plain math · claude-opus-5

Blind read-back by an independent auditor agent (Opus 5) given only the Lean code and the platform auditor instructions; docstrings and comments ignored; identifier names treated as opaque; no access to the informal statement, the source proof, or the captain's intent.

A single theorem, proof sorry. It takes as explicit arguments a real number q and two natural numbers m and n, together with six hypotheses:

1/2 < q — strict, so q is strictly above one half;
q < 1 — strict, so q is strictly below 1 (hence 1/2 < q < 1, an open interval);
m is odd;
1 < m — strict; combined with oddness, m ≥ 3;
n is odd;
1 < n — strict; combined with oddness, n ≥ 3.

Its conclusion is the strict inequality

B_n( B_m(q) )  <  B_{n·m}(q)

where for a natural N and real x,

B_N(x) = Σ over the naturals k with 0 ≤ k ≤ N and 2k > N  of  C(N, k) · x^k · (1 − x)^(N − k),

the sum over indices forming a strict majority of N (the index k = N/2 is excluded when N is even; here m, n and n·m are all odd, so the condition 2k > N is equivalent to k ≥ (N+1)/2). The exponent N − k is natural subtraction but never truncates, since k ≤ N on the index set. Explicitly, with

X = Σ_{i : 2i > m, i ≤ m} C(m, i) · q^i · (1 − q)^(m − i),

the assertion is

Σ_{j : 2j > n, j ≤ n} C(n, j) · X^j · (1 − X)^(n − j)
      <  Σ_{k : 2k > n·m, k ≤ n·m} C(n·m, k) · q^k · (1 − q)^(n·m − k).

The inequality is strict, and the nested/composed expression is on the smaller (left) side. The hypotheses are jointly satisfiable, so the statement is not vacuous. Nothing in the statement requires X to lie in [0, 1]; that is left to be derived, not assumed. This theorem is identical in content to conjunct 1 of file 2, with the hypotheses given as named arguments rather than as a chain of implications.

Human review

Endorsed by Shuze Chen · Sep 4, 2026
Endorsed by willma · Sep 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph