IBR for Scalar Games

For scalar interpretation games (truth sets totally ordered by inclusion), IBR converges to exhaustive interpretation (exhMW) at level 1.

The proof chains through strongestAt as a bridge predicate:

ibrN > 0  ↔  strongestAt  ↔  exhMW
(rational choice)        (order theory)

The left equivalence is proved by induction on the IBR sequence (ibrN_pos_iff_strongestAt). The right equivalence is pure order theory with no probabilities (strongestAt_iff_exhMW). This bypasses the general convergence machinery in Convergence.lean entirely for scalar games.

Key results:

• ibr_equals_exhMW: at every IBR level ≥ 1, the listener's support for a message is its exhMW interpretation — the scalar case where [Fra11]'s Fact 1 (§10, R₁(mS) ⊆ ExhMM(S)) sharpens to an equality
• ibr_converges_to_exhMW: IBR stabilizes at level 1 for scalar games (a derived strengthening; the paper states Fact 1 for R₁ only)

Franke writes ExhMM (minimal models) for the operator linglib names exhMW (minimal worlds, the project-canonical name).

Scalar games

def Franke2011.isScalarGame {T : Type u_1} {M : Type u_2} [Fintype T] (G : InterpGame T M) : Prop

A scalar game has truth sets that are totally ordered by inclusion — the Horn-scale structure under which [Fra11]'s Fact 1 (R₁(mS) ⊆ ExhMM(S), §10) sharpens to an equality. Without it, "dominated" messages (never optimal at any state) fall back to the literal listener, breaking the exhMW characterization.

Equations

• Franke2011.isScalarGame G = ∀ (m₁ m₂ : M), G.trueStates m₁ ⊆ G.trueStates m₂ ∨ G.trueStates m₂ ⊆ G.trueStates m₁

theorem Franke2011.scalar_trueMessages_total {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] (G : InterpGame T M) (hScalar : isScalarGame G) (s₁ s₂ : T) : G.trueMessages s₁ ⊆ G.trueMessages s₂ ∨ G.trueMessages s₂ ⊆ G.trueMessages s₁

In a scalar game, trueMessages are totally ordered: for any two states, one's true messages are a subset of the other's.

Proof: If ∃ m₁ ∈ trueMessages(s₁) \ trueMessages(s₂) and ∃ m₂ ∈ trueMessages(s₂) \ trueMessages(s₁), then trueStates(m₁) and trueStates(m₂) are incomparable (s₁ distinguishes them one way, s₂ the other), contradicting isScalarGame.

theorem Franke2011.scalar_minimal_messages_weaker {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] (G : InterpGame T M) (hScalar : isScalarGame G) (m : M) (s₀ : T) (hmin : ∀ (t : T), G.meaning m t → (G.trueMessages s₀).card ≤ (G.trueMessages t).card) (m' : M) (hm' : G.meaning m' s₀) : G.trueStates m ⊆ G.trueStates m'

In a scalar game, at an m-true state with fewest true messages, every message true there is weaker than m: its truth set contains trueStates(m).

Alternative-set bridge

def Franke2011.toAlternatives {T : Type u_1} {M : Type u_2} (G : InterpGame T M) : Set (Set T)

Convert interpretation game to alternative set for exhaustification.

Equations

• Franke2011.toAlternatives G = {x : Set T | ∃ (m : M), (fun (s : T) => G.meaning m s) = x}

def Franke2011.prejacent {T : Type u_1} {M : Type u_2} (G : InterpGame T M) (m : M) : Set T

The prejacent proposition for a message.

Equations

• Franke2011.prejacent G m s = G.meaning m s

theorem Franke2011.trueMessages_ssubset_implies_ltALT {T : Type u_1} {M : Type u_2} [Fintype M] (G : InterpGame T M) (s' s : T) (hss : G.trueMessages s' ⊂ G.trueMessages s) : s' <[toAlternatives G] s

Strict subset of trueMessages implies <_ALT under toAlternatives G.

theorem Franke2011.ltALT_implies_trueMessages_ssubset {T : Type u_1} {M : Type u_2} [Fintype M] (G : InterpGame T M) (s' s : T) (hlt : s' <[toAlternatives G] s) : G.trueMessages s' ⊂ G.trueMessages s

Key lemma: s' <_ALT s implies trueMessages s' ⊂ trueMessages s.

The strongestAt bridge

def Franke2011.strongestAt {T : Type u_1} {M : Type u_2} [Fintype T] (G : InterpGame T M) (m : M) (s : T) : Prop

strongestAt G m s — "m is the strongest true message at s": m is true at s, and trueStates(m) is contained in trueStates(m') for every other message m' true at s.

In a scalar game, this picks out the unique most informative message. This predicate is the purely set-theoretic bridge between the probabilistic IBR sequence and the logical exhMW operator:

ibrN > 0 ↔ strongestAt ↔ exhMW

The left equivalence is rational choice (proved via ibrN_opt_singleton). The right equivalence is pure order theory (no probabilities).

Equations

• Franke2011.strongestAt G m s = (G.meaning m s ∧ ∀ (m' : M), G.meaning m' s → G.trueStates m ⊆ G.trueStates m')

theorem Franke2011.strongestAt_implies_exhMW {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] (G : InterpGame T M) (m : M) (s : T) (h : strongestAt G m s) : Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

Forward: strongestAt → exhMW. Pure order theory, no probabilities.

theorem Franke2011.exhMW_implies_strongestAt {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] (G : InterpGame T M) (hScalar : isScalarGame G) (m : M) (s : T) (h : Exhaustification.exhMW (toAlternatives G) (prejacent G m) s) : strongestAt G m s

Backward: exhMW → strongestAt (requires scalar game).

exhMW-minimality → card-minimality (via scalar totality) → strongest (via scalar_minimal_messages_weaker).

theorem Franke2011.strongestAt_iff_exhMW {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] (G : InterpGame T M) (hScalar : isScalarGame G) (m : M) (s : T) : strongestAt G m s ↔ Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

For scalar games, strongestAt ↔ exhMW. The purely set-theoretic core of the IBR = exhMW theorem. No probabilities, no EG monotonicity.

IBR positivity at scalar games

Main theorems

theorem Franke2011.ibr_equals_exhMW {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] (G : InterpGame T M) (hScalar : isScalarGame G) (hPriorPos : ∀ (t : T), G.prior t > 0) (hFlatPrior : ∀ (t₁ t₂ : T), G.prior t₁ = G.prior t₂) (hDistinct : Function.Injective G.trueStates) (H : M → T → ℚ) (hIBR : ∃ (k : ℕ), H = ibrN G (k + 1)) (m : M) (s : T) : H m s > 0 ↔ Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

IBR = exhMW for scalar games ([Fra11] Fact 1, §10, sharpened).

At any IBR level k+1 of a scalar interpretation game, the listener's positive-probability states for message m are exactly the exhMW-minimal states.

Franke's Fact 1 states containment (R₁(mS) ⊆ ExhMM(S)) for the level-1 receiver, with equality under a "homogeneity" condition. For scalar games the nested truth sets deliver equality at every level ≥ 1, which is what is proved here — a per-level statement, not a fixed-point theorem.

The proof chains through strongestAt as a bridge:

ibrN > 0  ↔  strongestAt  ↔  exhMW
(rational choice)        (order theory)

Restriction: requires hIBR : ∃ k, H = ibrN G (k + 1), i.e. H arises from the IBR iteration; the claim is false for arbitrary hearer strategies.

Two structural hypotheses:

• isScalarGame: truth sets are totally ordered by inclusion (nested)
• hDistinct: no two messages have identical truth sets

theorem Franke2011.ibr_converges_to_exhMW {T : Type u_1} {M : Type u_2} [Fintype T] [Fintype M] [DecidableEq M] (G : InterpGame T M) (hScalar : isScalarGame G) (hPriorPos : ∀ (t : T), G.prior t > 0) (hFlatPrior : ∀ (t₁ t₂ : T), G.prior t₁ = G.prior t₂) (hDistinct : Function.Injective G.trueStates) (m : M) (s : T) : ibrN G 1 m s > 0 ↔ Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

For scalar games, IBR stabilizes at level 1: ibrN G 1 already assigns positive probability exactly to the exhMW-minimal states, bypassing the general convergence machinery (ibr_reaches_fixed_point in Convergence.lean).

The stabilization claim is derived here; [Fra11] states Fact 1 for the level-1 receiver only.