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., @cite{denic-2023}'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.

noncomputable def RSA.IBR.falseMessageScore (G : InterpGame) : ℝ

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

Equations

• RSA.IBR.falseMessageScore G = -Real.log ↑(Fintype.card G.State) - 1

noncomputable def RSA.IBR.rsaS1Real (G : InterpGame) (α : ℝ) (s : G.State) : G.Message → ℝ

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

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

theorem RSA.IBR.rsa_speaker_to_ibr (G : InterpGame) [Nonempty G.Message] (s : G.State) (m : G.Message) (hTrue : G.meaning m s = true) (hUnique : ∀ (m' : G.Message), m' ≠ m → G.meaning m' s = true → G.informativity m > G.informativity m') (hInfPos : 0 < G.informativity m) : Filter.Tendsto (fun (α : ℝ) => rsaS1Real G α s m) Filter.atTop (nhds 1)

The Limit Theorem (@cite{franke-2011}, formalized):

As α → ∞, RSA S1 probability concentrates on the uniquely most informative true message — which is exactly the IBR-optimal message.

This follows from Softmax.tendsto_softmax_infty_at_max: softmax converges to 1 at the unique maximum as α → ∞.