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 (~680 lines of EG monotonicity) entirely for scalar games.

Key results:

• ibr_equals_exhMW: IBR FP support = exhMW (@cite{franke-2011} Proposition 4)
• ibr_converges_to_exhMW: IBR stabilizes at level 1 for scalar games

def RSA.IBR.isScalarGame (G : InterpGame) : Prop

A scalar game has truth sets that are totally ordered by inclusion. This is the structural condition required for Franke's Proposition 4 (IBR FP = exhMW). Without it, "dominated" messages (never optimal at any state) fall back to L0, breaking the exhMW characterization.

Equations

• RSA.IBR.isScalarGame G = ∀ (m₁ m₂ : G.Message), G.trueStates m₁ ⊆ G.trueStates m₂ ∨ G.trueStates m₂ ⊆ G.trueStates m₁

theorem RSA.IBR.scalar_trueMessages_total (G : InterpGame) (hScalar : isScalarGame G) (s₁ s₂ : G.State) : 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 RSA.IBR.scalar_minimal_messages_weaker (G : InterpGame) (hScalar : isScalarGame G) (m : G.Message) (s₀ : G.State) (hs₀ : G.meaning m s₀ = true) (hmin : ∀ (t : G.State), G.meaning m t = true → (G.trueMessages s₀).card ≤ (G.trueMessages t).card) (m' : G.Message) (hm' : G.meaning m' s₀ = true) : G.trueStates m ⊆ G.trueStates m'

In a scalar game, at the m-true state s₀ with fewest true messages, every message true at s₀ has trueStates ⊇ trueStates(m).

Proof: If ∃ m₁ ∈ trueMessages(s₁) \ trueMessages(s₂) and ∃ m₂ ∈ trueMessages(s₂) \ trueMessages(s₁), then trueStates(m₁) and trueStates(m₂) are incomparable, contradicting isScalarGame.

def RSA.IBR.toAlternatives (G : InterpGame) : Set (Prop' G.State)

Convert interpretation game to alternative set for exhaustification. Converts Bool meaning to Prop' by using equality with true.

Equations

• RSA.IBR.toAlternatives G = {x : Prop' G.State | ∃ (m : G.Message), (fun (s : G.State) => G.meaning m s = true) = x}

def RSA.IBR.prejacent (G : InterpGame) (m : G.Message) : Prop' G.State

The prejacent proposition for a message (Bool → Prop conversion)

Equations

• RSA.IBR.prejacent G m s = (G.meaning m s = true)

theorem RSA.IBR.trueMessages_ssubset_implies_ltALT (G : InterpGame) (s' s : G.State) (hss : G.trueMessages s' ⊂ G.trueMessages s) : s' <[toAlternatives G] s

Strict subset of trueMessages implies <_ALT under toAlternatives G.

theorem RSA.IBR.ltALT_implies_trueMessages_ssubset (G : InterpGame) (s' s : G.State) (hlt : s' <[toAlternatives G] s) : G.trueMessages s' ⊂ G.trueMessages s

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

def RSA.IBR.strongestAt (G : InterpGame) (m : G.Message) (s : G.State) : 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

• RSA.IBR.strongestAt G m s = (G.meaning m s = true ∧ ∀ (m' : G.Message), G.meaning m' s = true → G.trueStates m ⊆ G.trueStates m')

theorem RSA.IBR.strongestAt_implies_exhMW (G : InterpGame) (m : G.Message) (s : G.State) (h : strongestAt G m s) : Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

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

theorem RSA.IBR.exhMW_implies_strongestAt (G : InterpGame) (hScalar : isScalarGame G) (m : G.Message) (s : G.State) (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 RSA.IBR.strongestAt_iff_exhMW (G : InterpGame) (hScalar : isScalarGame G) (m : G.Message) (s : G.State) : 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.

theorem RSA.IBR.ibr_equals_exhMW (G : InterpGame) (H : HearerStrategy G) (_hFP : isIBRFixedPoint G H) (hPriorPos : ∀ (t : G.State), G.prior t > 0) (hFlatPrior : ∀ (t₁ t₂ : G.State), G.prior t₁ = G.prior t₂) (hScalar : isScalarGame G) (hDistinct : ∀ (m₁ m₂ : G.Message), G.trueStates m₁ = G.trueStates m₂ → m₁ = m₂) (hIBR : ∃ (k : ℕ), H = ibrN G (k + 1)) (m : G.Message) (s : G.State) : H.respond m s > 0 ↔ Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

IBR = exhMW (Main theorem — @cite{franke-2011}, Section 9.3)

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.

The proof chains through strongestAt as a bridge:

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

The left equivalence (ibrN_pos_iff_strongestAt) is proved by induction on the IBR sequence. The right equivalence (strongestAt_iff_exhMW) is pure order theory with no probabilities.

Restriction: Requires hIBR : ∃ k, H = ibrN G (k + 1), i.e., H is from the IBR iteration. The claim is false for arbitrary FPs of scalar games.

Two structural hypotheses:

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

theorem RSA.IBR.ibr_converges_to_exhMW (G : InterpGame) (hPriorPos : ∀ (s : G.State), G.prior s > 0) (hFlatPrior : ∀ (t₁ t₂ : G.State), G.prior t₁ = G.prior t₂) (hScalar : isScalarGame G) (hDistinct : ∀ (m₁ m₂ : G.Message), G.trueStates m₁ = G.trueStates m₂ → m₁ = m₂) (m : G.Message) (s : G.State) : (ibrN G 1).respond m s > 0 ↔ Exhaustification.exhMW (toAlternatives G) (prejacent G m) s

For scalar games, IBR stabilizes at level 1. No EG monotonicity needed.

The IBR sequence for scalar games reaches its correct behavior at level 1: ibrN G 1 already assigns positive probability exactly to exhMW-minimal states. This bypasses the general convergence machinery (ibr_reaches_fixed_point, ~350 lines of EG arithmetic) entirely.

def RSA.IBR.messageLevel (G : InterpGame) (m : G.Message) : Finset G.State

Level of a message: the states where m is the strongest true message.

In a scalar game, these form an equivalence class of the truth-pattern partition. IBR reasoning assigns positive probability to (m, s) iff s is in the level of m.

Equations

• RSA.IBR.messageLevel G m = {s : G.State | G.meaning m s = true ∧ ∀ (m' : G.Message), G.meaning m' s = true → G.trueStates m ⊆ G.trueStates m'}

def RSA.IBR.levelUniformPrior (G : InterpGame) : Prop

The prior is level-uniform if it is constant within each message's level.

This is the minimal condition for IBR = exhMW. Flat priors (∀ t₁ t₂, P(t₁) = P(t₂)) trivially satisfy this, but level-uniformity is strictly weaker.

Equations

• RSA.IBR.levelUniformPrior G = ∀ (m : G.Message) (s₁ s₂ : G.State), s₁ ∈ RSA.IBR.messageLevel G m → s₂ ∈ RSA.IBR.messageLevel G m → G.prior s₁ = G.prior s₂

def RSA.IBR.isEquivalenceClassGame (G : InterpGame) : Prop

An equivalence class game has states that are truth-pattern equivalence classes: each message level is a singleton set. In such games, levelUniformPrior holds for ANY positive prior (there's only one state per level, so the uniformity condition is vacuous).

@cite{franke-2011}'s Theorem 1 shows that for equivalence class games, heavy = light systems — the prior doesn't affect the interpretation.

Equations

• RSA.IBR.isEquivalenceClassGame G = ∀ (m : G.Message), (RSA.IBR.messageLevel G m).Nonempty → (RSA.IBR.messageLevel G m).card = 1

theorem RSA.IBR.flat_prior_is_levelUniform (G : InterpGame) (hFlat : ∀ (t₁ t₂ : G.State), G.prior t₁ = G.prior t₂) : levelUniformPrior G

Flat priors are level-uniform.

theorem RSA.IBR.eqclass_levelUniform (G : InterpGame) (hEq : isEquivalenceClassGame G) : levelUniformPrior G

Equivalence class games have level-uniform priors for any prior.