Information-Theoretic Foundations of RSA

@cite{cover-thomas-2006} @cite{frank-goodman-2012} @cite{zaslavsky-hu-levy-2020}

Re-exports domain-agnostic information-theoretic primitives from Core.InformationTheory into the RSA.InformationTheory namespace, and adds RSA-specific definitions (RSALevel).

The ℚ-based RSA evaluation infrastructure (RSAScenarioQ, RSA.Eval, RSA.Q) has been removed. This file retains the re-exported information-theoretic definitions (entropy, KL divergence, log2Approx) that are used by other modules (e.g., ArgumentativeStrength), but all RSAScenarioQ-dependent computations and dynamics have been removed.

Original Results (To Be Re-derived with RSAConfig)

1. RSA as alternating maximization: RSA optimizes G_α = H_S(U|M) + α·E[V_L]
2. G_α monotonicity: G_α(S_t, L_t) ≤ G_α(S_{t+1}, L_{t+1})
3. Critical α = 1: Phase transition at α = 1
4. Utility non-monotonicity: E[V_L] can decrease even as G_α increases

inductive RSA.InformationTheory.RSALevel : Type

RSA iteration level.

Track the depth of pragmatic reasoning:

• L0 = literal listener
• S1 = pragmatic speaker (responds to L0)
• L1 = pragmatic listener (responds to S1)
• S2 = second-order speaker (responds to L1)
• etc.

• L : ℕ → RSALevel
• S : ℕ → RSALevel

instance RSA.InformationTheory.instDecidableEqRSALevel : DecidableEq RSALevel

Equations

• RSA.InformationTheory.instDecidableEqRSALevel = RSA.InformationTheory.instDecidableEqRSALevel.decEq

def RSA.InformationTheory.instDecidableEqRSALevel.decEq (x✝ x✝¹ : RSALevel) : Decidable (x✝ = x✝¹)

Equations

• RSA.InformationTheory.instDecidableEqRSALevel.decEq (RSA.InformationTheory.RSALevel.L a) (RSA.InformationTheory.RSALevel.L b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RSA.InformationTheory.instDecidableEqRSALevel.decEq (RSA.InformationTheory.RSALevel.L a) (RSA.InformationTheory.RSALevel.S a_1) = isFalse ⋯
• RSA.InformationTheory.instDecidableEqRSALevel.decEq (RSA.InformationTheory.RSALevel.S a) (RSA.InformationTheory.RSALevel.L a_1) = isFalse ⋯
• RSA.InformationTheory.instDecidableEqRSALevel.decEq (RSA.InformationTheory.RSALevel.S a) (RSA.InformationTheory.RSALevel.S b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance RSA.InformationTheory.instBEqRSALevel : BEq RSALevel

Equations

• RSA.InformationTheory.instBEqRSALevel = { beq := RSA.InformationTheory.instBEqRSALevel.beq }

def RSA.InformationTheory.instBEqRSALevel.beq : RSALevel → RSALevel → Bool

Equations

• RSA.InformationTheory.instBEqRSALevel.beq (RSA.InformationTheory.RSALevel.L a) (RSA.InformationTheory.RSALevel.L b) = (a == b)
• RSA.InformationTheory.instBEqRSALevel.beq (RSA.InformationTheory.RSALevel.S a) (RSA.InformationTheory.RSALevel.S b) = (a == b)
• RSA.InformationTheory.instBEqRSALevel.beq x✝¹ x✝ = false

def RSA.InformationTheory.instReprRSALevel.repr : RSALevel → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

instance RSA.InformationTheory.instReprRSALevel : Repr RSALevel

Equations

• RSA.InformationTheory.instReprRSALevel = { reprPrec := RSA.InformationTheory.instReprRSALevel.repr }