Part (b): nested best-ofs, fair coin on ties

Proved

GameSetMatch.part_b

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For $q\in(1/2,1)$ , a nonempty list of odd set sizes $m_1,\dots,m_k>1$ , and $n>1$ : the fair-coin probability of winning a best-of- $n$ of nested best-of- $m_1$ of … of best-of- $m_k$ is strictly less than the fair-coin probability of winning a best-of- $nm_1\cdots m_k$ .

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Part (b). -/
theorem part_b (q : ℝ) (ms : List ℕ) (n : ℕ) (hq0 : 1 / 2 < q) (hq1 : q < 1)
    (hms : ∀ m ∈ ms, Odd m ∧ 1 < m) (hne : ms ≠ []) (hn1 : 1 < n) :
    bestOfFairCoinWinProb n (nestedBestOfWinProb ms q)
      < bestOfFairCoinWinProb (n * ms.prod) q := by
  sorry

end GameSetMatch

Source

Mission statement 'Don't Label Twice: Game, Set, Match', part (b). 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. Explicit arguments: a real q, a list ms of natural numbers, and a natural n. Hypotheses:

1/2 < q (strict);
q < 1 (strict);
for every m that is a member of the list ms, m is odd and 1 < m (so every entry is an odd natural ≥ 3); this is a statement about list membership, so repeated entries are covered and the order of entries is irrelevant to the hypothesis;
ms is not the empty list;
1 < n, i.e. n ≥ 2. n is not required to be odd.

Conclusion:

F_n( Nest(ms, q) )  <  F_{n · ∏ms}(q)

Unfolding the two ingredients: Nest(ms, q) is the iterated composition in which the head of the list is the outermost application, so for ms = [m₁, …, m_k] (with k ≥ 1 by hypothesis 4) it equals B_{m₁}(B_{m₂}(⋯B_{m_k}(q)⋯)); and ∏ms = m₁·m₂·⋯·m_k, a product of odd naturals each ≥ 3, hence an odd natural ≥ 3. For a natural N and real x,

F_N(x) = [ Σ_{k ≤ N, 2k > N} C(N, k) x^k (1 − x)^(N − k) ]
         + (1/2) · [ if N is even then C(N, N/2) x^(N/2) (1 − x)^(N/2) else 0 ].

So the left-hand side is the strict-majority tail of n Bernoulli trials with parameter Nest(ms, q), plus one half of the exact-half term when n is even (and plus 0 when n is odd); the right-hand side is the strict-majority tail of n·∏ms trials with parameter q, plus one half of the exact-half term when n·∏ms is even. Since ∏ms is odd, n·∏ms is even exactly when n is even, so both sides carry a nonzero tie term under the same parity condition on n. The N/2 appearing in the tie term is floor division of naturals, but it is only used when N is even. The asserted inequality is strict, with the nested/smaller-count expression on the left. Hypotheses are satisfiable (q = 0.6, ms = [3], n = 2), so the statement is not vacuous. This theorem matches conjunct 2 of file 2.

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