Canonical RSA pipeline

The single L0 → S1 → L1 pipeline for Rational Speech Act models [FG12] [Deg23], built directly on the Core/Probability shell with no bundled configuration.

The pragmatic speaker S1 is the softmax of a utility score : St → U → EReal mapping a speaker state (a world, or a world × latent pair) to a per-utterance utility; an utterance is inapplicable exactly when its utility is ⊥ (softmax weight 0). The standard informativity utility is rsaUtility = α·(log L0 − cost), but any utility plugs in the same way — action-utility ([HTB+25]) and belief-utility speakers included. The pragmatic listener L1 is the joint Bayesian posterior over world × latent, with marginals .fst/.snd.

Positivity is supplied once as a ViableSpeaker instance (no utterance has infinite utility; every state has an applicable utterance), so per-paper speakers carry no tsum ≠ 0 / ≠ ⊤ plumbing.

A prediction is stated in the *_prefers_iff vocabulary, each a one-line wrapper over a Core/Probability decomposition lemma (PMF.softmax_lt_iff_score_lt, PMF.posterior_fst_lt_iff): the partition and the marginal cancel, leaving a comparison of utilities / conditional-joint sums.

Main definitions

• RSA.Canonical.ViableSpeaker — positivity mixin discharging the softmax obligations.
• RSA.Canonical.S1 — pragmatic speaker, PMF.softmax of a viable utility.
• RSA.Canonical.rsaUtility — the standard informativity utility α·(log L0 − cost).
• RSA.Canonical.L1 — pragmatic listener, joint PMF.posterior over world × latent.
• RSA.Canonical.L1Intent — pair-choice pragmatic listener: the speaker chooses an (utterance, latent) pair, the listener observes only the utterance (PMF.emissionPosterior).
• RSA.Canonical.ratS1 — the propositional-model speaker as an exact rational.

Main statements

• RSA.Canonical.S1_prefers_iff — speaker preference ↔ utility comparison.
• RSA.Canonical.L1_world_prefers_iff / L1_latent_prefers_iff — listener marginal preference ↔ conditional-joint-sum comparison.
• RSA.Canonical.S1_eq_ofReal — the power-utility speaker over a propositional model equals ENNReal.ofReal of ratS1.

Implementation notes

Non-latent models take St = W and use the foundation PMF.posterior_lt_iff_score_lt directly (the latent = Unit collapse). The IsCovering ⇒ ViableSpeaker (rsaUtility …) bridge for standard informativity speakers is added when first needed.

Pragmatic speaker

class RSA.Canonical.ViableSpeaker {St : Type u_1} {U : Type u_2} (score : St → U → EReal) : Prop

A speaker utility score : St → U → EReal is viable when no utterance has infinite utility and every state has at least one finite-utility (applicable) utterance — precisely the conditions under which the softmax speaker is well-defined. Supplied as an instance, it discharges the PMF.softmax positivity obligations so per-paper speakers need no explicit tsum-positivity plumbing.

• no_top (s : St) (u : U) : score s u ≠ ⊤

  No utterance has +∞ utility.

• some_finite (s : St) : ∃ (u : U), score s u ≠ ⊥

  Every state has at least one applicable (finite-utility) utterance.

noncomputable def RSA.Canonical.S1 {St : Type u_1} {U : Type u_2} [Fintype U] (score : St → U → EReal) [ViableSpeaker score] (s : St) : PMF U

The canonical pragmatic speaker at state s: the softmax of a viable utility. The single speaker the library instantiates; the standard informativity form is rsaUtility, while action/belief-utility speakers supply their own score.

Equations

• RSA.Canonical.S1 score s = PMF.softmax (score s) ⋯ ⋯

theorem RSA.Canonical.S1_prefers_iff {St : Type u_1} {U : Type u_2} [Fintype U] (score : St → U → EReal) [ViableSpeaker score] (s : St) (u₁ u₂ : U) : (S1 score s) u₁ < (S1 score s) u₂ ↔ score s u₁ < score s u₂

Cross-utterance prediction: the speaker prefers u₂ to u₁ at state s iff u₂ has the higher utility. The partition function cancels.

theorem RSA.Canonical.S1_prefers_le_iff {St : Type u_1} {U : Type u_2} [Fintype U] (score : St → U → EReal) [ViableSpeaker score] (s : St) (u₁ u₂ : U) : (S1 score s) u₁ ≤ (S1 score s) u₂ ↔ score s u₁ ≤ score s u₂

≤ companion of S1_prefers_iff.

theorem RSA.Canonical.S1_eq_iff {St : Type u_1} {U : Type u_2} [Fintype U] (score : St → U → EReal) [ViableSpeaker score] (s : St) (u₁ u₂ : U) : (S1 score s) u₁ = (S1 score s) u₂ ↔ score s u₁ = score s u₂

= companion of S1_prefers_iff: score symmetry.

theorem RSA.Canonical.S1_ne_zero {St : Type u_1} {U : Type u_2} [Fintype U] (score : St → U → EReal) [ViableSpeaker score] {s : St} {u : U} (h : score s u ≠ ⊥) : (S1 score s) u ≠ 0

The speaker assigns positive probability to any applicable (finite-utility) utterance — the witness for discharging L1 marginal positivity.

Standard informativity utility

noncomputable def RSA.Canonical.rsaUtility {W : Type u_1} {U : Type u_2} (L0 : W → U → ENNReal) (cost : U → ℝ) (α : ℝ) (w : W) (u : U) : EReal

The standard informativity utility α·(log L0(u | w) − cost u), EReal-valued so an inapplicable utterance (L0 = 0 ⇒ log = ⊥) is ⊥ (softmax weight 0). Plug into S1; the rpow speaker RSA.S1Belief is the cost-free case.

Equations

• RSA.Canonical.rsaUtility L0 cost α w u = ↑α * ((L0 w u).log - ↑(cost u))

Pragmatic listener

noncomputable def RSA.Canonical.L1 {W : Type u_1} {Lat : Type u_2} {U : Type u_3} (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) : PMF (W × Lat)

The canonical pragmatic listener: the joint Bayesian posterior over world × latent given the observed utterance u. World/latent marginals are .fst/.snd.

Equations

• RSA.Canonical.L1 S joint u h = PMF.posterior S joint u h

theorem RSA.Canonical.L1_world_prefers_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq W] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (w₁ w₂ : W) : (L1 S joint u h).fst w₁ < (L1 S joint u h).fst w₂ ↔ ∑ l : Lat, joint (w₁, l) * (S (w₁, l)) u < ∑ l : Lat, joint (w₂, l) * (S (w₂, l)) u

Cross-world prediction: marginalising the latent, L1 favours world w₂ over w₁ iff the conditional-joint sums favour it.

theorem RSA.Canonical.L1_world_prefers_le_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq W] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (w₁ w₂ : W) : (L1 S joint u h).fst w₁ ≤ (L1 S joint u h).fst w₂ ↔ ∑ l : Lat, joint (w₁, l) * (S (w₁, l)) u ≤ ∑ l : Lat, joint (w₂, l) * (S (w₂, l)) u

≤ companion of L1_world_prefers_iff.

theorem RSA.Canonical.L1_world_eq_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq W] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (w₁ w₂ : W) : (L1 S joint u h).fst w₁ = (L1 S joint u h).fst w₂ ↔ ∑ l : Lat, joint (w₁, l) * (S (w₁, l)) u = ∑ l : Lat, joint (w₂, l) * (S (w₂, l)) u

= companion of L1_world_prefers_iff: conditional-joint-sum symmetry.

theorem RSA.Canonical.L1_latent_prefers_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq Lat] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (l₁ l₂ : Lat) : (L1 S joint u h).snd l₁ < (L1 S joint u h).snd l₂ ↔ ∑ w : W, joint (w, l₁) * (S (w, l₁)) u < ∑ w : W, joint (w, l₂) * (S (w, l₂)) u

Cross-latent prediction: marginalising the world, L1 favours latent l₂ over l₁ iff the conditional-joint sums favour it.

theorem RSA.Canonical.L1_latent_prefers_le_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq Lat] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (l₁ l₂ : Lat) : (L1 S joint u h).snd l₁ ≤ (L1 S joint u h).snd l₂ ↔ ∑ w : W, joint (w, l₁) * (S (w, l₁)) u ≤ ∑ w : W, joint (w, l₂) * (S (w, l₂)) u

≤ companion of L1_latent_prefers_iff.

theorem RSA.Canonical.L1_latent_eq_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq Lat] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (l₁ l₂ : Lat) : (L1 S joint u h).snd l₁ = (L1 S joint u h).snd l₂ ↔ ∑ w : W, joint (w, l₁) * (S (w, l₁)) u = ∑ w : W, joint (w, l₂) * (S (w, l₂)) u

= companion of L1_latent_prefers_iff: conditional-joint-sum symmetry.

theorem RSA.Canonical.L1_uniform_world_prefers_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq W] [Nonempty (W × Lat)] (S : W × Lat → PMF U) (u : U) (h : PMF.marginal S (PMF.uniformOfFintype (W × Lat)) u ≠ 0) (w₁ w₂ : W) : (L1 S (PMF.uniformOfFintype (W × Lat)) u h).fst w₁ < (L1 S (PMF.uniformOfFintype (W × Lat)) u h).fst w₂ ↔ ∑ l : Lat, (S (w₁, l)) u < ∑ l : Lat, (S (w₂, l)) u

At a uniform joint prior the prior cancels: world preference reduces to comparing pooled speaker sums over the latent.

theorem RSA.Canonical.L1_uniform_latent_prefers_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [DecidableEq Lat] [Nonempty (W × Lat)] (S : W × Lat → PMF U) (u : U) (h : PMF.marginal S (PMF.uniformOfFintype (W × Lat)) u ≠ 0) (l₁ l₂ : Lat) : (L1 S (PMF.uniformOfFintype (W × Lat)) u h).snd l₁ < (L1 S (PMF.uniformOfFintype (W × Lat)) u h).snd l₂ ↔ ∑ w : W, (S (w, l₁)) u < ∑ w : W, (S (w, l₂)) u

Latent companion of L1_uniform_world_prefers_iff.

Pair-choice pragmatic listener

When the speaker chooses an (utterance, latent) pair — the latent an output of the speaker rather than part of its state ([FB20b]) — one speaker per world normalizes over pairs, and the listener recovers the joint (world, latent) from the utterance alone via PMF.emissionPosterior.

noncomputable def RSA.Canonical.L1Intent {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype Lat] [Fintype U] [DecidableEq U] (S : W → PMF (U × Lat)) (prior : PMF W) (u : U) (h : PMF.marginal (fun (w : W) => (S w).fst) prior u ≠ 0) : PMF (W × Lat)

The pair-choice pragmatic listener: the posterior over world × latent given the observed utterance component of a jointly chosen (utterance, latent) action.

Equations

• RSA.Canonical.L1Intent S prior u h = PMF.emissionPosterior S prior u h

theorem RSA.Canonical.L1Intent_uniform_world_prefers_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [Fintype U] [DecidableEq U] [DecidableEq W] [Nonempty W] (S : W → PMF (U × Lat)) (u : U) (h : PMF.marginal (fun (w : W) => (S w).fst) (PMF.uniformOfFintype W) u ≠ 0) (w₁ w₂ : W) : (L1Intent S (PMF.uniformOfFintype W) u h).fst w₁ < (L1Intent S (PMF.uniformOfFintype W) u h).fst w₂ ↔ ∑ l : Lat, (S w₁) (u, l) < ∑ l : Lat, (S w₂) (u, l)

At a uniform world prior, L1Intent world preference reduces to pooled speaker sums over the latent.

theorem RSA.Canonical.L1Intent_uniform_latent_prefers_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [Fintype U] [DecidableEq U] [DecidableEq Lat] [Nonempty W] (S : W → PMF (U × Lat)) (u : U) (h : PMF.marginal (fun (w : W) => (S w).fst) (PMF.uniformOfFintype W) u ≠ 0) (l₁ l₂ : Lat) : (L1Intent S (PMF.uniformOfFintype W) u h).snd l₁ < (L1Intent S (PMF.uniformOfFintype W) u h).snd l₂ ↔ ∑ w : W, (S w) (u, l₁) < ∑ w : W, (S w) (u, l₂)

At a uniform world prior, L1Intent latent preference reduces to pooled speaker sums over worlds.

theorem RSA.Canonical.L1Intent_uniform_marginal_ne_zero {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [Fintype U] [DecidableEq U] [Nonempty W] (S : W → PMF (U × Lat)) {w : W} {u : U} {l : Lat} (h : (S w) (u, l) ≠ 0) : PMF.marginal (fun (w : W) => (S w).fst) (PMF.uniformOfFintype W) u ≠ 0

A single world w where the pair (u, l) has positive speaker mass makes the utterance marginal non-zero — the positivity discharge for L1Intent at a uniform prior.

Power-utility informativity speakers

The cost-free informativity speaker at a natural exponent α — S1(u|s) ∝ L0(s|u)^α, the [FG12] form taken by most RSA papers. The speaker state is a world × latent pair s : W × I and the literal listener a per-latent kernel L0 : I → U → PMF W. powUtility is rsaUtility at zero cost (powUtility_eq_rsaUtility); through the bridge PMF.softmaxWeight_natMul_log_eq_pow the softmax weights are the powers powWeight = L0^α, so predictions reduce to weight dominance via the PMF.normalize bound lemmas, with ℕ-certificates (ENNReal.natCast_mul_inv_pow_lt) closing uniform-extension comparisons.

noncomputable def RSA.Canonical.powUtility {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) (s : W × I) (u : U) : EReal

The power-utility informativity speaker score α · log L0(w | u, i).

Equations

• RSA.Canonical.powUtility α L0 s u = ↑α * ((L0 s.2 u) s.1).log

theorem RSA.Canonical.powUtility_eq_rsaUtility {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) (s : W × I) (u : U) : powUtility α L0 s u = rsaUtility (fun (s : W × I) (u : U) => (L0 s.2 u) s.1) (fun (x : U) => 0) (↑α) s u

Grounding: powUtility is rsaUtility at exponent α and zero cost.

theorem RSA.Canonical.viableSpeaker_powUtility_of_witness {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) (hw : ∀ (s : W × I), ∃ (u : U), (L0 s.2 u) s.1 ≠ 0) : ViableSpeaker (powUtility α L0)

powUtility is viable as soon as every state has an applicable utterance — the discharge for the ViableSpeaker instance of any informativity speaker.

noncomputable def RSA.Canonical.powWeight {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) (s : W × I) (u : U) : ENNReal

Softmax weight of the power-utility speaker: the power L0^α.

Equations

• RSA.Canonical.powWeight α L0 s u = (L0 s.2 u) s.1 ^ α

theorem RSA.Canonical.tsum_powWeight_ne_zero {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [ViableSpeaker (powUtility α L0)] (s : W × I) : ∑' (u : U), powWeight α L0 s u ≠ 0

theorem RSA.Canonical.tsum_powWeight_ne_top {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [Fintype U] (s : W × I) : ∑' (u : U), powWeight α L0 s u ≠ ⊤

theorem RSA.Canonical.S1_powUtility_eq_normalize {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [Fintype U] [ViableSpeaker (powUtility α L0)] (s : W × I) : S1 (powUtility α L0) s = PMF.normalize (powWeight α L0 s) ⋯ ⋯

The power-utility speaker in PMF.normalize-of-powers form (the bridge PMF.softmaxWeight_natMul_log_eq_pow).

theorem RSA.Canonical.S1_powUtility_lt_inv_succ {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [Fintype U] [ViableSpeaker (powUtility α L0)] {s : W × I} {a : U} {S : Finset U} {n : ℕ} (ha : a ∉ S) (h : ↑n * powWeight α L0 s a < ∑ b ∈ S, powWeight α L0 s b) : (S1 (powUtility α L0) s) a < (↑n + 1)⁻¹

Dominance upper bound: the competitors in S outweigh a by a factor of n, so a's share is below (n+1)⁻¹.

theorem RSA.Canonical.inv_succ_lt_S1_powUtility {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [Fintype U] [ViableSpeaker (powUtility α L0)] [DecidableEq U] {s : W × I} {a : U} {n : ℕ} (h : ∑ b ∈ Finset.univ.erase a, powWeight α L0 s b < ↑n * powWeight α L0 s a) : (↑n + 1)⁻¹ < (S1 (powUtility α L0) s) a

Majority lower bound: all competitors together weigh less than n times a, so a's share exceeds (n+1)⁻¹.

theorem RSA.Canonical.S1_powUtility_eq_one {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [Fintype U] [ViableSpeaker (powUtility α L0)] {s : W × I} (hα : α ≠ 0) (a : U) (h : ∀ (b : U), b ≠ a → (L0 s.2 b) s.1 = 0) : (S1 (powUtility α L0) s) a = 1

The only applicable utterance is produced with certainty.

theorem RSA.Canonical.S1_powUtility_eq_zero {W : Type u_1} {I : Type u_2} {U : Type u_3} (α : ℕ) (L0 : I → U → PMF W) [Fintype U] [ViableSpeaker (powUtility α L0)] {s : W × I} {a : U} (hα : α ≠ 0) (h : (L0 s.2 a) s.1 = 0) : (S1 (powUtility α L0) s) a = 0

An inapplicable utterance is never produced.

Event comparison for the pragmatic listener

theorem RSA.Canonical.L1_event_lt_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype (W × Lat)] (S : W × Lat → PMF U) (joint : PMF (W × Lat)) (u : U) (h : PMF.marginal S joint u ≠ 0) (A B : Finset (W × Lat)) : (L1 S joint u h).toOuterMeasure ↑A < (L1 S joint u h).toOuterMeasure ↑B ↔ ∑ p ∈ A, joint p * (S p) u < ∑ p ∈ B, joint p * (S p) u

Posterior-mass comparison over events of the joint listener reduces to comparing prior-weighted speaker sums — PMF.posterior_toOuterMeasure_lt_iff_finset_score_lt in the L1 vocabulary.

theorem RSA.Canonical.L1_uniform_event_lt_iff {W : Type u_1} {Lat : Type u_2} {U : Type u_3} [Fintype W] [Fintype Lat] [Nonempty (W × Lat)] (S : W × Lat → PMF U) (u : U) (h : PMF.marginal S (PMF.uniformOfFintype (W × Lat)) u ≠ 0) (A B : Finset (W × Lat)) : (L1 S (PMF.uniformOfFintype (W × Lat)) u h).toOuterMeasure ↑A < (L1 S (PMF.uniformOfFintype (W × Lat)) u h).toOuterMeasure ↑B ↔ ∑ p ∈ A, (S p) u < ∑ p ∈ B, (S p) u

At a uniform joint prior the prior cancels: event comparison reduces to comparing summed speaker probabilities.

Propositional-meaning literal listeners with latent interpretations

The [BLG16] lexical-uncertainty shape: a decidable meaning per latent interpretation, the literal listener uniform on the extension.

noncomputable def RSA.Canonical.L0OfPred {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) (i : I) (u : U) : PMF W

Per-interpretation literal listener: uniform on the extension.

Equations

• RSA.Canonical.L0OfPred m hne i u = RSA.L0OfPred (m i) u ⋯

theorem RSA.Canonical.L0OfPred_ne_zero {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {i : I} {u : U} {w : W} (h : m i u w) : (L0OfPred m hne i u) w ≠ 0

theorem RSA.Canonical.L0OfPred_eq_zero {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {i : I} {u : U} {w : W} (h : ¬m i u w) : (L0OfPred m hne i u) w = 0

theorem RSA.Canonical.powWeight_L0OfPred_of_mem {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {α : ℕ} {w : W} {i : I} {u : U} (k : ℕ) (h : m i u w) (hk : (extensionOf (m i) u).card = k) : powWeight α (L0OfPred m hne) (w, i) u = (↑k)⁻¹ ^ α

Weight of the power-utility speaker over a propositional model: the inverse extension size, to the α.

theorem RSA.Canonical.powWeight_L0OfPred_of_not_mem {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {α : ℕ} (hα : α ≠ 0) {w : W} {i : I} {u : U} (h : ¬m i u w) : powWeight α (L0OfPred m hne) (w, i) u = 0

theorem RSA.Canonical.S1_L0OfPred_lt_inv_succ_of_dominator {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {α : ℕ} [Fintype U] [ViableSpeaker (powUtility α (L0OfPred m hne))] {w : W} {i : I} {u u' : U} {n k k' : ℕ} (huu' : u ≠ u') (hu : m i u w) (hu' : m i u' w) (hk : (extensionOf (m i) u).card = k) (hk' : (extensionOf (m i) u').card = k') (hα : α ≠ 0) (hcert : n * k' ^ α < k ^ α) : (S1 (powUtility α (L0OfPred m hne)) (w, i)) u < (↑n + 1)⁻¹

One-dominator bound over a propositional model: if u' is also applicable with an extension smaller by an ℕ-certificate factor, u is produced with probability below (n+1)⁻¹.

theorem RSA.Canonical.S1_L0OfPred_ne_zero {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {α : ℕ} [Fintype U] [ViableSpeaker (powUtility α (L0OfPred m hne))] {i : I} {u : U} {w : W} (h : m i u w) : (S1 (powUtility α (L0OfPred m hne)) (w, i)) u ≠ 0

The propositional-model speaker never assigns zero mass to a true utterance — the witness for pragmatic-listener positivity obligations.

Exact rational evaluation over a propositional model

ratS1 computes the propositional-model speaker as an exact rational and S1_eq_ofReal bridges it to S1; concrete masses and pooled sums then reduce to ℚ arithmetic (norm_num).

def RSA.Canonical.ratWeight {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (α : ℕ) (i : I) (w : W) (u : U) : ℚ

Exact rational unnormalised speaker weight over a propositional model.

Equations

• RSA.Canonical.ratWeight m α i w u = if m i u w then (↑(RSA.extensionOf (m i) u).card)⁻¹ ^ α else 0

def RSA.Canonical.ratPartition {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (α : ℕ) [Fintype U] (i : I) (w : W) : ℚ

Exact rational partition function over a propositional model.

Equations

• RSA.Canonical.ratPartition m α i w = ∑ u : U, RSA.Canonical.ratWeight m α i w u

def RSA.Canonical.ratS1 {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (α : ℕ) [Fintype U] (i : I) (w : W) (u : U) : ℚ

Exact rational normalised speaker mass over a propositional model.

Equations

• RSA.Canonical.ratS1 m α i w u = RSA.Canonical.ratWeight m α i w u / RSA.Canonical.ratPartition m α i w

theorem RSA.Canonical.ratWeight_nonneg {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (α : ℕ) (i : I) (w : W) (u : U) : 0 ≤ ratWeight m α i w u

theorem RSA.Canonical.powWeight_eq_ofReal {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) {α : ℕ} (hα : α ≠ 0) (i : I) (w : W) (u : U) : powWeight α (L0OfPred m hne) (w, i) u = ENNReal.ofReal ↑(ratWeight m α i w u)

theorem RSA.Canonical.tsum_powWeight_eq_ofReal {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) [Fintype U] {α : ℕ} (hα : α ≠ 0) (i : I) (w : W) : ∑' (u : U), powWeight α (L0OfPred m hne) (w, i) u = ENNReal.ofReal ↑(ratPartition m α i w)

theorem RSA.Canonical.ratPartition_pos {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) [Fintype U] {α : ℕ} [ViableSpeaker (powUtility α (L0OfPred m hne))] (hα : α ≠ 0) (i : I) (w : W) : 0 < ratPartition m α i w

theorem RSA.Canonical.ratS1_nonneg {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] [Fintype U] (α : ℕ) (i : I) (w : W) (u : U) : 0 ≤ ratS1 m α i w u

theorem RSA.Canonical.S1_eq_ofReal {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) [Fintype U] {α : ℕ} [ViableSpeaker (powUtility α (L0OfPred m hne))] (hα : α ≠ 0) (i : I) (w : W) (u : U) : (S1 (powUtility α (L0OfPred m hne)) (w, i)) u = ENNReal.ofReal ↑(ratS1 m α i w u)

Exact rational value of the power-utility speaker over a propositional model.

theorem RSA.Canonical.sum_S1_eq_ofReal {W : Type u_1} {I : Type u_2} {U : Type u_3} [Fintype W] (m : I → U → W → Prop) [(i : I) → (u : U) → DecidablePred (m i u)] (hne : ∀ (i : I) (u : U), (extensionOf (m i) u).Nonempty) [Fintype U] {α : ℕ} [ViableSpeaker (powUtility α (L0OfPred m hne))] (hα : α ≠ 0) {ι : Type u_4} (s : Finset ι) (st : ι → W × I) (uu : ι → U) : ∑ x ∈ s, (S1 (powUtility α (L0OfPred m hne)) (st x)) (uu x) = ENNReal.ofReal (∑ x ∈ s, ↑(ratS1 m α (st x).2 (st x).1 (uu x)))

Any finite family of propositional-model speaker masses sums to the ofReal of the corresponding ratS1 sum — the workhorse for pooled-latent reductions.