A nested set is no better than a flat best-of of the same length

Proved

GameSetMatch.nested_adv_le_majorityAdv

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

label-aggregationmajority-voteprobabilityrandom-walktennis

For odd set sizes and $x\in[0,1]$ : the iterated advantage $H_{m_1}(\cdots H_{m_k}(x))$ is at most $H_{m_1\cdots m_k}(x)$ (equation (5)).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- The advantage of one nested best-of-`m₁` of … of best-of-`mₖ` is at most that of a flat
best-of-`(m₁⋯mₖ)`. -/
theorem nested_adv_le_majorityAdv (ms : List ℕ) (hms : ∀ m ∈ ms, Odd m) (x : ℝ)
    (hx0 : 0 ≤ x) (hx1 : x ≤ 1) :
    ms.foldr (fun m y => majorityAdv m y) x ≤ majorityAdv ms.prod x := by
  sorry

end GameSetMatch

Source

four_part_nested_best_of_proof.md (private notes, 3 Sep 2026)

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