IBR Convergence

General convergence proof for Iterated Best Response (@cite{franke-2011} Appendix B.1).

Expected gain (EG) is monotone non-decreasing along the IBR sequence (Lemma 3), and the strategy space is finite (pigeonhole), so IBR must reach a fixed point (Theorem 3).

This machinery is not needed for scalar games, where ibr_converges_to_exhMW (in ScalarGames.lean) shows IBR stabilizes at level 1. It is needed for general (non-scalar) interpretation games.

theorem RSA.IBR.eg_speaker_improvement (G : InterpGame) (S_old S_new : SpeakerStrategy G) (H : HearerStrategy G) (hBR : S_new = SpeakerStrategy.bestResponse G H) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (hSNonneg : ∀ (s : G.State) (m : G.Message), S_old.choose s m ≥ 0) (hSSum : ∀ (s : G.State), ∑ m : G.Message, S_old.choose s m ≤ 1) (hSTruth : ∀ (s : G.State) (m : G.Message), G.meaning m s = false → S_old.choose s m = 0) (_hHNonneg : ∀ (m : G.Message) (s : G.State), H.respond m s ≥ 0) : expectedGain G S_old H ≤ expectedGain G S_new H

Lemma 3a: best-response speaker improves EG.

At each state t, bestResponse maximizes ∑_m S(t,m) * H(m,t) by concentrating all probability on messages that maximize H(m,t). Any valid S_old achieves at most maxU(t), which is exactly what S_new achieves.

theorem RSA.IBR.eg_ibr_monotone (G : InterpGame) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (hPriorSum : Finset.univ.sum G.prior = 1) (n : ℕ) : expectedGain G (speakerUpdate G (ibrN G n)) (ibrN G n) ≤ expectedGain G (speakerUpdate G (ibrN G (n + 1))) (ibrN G (n + 1))

Franke's Lemma 3: EG is monotone non-decreasing along the IBR sequence.

The combined effect of speaker best response + hearer argmax response produces a strategy pair with at least as high expected gain: EG(S_{n+1}, L_n) ≤ EG(S_{n+2}, L_{n+1})

Proof decomposes into two steps via the intermediate EG(S_{n+1}, L_{n+1}):

Speaker step (proved via eg_speaker_improvement): EG(S_{n+1}, L_{n+1}) ≤ EG(S_{n+2}, L_{n+1}) because S_{n+2} = bestResponse(L_{n+1}) achieves at least as much EG against L_{n+1} as any valid speaker strategy.

Hearer step (proved via eg_hearerBR_improvement): EG(S_{n+1}, L_n) ≤ EG(S_{n+1}, L_{n+1}) because L_{n+1} = hearerBR(S_{n+1}) is the argmax best response. Per-message: Σ_t w(t)·H_old(m,t) ≤ maxW (from per_message_bound) and Σ_t w(t)·hearerBR(m,t) ≥ maxW (argmax achieves).

theorem RSA.IBR.eg_bounded (G : InterpGame) (S : SpeakerStrategy G) (H : HearerStrategy G) (hPriorSum : Finset.univ.sum G.prior = 1) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (hSNonneg : ∀ (s : G.State) (m : G.Message), S.choose s m ≥ 0) (hSSum : ∀ (s : G.State), ∑ m : G.Message, S.choose s m ≤ 1) (hHBound : ∀ (m : G.Message) (s : G.State), H.respond m s ≤ 1) (_hHNonneg : ∀ (m : G.Message) (s : G.State), H.respond m s ≥ 0) : expectedGain G S H ≤ 1

Expected gain is bounded above by 1 (probability of perfect communication).

theorem RSA.IBR.ibr_reaches_fixed_point (G : InterpGame) (hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (hPriorPos : ∀ (s : G.State), G.prior s > 0) (hPriorSum : Finset.univ.sum G.prior = 1) : ∃ (n : ℕ), isIBRFixedPoint G (ibrN G n)

Theorem 3: IBR converges. EG is monotone increasing and bounded ⟹ fixed point.

The proof uses cycle elimination: since the hearer strategy space is finite, the IBR sequence must repeat. EG monotonicity forces EG constant on the cycle. Constant EG implies optimalMessages containment at each step. Around the cycle, containment of finite sets gives equality. Equal optimalMessages gives equal bestResponse speakers, hence equal hearer BR, giving a consecutive repeat, which is a fixed point.