Lemma 2, strict at r = 1

Proved

GameSetMatch.winLossAdv_nested_lt_one

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

label-aggregationmajority-voteprobabilityrandom-walktennis

Strict for $M,n>1$ , $r=1$ , $0<x<1$ — the explicit disagreement configurations of parts (a) and (b).

Preamble

import Definitions.Def_GameSetMatchInternal

Formal statement

namespace GameSetMatch

/-- Lemma 2, strict at `r = 1` for `M, n > 1` and `0 < x < 1`. -/
theorem winLossAdv_nested_lt_one (x : ℝ) (M n : ℕ) (hM : Odd M) (hM1 : 1 < M) (hn : 1 < n)
    (hx0 : 0 < x) (hx1 : x < 1) :
    winLossAdv 1 (majorityAdv M x) n < winLossAdv 1 x (n * M) := 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