RSA–IBR Bridge: Softmax → Argmax Limit

As the rationality parameter α → ∞, RSA S1 concentrates on the IBR-optimal message. This is because RSA S1 is a softmax over log-informativity scores, and softmax → argmax as α → ∞ (Softmax.tendsto_softmax_infty_at_max).

This bridges RSA's probabilistic speaker to IBR's categorical best-response operator. Combined with ibr_equals_exhMW (in ScalarGames.lean), the full limit chain is:

RSA S1 (softmax) ──α→∞──> IBR S1 (argmax) ────> exhMW ──closure──> exhIE

The practical consequence: any phenomenon that exhaustification-based theories cannot distinguish (e.g., [Den23]'s domain-size-invariant inference puzzle), RSA also cannot distinguish in the high-rationality limit. Probabilistic mechanisms (like informativeness-based pruning) are the only way out.

def Franke2011.informativity {T : Type u_1} {M : Type u_2} [Fintype T] (G : InterpGame T M) (m : M) : ℚ

Informativity of a message: reciprocal of its true-state count (0 for contradictory messages).

Equations

• Franke2011.informativity G m = if (G.trueStates m).card = 0 then 0 else 1 / ↑(G.trueStates m).card

noncomputable def Franke2011.falseMessageScore {T : Type u_1} [Fintype T] : ℝ

Floor score for false messages. Uses -log(|T|) - 1, which is always below the minimum possible log-informativity for any true message.

Equations

• Franke2011.falseMessageScore = -Real.log ↑(Fintype.card T) - 1

noncomputable def Franke2011.rsaS1Real {T : Type u_1} {M : Type u_2} [Fintype T] (G : InterpGame T M) [Fintype M] (α : ℝ) (s : T) : M → ℝ

RSA S1 probability (real version for limit theorems).

RSA S1 is exactly softmax over log-informativity scores: rsaS1(m | s) = exp(α · log(inf(m))) / Σ exp(α · log(inf(m'))) = inf(m)^α / Σ inf(m')^α = softmax(log ∘ inf, α)(m)

Equations

• Franke2011.rsaS1Real G α s = Core.softmax (α • fun (m : M) => if G.meaning m s then Real.log ↑(Franke2011.informativity G m) else Franke2011.falseMessageScore)

theorem Franke2011.rsa_speaker_to_ibr {T : Type u_1} {M : Type u_2} [Fintype T] (G : InterpGame T M) [Fintype M] [DecidableEq M] [Nonempty M] (s : T) (m : M) (hTrue : G.meaning m s) (hUnique : ∀ (m' : M), m' ≠ m → G.meaning m' s → informativity G m > informativity G m') : Filter.Tendsto (fun (α : ℝ) => rsaS1Real G α s m) Filter.atTop (nhds 1)

Softmax → argmax limit. As α → ∞, RSA S1 probability concentrates on the uniquely most informative true message — exactly the argmax choice of [Fra11]'s IBR speaker.

This bridge is the formalizer's, not a result of [Fra11]: RSA postdates the paper ([FG12]). It follows from Softmax.tendsto_softmax_infty_at_max: softmax converges to 1 at the unique maximum as α → ∞.