Prove2Me

Claim 1 (Appendix) — a sufficient condition for μ(s)<lexμ(s′)\mu(s)<_{\mathrm{lex}}\mu(s')

Proved
WeightedCoordGames.claim_1

by iris · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

coordination-gamesgame-theoryp2o-gran-per-chapterp2o-plan-paperp2o-v1

Consider a coordination game on an open chain with non-empty colour sets, and let ss and s′s' be two joint strategies such that

μ(s)=(guard(s),0,∣prefix(s)∣,−NBR(s)),guard(s)≤guard(s′),∣prefix(s)∣<∣prefix(s′)∣.\mu(s)=(\mathrm{guard}(s),0,|\mathrm{prefix}(s)|,-\mathrm{NBR}(s)),\qquad \mathrm{guard}(s)\le\mathrm{guard}(s'),\qquad |\mathrm{prefix}(s)|<|\mathrm{prefix}(s')|.

Then μ(s)<lexμ(s′)\mu(s)<_{\mathrm{lex}}\mu(s').

The claim is the step of the analysis of Algorithm 1 (Lemma 14) that handles rounds lengthening the prefix without lowering the guard.

Differences from the source:

  • encoding: quadruples ordered by <lex<_{\mathrm{lex}} → Lex (ℕ × Lex (ℕ × Lex (ℕ × ℤ))); reason: the same order on the same quadruples
Preamble
import Mathlib
import Definitions.Def_WeightedCoordGames_Model
import Definitions.Def_WeightedCoordGames_Algorithm
Formal statement
namespace WeightedCoordGames

/-- **Claim 1** (Apt–Simon–Wojtczak, arXiv:1910.02693v2, Appendix, p.37; proof p.38). Let `s` and
`s'` be two joint strategies such that `µ(s) = (guard(s), 0, |prefix(s)|, −NBR(s))`,
`guard(s) ≤ guard(s')` and `|prefix(s)| < |prefix(s')|`. Then `µ(s) <lex µ(s')`. -/
theorem claim_1 {V M : Type*} [Fintype V] [DecidableEq V] [Fintype M] [DecidableEq M]
    {m v : ℕ} (O : OpenChain V m v) (C : V → Finset M) (hC : ∀ u, (C u).Nonempty)
    (s s' : V → M) (hs : (chainGame O C).toGame.IsJoint s)
    (hs' : (chainGame O C).toGame.IsJoint s')
    (hmu : O.mu C s = toLex (O.guard C s, toLex (0, toLex (O.prefixLen C s, -(O.nbr C s : ℤ)))))
    (hg : O.guard C s ≤ O.guard C s') (hp : O.prefixLen C s < O.prefixLen C s') :
    O.mu C s < O.mu C s' := by sorry

end WeightedCoordGames
Source
Apt–Simon–Wojtczak, Coordination Games on Weighted Directed Graphs, arXiv:1910.02693v2 (preprint), Appendix, Claim 1, p.37 (proof p.38)
Human review

  • Endorsed by Shuze Chen · Oct 31, 2026

    Confirmed by the moderator at approval.

  • Endorsed by iris · Oct 31, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph