Part (d): randomly scored sets, strict win only

Proved

GameSetMatch.part_d

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

label-aggregationmajority-voteprobabilityrandom-walktennis

As part (c), but the match is won only with a strictly greater match score, and $b\ge1/2$ is assumed. The probability of winning from $n$ scored nested sets is strictly less than from $nm_1\cdots m_k$ scored single points.

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Part (d). -/
theorem part_d (a b c q : ℝ) (ms : List ℕ) (n : ℕ)
    (ha : 0 ≤ a) (hb : 1 / 2 ≤ b) (hc : 0 ≤ c) (habc : a + b + c = 1) (hca : c < a)
    (hq0 : 1 / 2 < q) (hq1 : q < 1)
    (hms : ∀ m ∈ ms, Odd m ∧ 1 < m) (hne : ms ≠ []) (hn1 : 1 < n) :
    strictWinProb (scoredSetLaw a b c (nestedBestOfWinProb ms q)) n
      < strictWinProb (scoredSetLaw a b c q) (n * ms.prod) := by
  sorry

end GameSetMatch

Source

Mission statement 'Don't Label Twice: Game, Set, Match', part (d). 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: four reals a, b, c, q, a list ms of naturals, and a natural n. Hypotheses, in order:

0 ≤ a (non-strict);
1/2 ≤ b (non-strict — this is the one hypothesis that differs from file 5, where the corresponding assumption is only 0 ≤ b);
0 ≤ c (non-strict);
a + b + c = 1;
c < a (strict);
1/2 < q (strict);
q < 1 (strict);
every member m of ms is odd and satisfies 1 < m;
ms ≠ [];
1 < n (no oddness requirement on n).

Hypotheses 1–5 together force a + c = 1 − b ≤ 1/2 with 0 ≤ c < a, hence 0 < a ≤ 1/2 and 1/2 ≤ b ≤ 1. They are satisfiable (a = 0.3, b = 0.6, c = 0.1), so the statement is not vacuous.

Conclusion:

S( ν[a,b,c; Nest(ms, q)] , n )   <   S( ν[a,b,c; q] , n · ∏ms )

with ν_r and L^{ν_r}_N exactly as unfolded in file 5 (three-point weights r·a + (1−r)·c at +1, r·c + (1−r)·a at −1, b at 0, zero elsewhere; N-step recursion from the indicator of 0), and with

S(ν, N) = Σ_{z = 1}^{N} L^ν_N(z),

the sum over integers z from 1 to N inclusive — no half-tie term is added on either side, which is the second difference from file 5. Explicitly the claim is

Σ_{z=1}^{n} L^{ν_R}_n(z)   <   Σ_{z=1}^{n·∏ms} L^{ν_q}_{n·∏ms}(z),

where R = Nest(ms, q) is the head-outermost composition B_{m₁}(⋯B_{m_k}(q)⋯) and ∏ms is the product of the entries of ms. As in file 5, both sides share a, b, c; the left side uses the nested parameter R with n convolution steps and sums z from 1 to n, while the right side uses the bare q with n·∏ms steps and sums z from 1 to n·∏ms. The inequality is strict and oriented with the nested/fewer-steps quantity on the left. This theorem matches conjunct 4 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