The Rational Speech Act pipeline on probability kernels

The RSA model ([FG12]; [Deg23] eqs. 1–4; [FB20b] eqs. 5–22) in mathlib's probability vocabulary. A RSA.Scenario bundles a choice space with an extension and an observable form per choice; the literal listener is uniform on the extension, the speaker is the best response in power-weight form (ENNReal.rpow is total, so falsity needs no signed utilities), and the listeners are conditionals of the joint — rationality and priors are arguments, so findings quantify over them. Preference facts come in two registers, each closed by decide: Multiset.StrictDominates certificates on informativity profiles (strict stochastic dominance — uniform in the rationality, with empty fibers as the support case), and pinned natural rationality, where comparisons clear to ℕ inequalities via Multiset.divPowSum.

Main definitions

• RSA.literalListener — eq. 1: a prior conditioned on the extension.
• RSA.speakerOf — eqs. 2/6–7: the best-response speaker to a listener kernel, as ProbabilityTheory.Kernel.ofWeights of L ^ α.
• RSA.Scenario — the bundled model: sem, obs, and the derived L0, speaker, production, jointListener, listener, choicePosterior.
• RSA.Scenario.pool — choice-side latents: the speaker chooses the family index, normalizing across the pooled pairs (eqs. 18a/21a).
• RSA.Scenario.familySpeaker, RSA.Scenario.familyListener — state-side latents: the index is a speaker argument, normalization is per-index (eqs. 11–13). pool_L0 shows the two architectures share their weights — they differ only in the position of the latent.

Main statements

• ProbabilityTheory.posterior_apply_singleton — exact Bayes for κ†μ at a positive-mass observation.
• RSA.Scenario.listener_real_lt_of_prodMul_strictDominates — the certificate register: strict domination of fiber-by-rest profile products decides listener preference uniformly in the rationality.
• RSA.Scenario.listener_real_lt_of_divPowSum, RSA.Scenario.choicePosterior_real_lt_of_divPowSum — the evaluation register: at a natural rationality, preference is a decided ℕ inequality.

Implementation notes

All spaces here are finite and discrete; the ⊤ σ-algebra makes every study enum standard Borel, so mathlib's disintegration-based conditionals apply. Their characterization is almost-everywhere, but an ae-fact holds at every atom of positive mass (MeasureTheory.ae_of_singleton_ne_zero), which yields exact Bayes pointwise — no rnDeriv.

Almost-everywhere facts at atoms

theorem MeasureTheory.ae_of_singleton_ne_zero {α : Type u_1} [MeasurableSpace α] {ν : Measure α} {P : α → Prop} (h : ∀ᵐ (x : α) ∂ν, P x) {x : α} (hx : ν {x} ≠ 0) : P x

An almost-everywhere property holds at any atom of positive mass.

Kernels from weight functions

noncomputable def ProbabilityTheory.Kernel.ofWeights {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (w : α → β → ENNReal) : Kernel α β

The kernel that normalizes a nonnegative weight function on a finite target: row a is the probability measure proportional to w a. A row of zero (or infinite) total weight collapses to the zero measure.

Equations

• ProbabilityTheory.Kernel.ofWeights w = ProbabilityTheory.Kernel.ofFunOfCountable fun (a : α) => (∑ b : β, w a b)⁻¹ • ∑ b : β, w a b • MeasureTheory.Measure.dirac b

@[simp]

theorem ProbabilityTheory.Kernel.ofWeights_apply_singleton {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] (w : α → β → ENNReal) (a : α) (b : β) : ((ofWeights w) a) {b} = w a b / ∑ b' : β, w a b'

theorem ProbabilityTheory.Kernel.isMarkovKernel_ofWeights {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] {w : α → β → ENNReal} (h0 : ∀ (a : α), ∃ (b : β), w a b ≠ 0) (htop : ∀ (a : α) (b : β), w a b ≠ ⊤) : IsMarkovKernel (ofWeights w)

A row with a positive entry and finite entries normalizes to a probability measure.

theorem ProbabilityTheory.Kernel.ofWeights_real_singleton_lt_iff {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] [MeasurableSingletonClass β] {w : α → β → ENNReal} (a : α) (h0 : ∑ b : β, w a b ≠ 0) (htop : ∑ b : β, w a b ≠ ⊤) {b₁ b₂ : β} : ((ofWeights w) a).real {b₁} < ((ofWeights w) a).real {b₂} ↔ w a b₁ < w a b₂

Row-preference in a weight kernel reduces to weight comparison; the normalization cancels.

theorem ProbabilityTheory.Kernel.ofWeights_apply_univ_le_one {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (w : α → β → ENNReal) (a : α) : ((ofWeights w) a) Set.univ ≤ 1

Weight-kernel rows are subprobabilities: normalization gives mass 1 on positive finite total weight and 0 otherwise.

instance ProbabilityTheory.Kernel.instIsFiniteKernelOfWeights {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] [Countable α] [MeasurableSingletonClass α] [Fintype β] (w : α → β → ENNReal) : IsFiniteKernel (ofWeights w)

Exact Bayes for the posterior kernel at atoms

theorem ProbabilityTheory.posterior_apply_singleton {Ω : Type u_1} {𝓧 : Type u_2} [MeasurableSpace Ω] [MeasurableSpace 𝓧] [MeasurableSingletonClass Ω] [MeasurableSingletonClass 𝓧] [StandardBorelSpace Ω] [Nonempty Ω] (κ : Kernel Ω 𝓧) (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (ω : Ω) : ((posterior κ μ) x) {ω} = μ {ω} * (κ ω) {x} / (μ.bind ⇑κ) {x}

Exact Bayes for the posterior kernel at a positive-mass observation: evaluate the defining compProd identity on a singleton rectangle.

theorem ProbabilityTheory.comp_apply_singleton_ne_zero {Ω' : Type u_3} {𝓧' : Type u_4} [MeasurableSpace Ω'] [MeasurableSpace 𝓧'] [MeasurableSingletonClass 𝓧'] (κ : Kernel Ω' 𝓧') (μ : MeasureTheory.Measure Ω') {w : Ω'} {x : 𝓧'} (hμ : μ {w} ≠ 0) (hκ : (κ w) {x} ≠ 0) : (μ.bind ⇑κ) {x} ≠ 0

A single state of positive prior mass and positive emission witnesses a positive observation marginal.

Marginal evaluation on finite products

theorem MeasureTheory.Measure.fst_apply_singleton {Ω : Type u_1} {Θ : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Θ] [MeasurableSingletonClass Ω] [MeasurableSingletonClass Θ] [Fintype Θ] (m : Measure (Ω × Θ)) (ω : Ω) : m.fst {ω} = ∑ θ : Θ, m {(ω, θ)}

theorem MeasureTheory.Measure.snd_apply_singleton {Ω : Type u_1} {Θ : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Θ] [MeasurableSingletonClass Ω] [MeasurableSingletonClass Θ] [Fintype Ω] (m : Measure (Ω × Θ)) (θ : Θ) : m.snd {θ} = ∑ ω : Ω, m {(ω, θ)}

Uniform priors on reals

theorem MeasureTheory.uniformOn_univ_real_singleton {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype W] (w : W) : (ProbabilityTheory.uniformOn Set.univ).real {w} = (↑(Fintype.card W))⁻¹

theorem MeasureTheory.uniformOn_univ_real_coe_finset {W : Type u_1} [MeasurableSpace W] [MeasurableSingletonClass W] [Fintype W] (s : Finset W) : (ProbabilityTheory.uniformOn Set.univ).real ↑s = ↑s.card / ↑(Fintype.card W)

Marginal listener preference over product parameter spaces

theorem ProbabilityTheory.posterior_fst_real_lt_iff {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {A : Type u_2} {B : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [Fintype B] [StandardBorelSpace A] [Nonempty A] [StandardBorelSpace B] [Nonempty B] (κ : Kernel (A × B) 𝓧) (μ : MeasureTheory.Measure (A × B)) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (a₁ a₂ : A) : ((posterior κ μ) x).fst.real {a₁} < ((posterior κ μ) x).fst.real {a₂} ↔ ∑ b : B, μ.real {(a₁, b)} * (κ (a₁, b)).real {x} < ∑ b : B, μ.real {(a₂, b)} * (κ (a₂, b)).real {x}

Marginal listener preference over a product parameter space, on reals: for latent-in-the-state models, the observation's marginal cancels and the latent pools.

theorem ProbabilityTheory.posterior_snd_real_lt_iff {𝓧 : Type u_1} [MeasurableSpace 𝓧] [MeasurableSingletonClass 𝓧] {A : Type u_2} {B : Type u_3} [MeasurableSpace A] [MeasurableSpace B] [MeasurableSingletonClass A] [MeasurableSingletonClass B] [Fintype A] [StandardBorelSpace A] [Nonempty A] [StandardBorelSpace B] [Nonempty B] (κ : Kernel (A × B) 𝓧) (μ : MeasureTheory.Measure (A × B)) [MeasureTheory.IsFiniteMeasure μ] [IsFiniteKernel κ] {x : 𝓧} (hx : (μ.bind ⇑κ) {x} ≠ 0) (b₁ b₂ : B) : ((posterior κ μ) x).snd.real {b₁} < ((posterior κ μ) x).snd.real {b₂} ↔ ∑ a : A, μ.real {(a, b₁)} * (κ (a, b₁)).real {x} < ∑ a : A, μ.real {(a, b₂)} * (κ (a, b₂)).real {x}

Marginal listener preference over the latent component of a product parameter space, on reals: the states pool.

The RSA pipeline

noncomputable def RSA.literalListener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (sem : U → Set W) : ProbabilityTheory.Kernel U W

The literal listener (eq. 1): the prior belief conditioned on the utterance's extension.

Equations

• RSA.literalListener μ sem = ProbabilityTheory.Kernel.ofFunOfCountable fun (u : U) => μ[|sem u]

theorem RSA.literalListener_apply {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (sem : U → Set W) (u : U) (t : Set W) : ((literalListener μ sem) u) t = (μ (sem u))⁻¹ * μ (sem u ∩ t)

theorem RSA.literalListener_apply_singleton_of_mem {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (sem : U → Set W) {u : U} {w : W} (h : w ∈ sem u) : ((literalListener μ sem) u) {w} = (μ (sem u))⁻¹ * μ {w}

On a positive-mass extension, the literal listener is the renormalized prior at members …

theorem RSA.literalListener_apply_singleton_of_not_mem {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) (sem : U → Set W) {u : U} {w : W} (h : w ∉ sem u) : ((literalListener μ sem) u) {w} = 0

… and zero at non-members: literal falsity is never entertained.

theorem RSA.isMarkovKernel_literalListener {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype U] [MeasurableSingletonClass U] (μ : MeasureTheory.Measure W) [MeasureTheory.IsFiniteMeasure μ] (sem : U → Set W) (h : ∀ (u : U), μ (sem u) ≠ 0) : ProbabilityTheory.IsMarkovKernel (literalListener μ sem)

The literal listener is Markov as soon as every extension has positive prior mass.

The best-response speaker in power-weight form

[FB20b] eq. 6 ≡ eq. 7: softmax of α · log L is, in weight form, L ^ α. On ℝ≥0∞ the power is total — an inapplicable utterance has weight 0 ^ α = 0 — so falsity needs no EReal utilities and no ⊥/⊤ side conditions.

noncomputable def RSA.speakerOf {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] (α : ℝ) (L : ProbabilityTheory.Kernel U W) : ProbabilityTheory.Kernel W U

The best-response speaker to a listener kernel: power weights L u {w} ^ α ([FB20b] eq. 7, [Deg23] eq. 2 at the informativity utility).

Equations

• RSA.speakerOf α L = ProbabilityTheory.Kernel.ofWeights fun (w : W) (u : U) => (L u) {w} ^ α

@[simp]

theorem RSA.speakerOf_apply_singleton {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] (α : ℝ) (L : ProbabilityTheory.Kernel U W) (w : W) (u : U) : ((speakerOf α L) w) {u} = (L u) {w} ^ α / ∑ u' : U, (L u') {w} ^ α

instance RSA.instIsFiniteKernelSpeakerOf {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] (α : ℝ) (L : ProbabilityTheory.Kernel U W) : ProbabilityTheory.IsFiniteKernel (speakerOf α L)

theorem RSA.isMarkovKernel_speakerOf {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] {α : ℝ} (hα : 0 ≤ α) (L : ProbabilityTheory.Kernel U W) (hle : ∀ (u : U) (w : W), (L u) {w} ≤ 1) (h0 : ∀ (w : W), ∃ (u : U), (L u) {w} ≠ 0) : ProbabilityTheory.IsMarkovKernel (speakerOf α L)

The speaker is a probability kernel whenever every state has a true utterance ([FB20b] eq. 7's proviso).

theorem RSA.speakerOf_apply_singleton_eq_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] {α : ℝ} (hα : 0 < α) {L : ProbabilityTheory.Kernel U W} {w : W} {u : U} (h : (L u) {w} = 0) : ((speakerOf α L) w) {u} = 0

A literally false utterance is never produced (positive rationality).

theorem RSA.speakerOf_apply_singleton_ne_zero {W : Type u_1} {U : Type u_2} [MeasurableSpace W] [MeasurableSpace U] [Fintype W] [MeasurableSingletonClass W] [Fintype U] [MeasurableSingletonClass U] {α : ℝ} (hα : 0 ≤ α) {L : ProbabilityTheory.Kernel U W} {w : W} (hle : ∀ (u' : U), (L u') {w} ≤ 1) {u : U} (h : (L u) {w} ≠ 0) : ((speakerOf α L) w) {u} ≠ 0

A literally true utterance is produced with positive mass.

Choice scenarios

The bundled theory object: a choice space with an extension and an observable form for each choice. Rationality and prior are arguments of the derived kernels, not data — findings quantify over α. [FB20b]'s vanilla, LI, and GI models are three instantiations (identity observation with the bare parse; Prod.fst over pair choices, eqs. 18/21); LU places its latent in the state instead and is not a Scenario — its speaker normalizes per lexicon, not against the pooled choice space.

structure RSA.Scenario (T : Type u_3) (C : Type u_4) (O : Type u_5) : Type (max (max u_3 u_4) u_5)

A finite RSA choice scenario: each choice (an utterance, or an (utterance, parse) pair) carries an extension and an observable form.

• sem : C → Finset T

  The extension of each choice.

• obs : C → O

  The observable form of each choice: what the listener hears.

def RSA.Scenario.pool {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} (f : L → Scenario T C O) : Scenario T (C × L) O

Pool a family of scenarios into one whose choices carry the family index: the speaker chooses the index with the utterance, normalizing across the whole family ([FB20b] eqs. 18a/21a). familySpeaker instead keeps the index as an argument of the speaker (eq. 11) — with pool_L0, the paper's observation (p. e86) that the two architectures differ only in the position of the latent parameter.

Equations

• RSA.Scenario.pool f = { sem := fun (cl : C × L) => (f cl.2).sem cl.1, obs := fun (cl : C × L) => (f cl.2).obs cl.1 }

@[simp]

theorem RSA.Scenario.pool_sem {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} (f : L → Scenario T C O) (cl : C × L) : (pool f).sem cl = (f cl.2).sem cl.1

@[simp]

theorem RSA.Scenario.pool_obs {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} (f : L → Scenario T C O) (cl : C × L) : (pool f).obs cl = (f cl.2).obs cl.1

noncomputable def RSA.Scenario.L0 {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) : ProbabilityTheory.Kernel C T

The literal listener ([FB20b] eq. 5 at the paper's standing uniform prior): uniform over the choice's extension.

Equations

• s.L0 = ProbabilityTheory.Kernel.ofFunOfCountable fun (c : C) => ProbabilityTheory.uniformOn ↑(s.sem c)

theorem RSA.Scenario.L0_apply_singleton {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) (c : C) (t : T) : (s.L0 c) {t} = if t ∈ s.sem c then (↑(s.sem c).card)⁻¹ else 0

theorem RSA.Scenario.L0_apply_singleton_le_one {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) (c : C) (t : T) : (s.L0 c) {t} ≤ 1

theorem RSA.Scenario.L0_apply_singleton_ne_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) {c : C} {t : T} (h : t ∈ s.sem c) : (s.L0 c) {t} ≠ 0

theorem RSA.Scenario.pool_L0 {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] {L : Type u_6} [Fintype L] [MeasurableSpace L] [DiscreteMeasurableSpace L] (f : L → Scenario T C O) (c : C) (l : L) : (pool f).L0 (c, l) = (f l).L0 c

Pooling does not change the literal listener: pool and familySpeaker share their weights and differ only in the normalization domain — the type-level content of [FB20b]'s contrast between eq. 11 and eqs. 18a/21a (p. e86).

noncomputable def RSA.Scenario.speaker {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] (α : ℝ) : ProbabilityTheory.Kernel T C

The pragmatic speaker ([FB20b] eqs. 6–7, 18a, 21a): best response at rationality α.

Equations

• s.speaker α = RSA.speakerOf α s.L0

instance RSA.Scenario.instIsFiniteKernelSpeaker {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] (α : ℝ) : ProbabilityTheory.IsFiniteKernel (s.speaker α)

theorem RSA.Scenario.speaker_apply_univ_le_one {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] (α : ℝ) (t : T) : ((s.speaker α) t) Set.univ ≤ 1

class RSA.Scenario.Expressible (T : Type u_3) (C : Type u_4) (O : Type u_5) (s : Scenario T C O) : Prop

Every state has a true choice — the proviso making the speaker a probability kernel.

• exists_mem_sem (t : T) : ∃ (c : C), t ∈ s.sem c

theorem RSA.Scenario.isMarkovKernel_speaker {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 ≤ α) [Expressible T C O s] : ProbabilityTheory.IsMarkovKernel (s.speaker α)

theorem RSA.Scenario.speaker_apply_singleton_eq_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 < α) {t : T} {c : C} (h : t ∉ s.sem c) : ((s.speaker α) t) {c} = 0

theorem RSA.Scenario.speaker_apply_singleton_ne_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 ≤ α) {t : T} {c : C} (h : t ∈ s.sem c) : ((s.speaker α) t) {c} ≠ 0

Informativity profiles

The combinatorial shadow of the model: the multiset of extension sizes of a state's true choices. Softmax masses are ratios of Multiset.invPowSums over profiles, so preference certificates are Multiset.StrictDominates facts closed by decide — uniform in the rationality.

def RSA.Scenario.trueChoices {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) (t : T) : Finset C

The choices true at a state.

Equations

• s.trueChoices t = {x : C | t ∈ s.sem x}

def RSA.Scenario.profile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) (t : T) : Multiset ℕ

The informativity profile: extension sizes of the true choices.

Equations

• s.profile t = Multiset.map (fun (c : C) => (s.sem c).card) (s.trueChoices t).val

def RSA.Scenario.fiberProfile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] (o : O) (t : T) : Multiset ℕ

The profile restricted to choices heard as o.

Equations

• s.fiberProfile o t = Multiset.map (fun (c : C) => (s.sem c).card) {x ∈ s.trueChoices t | s.obs x = o}.val

def RSA.Scenario.restProfile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] (o : O) (t : T) : Multiset ℕ

The profile of true choices heard otherwise.

Equations

• s.restProfile o t = Multiset.map (fun (c : C) => (s.sem c).card) {x ∈ s.trueChoices t | s.obs x ≠ o}.val

theorem RSA.Scenario.profile_eq_fiberProfile_add_restProfile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] (o : O) (t : T) : s.profile t = s.fiberProfile o t + s.restProfile o t

theorem RSA.Scenario.zero_notMem_profile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) (t : T) : 0 ∉ s.profile t

theorem RSA.Scenario.zero_notMem_fiberProfile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] (o : O) (t : T) : 0 ∉ s.fiberProfile o t

theorem RSA.Scenario.zero_notMem_restProfile {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] (o : O) (t : T) : 0 ∉ s.restProfile o t

theorem RSA.Scenario.exists_of_fiberProfile_ne_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] {o : O} {t : T} (h : s.fiberProfile o t ≠ 0) : ∃ (c : C), s.obs c = o ∧ t ∈ s.sem c

A nonempty fiber profile exhibits an o-shaped true choice — certificates carry their own truth witnesses.

theorem RSA.Scenario.profile_ne_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [Expressible T C O s] (t : T) : s.profile t ≠ 0

theorem RSA.Scenario.sum_rpow_L0 {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) {α : ℝ} (hα : 0 < α) (t : T) : ∑ c : C, (s.L0 c) {t} ^ α = Multiset.invPowSum α (s.profile t)

theorem RSA.Scenario.sum_fiber_rpow_L0 {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [DecidableEq O] {α : ℝ} (hα : 0 < α) (o : O) (t : T) : ∑ c : C with s.obs c = o, (s.L0 c) {t} ^ α = Multiset.invPowSum α (s.fiberProfile o t)

theorem RSA.Scenario.sum_fiber_speaker {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] {α : ℝ} (hα : 0 < α) (o : O) (t : T) : ∑ c : C with s.obs c = o, ((s.speaker α) t) {c} = Multiset.invPowSum α (s.fiberProfile o t) / Multiset.invPowSum α (s.profile t)

Pooled speaker mass over an observation's fiber is a ratio of profile sums — [FB20b] eq. 8, structurally.

theorem RSA.Scenario.speaker_real_singleton {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 < α) (t : T) (c : C) : ((s.speaker α) t).real {c} = (if t ∈ s.sem c then (↑(s.sem c).card)⁻¹ ^ α else 0) / (Multiset.invPowSum α (s.profile t)).toReal

Exact speaker mass on reals: extension-size weight over the state's partition.

theorem RSA.Scenario.speaker_real_singleton_eq_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 < α) {t : T} {c : C} (h : t ∉ s.sem c) : ((s.speaker α) t).real {c} = 0

theorem RSA.Scenario.sum_speaker_real_singleton_le_one {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] (α : ℝ) (t : T) (S : Finset C) : ∑ c ∈ S, ((s.speaker α) t).real {c} ≤ 1

Speaker shares over any set of choices stay within the row's unit mass.

theorem RSA.Scenario.speaker_real_singleton_lt_one {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq C] {α : ℝ} (hα : 0 ≤ α) {t : T} {c c' : C} (hne : c' ≠ c) (hmem' : t ∈ s.sem c') : ((s.speaker α) t).real {c} < 1

Competition: any other true choice caps a share strictly below one.

theorem RSA.Scenario.speaker_real_singleton_lt_of_card_lt {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 < α) {t : T} {c c' : C} (hmem : t ∈ s.sem c) (hmem' : t ∈ s.sem c') (hcard : (s.sem c').card < (s.sem c).card) : ((s.speaker α) t).real {c} < ((s.speaker α) t).real {c'}

Informativity monotonicity ([FB20b] eq. 7's qualitative claim): between two true choices, the one with the strictly smaller extension is produced with strictly higher probability, at every positive rationality.

theorem RSA.Scenario.speaker_real_singleton_of_profile_replicate {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {α : ℝ} (hα : 0 < α) {t : T} {c : C} {m n : ℕ} (hprof : s.profile t = Multiset.replicate m n) (hmem : t ∈ s.sem c) : ((s.speaker α) t).real {c} = (↑m)⁻¹

Softmax constant-utility invariance: when every true choice at a state has the same extension size, the speaker is uniform on them — each share is m⁻¹ regardless of the rationality.

def RSA.Scenario.divPowSumColumn {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [Fintype T] (D k : ℕ) (c : C) : ℕ

The ℕ-cleared production mass of a choice, pooled over its true states: its common-denominator weight times, per true state, the product of the other states' cleared partition sums. Pooled evaluation-register hypotheses compare these.

Equations

• s.divPowSumColumn D k c = (D / (s.sem c).card) ^ k * ∑ t ∈ s.sem c, ∏ t' ∈ Finset.univ.erase t, Multiset.divPowSum D k (s.profile t')

theorem RSA.Scenario.speaker_real_singleton_divPowSum {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] {k D : ℕ} [NeZero k] [NeZero D] {t : T} (hdvd : ∀ n ∈ s.profile t, n ∣ D) (c : C) : ((s.speaker ↑k) t).real {c} = (if t ∈ s.sem c then ↑((D / (s.sem c).card) ^ k) else 0) / ↑(Multiset.divPowSum D k (s.profile t))

Exact speaker mass at a natural rationality, as a ratio of ℕ-valued common-denominator sums.

theorem RSA.Scenario.map_obs_comp_ne_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] [MeasurableSingletonClass O] {α : ℝ} {μ : MeasureTheory.Measure T} {t : T} {c : C} {o : O} (hμ : μ {t} ≠ 0) (hc : s.obs c = o) (hs : ((s.speaker α) t) {c} ≠ 0) : (MeasureTheory.Measure.map s.obs (μ.bind ⇑(s.speaker α))) {o} ≠ 0

A positive-prior state truly described by an o-shaped choice witnesses a positive observation marginal.

noncomputable def RSA.Scenario.production {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] (α : ℝ) : ProbabilityTheory.Kernel T O

Utterance production ([FB20b] eq. 19a): the observable form of the speaker's choice.

Equations

• s.production α = (s.speaker α).map s.obs

noncomputable def RSA.Scenario.jointObs {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] (α : ℝ) (μ : MeasureTheory.Measure T) : MeasureTheory.Measure (O × T × C)

The joint distribution of the heard form with the (state, choice) pair.

Equations

• s.jointObs α μ = MeasureTheory.Measure.map (fun (p : T × C) => (s.obs p.2, p)) (μ.compProd (s.speaker α))

instance RSA.Scenario.instIsFiniteMeasureProdJointObs {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] (α : ℝ) (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] : MeasureTheory.IsFiniteMeasure (s.jointObs α μ)

theorem RSA.Scenario.jointObs_fst {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] (α : ℝ) (μ : MeasureTheory.Measure T) : (s.jointObs α μ).fst = MeasureTheory.Measure.map s.obs (μ.bind ⇑(s.speaker α))

The heard form is distributed as the production marginal.

noncomputable def RSA.Scenario.jointListener {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] (α : ℝ) (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.Kernel O (T × C)

The joint pragmatic listener ([FB20b] eqs. 18b/21b): posterior over (state, choice) given the heard form.

Equations

• s.jointListener α μ = (s.jointObs α μ).condKernel

noncomputable def RSA.Scenario.listener {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] (α : ℝ) (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.Kernel O T

The state posterior ([FB20b] eqs. 9/19b): the world marginal of the joint listener.

Equations

• s.listener α μ = (s.jointListener α μ).fst

noncomputable def RSA.Scenario.choicePosterior {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [MeasurableSpace O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] (α : ℝ) (μ : MeasureTheory.Measure T) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.Kernel O C

The choice posterior ([FB20b] eq. 22, at pairs).

Equations

• s.choicePosterior α μ = (s.jointListener α μ).snd

theorem RSA.Scenario.jointListener_apply_singleton {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {α : ℝ} {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {o : O} (ho : (MeasureTheory.Measure.map s.obs (μ.bind ⇑(s.speaker α))) {o} ≠ 0) (t : T) (c : C) : ((s.jointListener α μ) o) {(t, c)} = (if s.obs c = o then μ {t} * ((s.speaker α) t) {c} else 0) / (MeasureTheory.Measure.map s.obs (μ.bind ⇑(s.speaker α))) {o}

Exact Bayes for the joint listener at a positive-mass observation.

theorem RSA.Scenario.listener_real_lt_iff {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {α : ℝ} {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {o : O} (ho : (MeasureTheory.Measure.map s.obs (μ.bind ⇑(s.speaker α))) {o} ≠ 0) (t₁ t₂ : T) : ((s.listener α μ) o).real {t₁} < ((s.listener α μ) o).real {t₂} ↔ ∑ c : C with s.obs c = o, μ.real {t₁} * ((s.speaker α) t₁).real {c} < ∑ c : C with s.obs c = o, μ.real {t₂} * ((s.speaker α) t₂).real {c}

Listener preference on reals: the observation's marginal cancels, leaving prior-weighted speaker mass pooled over the observation's fiber.

theorem RSA.Scenario.choicePosterior_real_lt_iff {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {α : ℝ} {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] {o : O} (ho : (MeasureTheory.Measure.map s.obs (μ.bind ⇑(s.speaker α))) {o} ≠ 0) {c₁ c₂ : C} (h₁ : s.obs c₁ = o) (h₂ : s.obs c₂ = o) : ((s.choicePosterior α μ) o).real {c₁} < ((s.choicePosterior α μ) o).real {c₂} ↔ ∑ t : T, μ.real {t} * ((s.speaker α) t).real {c₁} < ∑ t : T, μ.real {t} * ((s.speaker α) t).real {c₂}

Choice preference among o-shaped choices reduces to comparing prior-weighted speaker masses across states.

theorem RSA.Scenario.choicePosterior_real_lt_of_divPowSum {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] [Expressible T C O s] {k D : ℕ} [NeZero k] [NeZero D] (hdvd : ∀ (t : T), ∀ n ∈ s.profile t, n ∣ D) (hμeq : ∀ (t t' : T), μ {t} = μ {t'}) (hμ0 : ∀ (t : T), μ {t} ≠ 0) {o : O} {c₁ c₂ : C} (h₁ : s.obs c₁ = o) (h₂ : s.obs c₂ = o) (hlt : s.divPowSumColumn D k c₁ < s.divPowSumColumn D k c₂) : ((s.choicePosterior (↑k) μ) o).real {c₁} < ((s.choicePosterior (↑k) μ) o).real {c₂}

The evaluation register for the choice posterior at a natural rationality and equal priors: pooled preference between two o-shaped choices is the ℕ-valued common-denominator comparison over all states — a kernel decide. The strict inequality carries its own truth witness.

theorem RSA.Scenario.listener_real_lt_iff_invPowSum {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] [Expressible T C O s] {α : ℝ} (hα : 0 < α) {o : O} {t₁ t₂ : T} (hμeq : μ {t₁} = μ {t₂}) (hμ0 : μ {t₂} ≠ 0) (h₂ : ∃ (c : C), s.obs c = o ∧ t₂ ∈ s.sem c) : ((s.listener α μ) o).real {t₁} < ((s.listener α μ) o).real {t₂} ↔ (Multiset.invPowSum α (s.fiberProfile o t₁)).toReal * (Multiset.invPowSum α (s.profile t₂)).toReal < (Multiset.invPowSum α (s.fiberProfile o t₂)).toReal * (Multiset.invPowSum α (s.profile t₁)).toReal

Listener preference at equal priors reduces to the cross-multiplied profile comparison, on reals: the observation marginal and the shared prior cancel. Both registers' closers enter here.

theorem RSA.Scenario.invPowSum_odds_lt_of_prodMul_strictDominates {T : Type u_3} {C : Type u_4} {O : Type u_5} [DecidableEq T] [Fintype C] (s : Scenario T C O) [DecidableEq O] {α : ℝ} (hα : 0 < α) {o : O} {t₁ t₂ : T} (hcert : ((s.fiberProfile o t₂).prodMul (s.restProfile o t₁)).StrictDominates ((s.fiberProfile o t₁).prodMul (s.restProfile o t₂))) : (Multiset.invPowSum α (s.fiberProfile o t₁)).toReal * (Multiset.invPowSum α (s.profile t₂)).toReal < (Multiset.invPowSum α (s.fiberProfile o t₂)).toReal * (Multiset.invPowSum α (s.profile t₁)).toReal

The certificate closes the odds comparison: strict domination of the fiber-by-rest cross products decides it uniformly in the rationality (the shared fiber-by-fiber terms cancel).

theorem RSA.Scenario.listener_real_lt_of_prodMul_strictDominates {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] [Expressible T C O s] {α : ℝ} (hα : 0 < α) {o : O} {t₁ t₂ : T} (hμeq : μ {t₁} = μ {t₂}) (hμ0 : μ {t₂} ≠ 0) (hcert : ((s.fiberProfile o t₂).prodMul (s.restProfile o t₁)).StrictDominates ((s.fiberProfile o t₁).prodMul (s.restProfile o t₂))) : ((s.listener α μ) o).real {t₁} < ((s.listener α μ) o).real {t₂}

The certificate register: at equal priors, strict domination of the fiber-by-rest profile products decides listener preference uniformly in the rationality. The certificate carries its own truth witness, so a finding is a single decided Multiset.StrictDominates fact. An empty fiber at t₁ is the support case: any nonempty product strictly dominates 0.

theorem RSA.Scenario.listener_real_lt_of_divPowSum {T : Type u_3} {C : Type u_4} {O : Type u_5} [MeasurableSpace T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] (s : Scenario T C O) [Fintype T] [DecidableEq O] [MeasurableSpace O] [MeasurableSingletonClass O] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace C] [Nonempty C] {μ : MeasureTheory.Measure T} [MeasureTheory.IsFiniteMeasure μ] [Expressible T C O s] {k D : ℕ} [NeZero k] [NeZero D] {o : O} {t₁ t₂ : T} (hμeq : μ {t₁} = μ {t₂}) (hμ0 : μ {t₂} ≠ 0) (hdvd₁ : ∀ n ∈ s.profile t₁, n ∣ D) (hdvd₂ : ∀ n ∈ s.profile t₂, n ∣ D) (hlt : Multiset.divPowSum D k (s.fiberProfile o t₁) * Multiset.divPowSum D k (s.profile t₂) < Multiset.divPowSum D k (s.fiberProfile o t₂) * Multiset.divPowSum D k (s.profile t₁)) : ((s.listener (↑k) μ) o).real {t₁} < ((s.listener (↑k) μ) o).real {t₂}

The evaluation register at a natural rationality: with all profile entries dividing D, listener preference at equal priors is the ℕ-valued common-denominator comparison — a kernel decide. The strict inequality carries its own truth witness.

State-side latent families

[FB20b] eqs. 11–13 (lexical uncertainty): each speaker carries a fixed latent index and best-responds within it — normalization is per-index, in contrast to the choice-side latents of jointListener, whose speaker normalizes across the pooled pairs. The weight functions coincide; only the normalization differs.

noncomputable def RSA.Scenario.familySpeaker {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] (f : L → Scenario T C O) (α : ℝ) : ProbabilityTheory.Kernel (T × L) C

The family speaker: the latent index rides in the state.

Equations

• RSA.Scenario.familySpeaker f α = ProbabilityTheory.Kernel.ofFunOfCountable fun (tl : T × L) => ((f tl.2).speaker α) tl.1

@[simp]

theorem RSA.Scenario.familySpeaker_apply {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] (f : L → Scenario T C O) (α : ℝ) (tl : T × L) : (familySpeaker f α) tl = ((f tl.2).speaker α) tl.1

instance RSA.Scenario.instIsFiniteKernelProdFamilySpeaker {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] (f : L → Scenario T C O) (α : ℝ) : ProbabilityTheory.IsFiniteKernel (familySpeaker f α)

noncomputable def RSA.Scenario.familyListener {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace L] [Nonempty L] (f : L → Scenario T C O) (α : ℝ) (μ : MeasureTheory.Measure (T × L)) [MeasureTheory.IsFiniteMeasure μ] : ProbabilityTheory.Kernel C (T × L)

The family listener: the Bayesian inverse of the family speaker over the joint (state, index) space — [FB20b] eqs. 12–13. Bundling the posterior keeps consumers' goals first-order in familyListener.

Equations

• RSA.Scenario.familyListener f α μ = ProbabilityTheory.posterior (RSA.Scenario.familySpeaker f α) μ

theorem RSA.Scenario.comp_familySpeaker_ne_zero {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] {f : L → Scenario T C O} {α : ℝ} (hα : 0 ≤ α) {μ : MeasureTheory.Measure (T × L)} (hμ0 : ∀ (p : T × L), μ {p} ≠ 0) {t : T} {l : L} {c : C} (hmem : t ∈ (f l).sem c) : (μ.bind ⇑(familySpeaker f α)) {c} ≠ 0

A member's true choice at a positive-prior state witnesses a positive observation marginal for the family speaker.

theorem RSA.Scenario.familyListener_fst_real_lt_iff {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace L] [Nonempty L] {μ : MeasureTheory.Measure (T × L)} [MeasureTheory.IsFiniteMeasure μ] [Fintype L] (f : L → Scenario T C O) {α : ℝ} (hα : 0 ≤ α) (hμeq : ∀ (p q : T × L), μ {p} = μ {q}) (hμ0 : ∀ (p : T × L), μ {p} ≠ 0) {c : C} {t₀ : T} {l₀ : L} (hmem : t₀ ∈ (f l₀).sem c) {t₁ t₂ : T} : ((familyListener f α μ) c).fst.real {t₁} < ((familyListener f α μ) c).fst.real {t₂} ↔ ∑ l : L, (((f l).speaker α) t₁).real {c} < ∑ l : L, (((f l).speaker α) t₂).real {c}

State-marginal preference for a latent family at equal priors: the latent pools, leaving summed member speaker shares. Any member's true choice at either state supplies the positivity side condition.

theorem RSA.Scenario.familyListener_snd_real_lt_iff {T : Type u_3} {C : Type u_4} {O : Type u_5} {L : Type u_6} [MeasurableSpace T] [Fintype T] [DecidableEq T] [MeasurableSingletonClass T] [MeasurableSpace C] [Fintype C] [DiscreteMeasurableSpace C] [MeasurableSpace L] [Countable L] [MeasurableSingletonClass L] [StandardBorelSpace T] [Nonempty T] [StandardBorelSpace L] [Nonempty L] {μ : MeasureTheory.Measure (T × L)} [MeasureTheory.IsFiniteMeasure μ] (f : L → Scenario T C O) {α : ℝ} (hα : 0 ≤ α) (hμeq : ∀ (p q : T × L), μ {p} = μ {q}) (hμ0 : ∀ (p : T × L), μ {p} ≠ 0) {c : C} {t₀ : T} {l₀ : L} (hmem : t₀ ∈ (f l₀).sem c) {l₁ l₂ : L} : ((familyListener f α μ) c).snd.real {l₁} < ((familyListener f α μ) c).snd.real {l₂} ↔ ∑ t : T, (((f l₁).speaker α) t).real {c} < ∑ t : T, (((f l₂).speaker α) t).real {c}

Latent-marginal preference for a latent family at equal priors: the states pool, leaving summed member speaker shares.