The uniform-prior RSA model

Finite states, Boolean meanings, a uniform prior, and no cost — the model of [FB20] eqs. 5–9 — as the pipeline of Linglib.Pragmatics.RSA.Basic at those arguments: the literal listener is uniform on each choice's extension, and the speaker's and listeners' masses reduce to the informativity profiles of Linglib.Pragmatics.RSA.Profile. Findings then close by decide: uniformly in the rationality through Multiset.StrictDominates certificates, or at a pinned natural rationality through ℕ inequalities (Multiset.divPowSum).

Main definitions

• RSA.uniformListener — literalListener at a uniform prior and indicator meanings.
• RSA.uniformSpeaker, RSA.uniformJointListener — the pipeline at those arguments.

Main results

• RSA.uniformSpeaker_real_singleton_lt_of_card_lt — informativity monotonicity.
• RSA.uniformJointListener_fst_real_lt_of_prodMul_strictDominates — the certificate register.
• RSA.uniformJointListener_fst_real_lt_of_divPowSum, RSA.uniformJointListener_snd_real_lt_of_divPowSum — the evaluation register.

noncomputable def RSA.uniformListener {T : Type u_1} {C : Type u_2} [MeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) : ProbabilityTheory.Kernel C T

The literal listener at a uniform prior (eq. 5): uniform on each choice's extension.

Equations

• RSA.uniformListener sem = RSA.literalListener (ProbabilityTheory.uniformOn Set.univ) fun (c : C) => (↑(sem c)).indicator 1

theorem RSA.uniformListener_apply {T : Type u_1} {C : Type u_2} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (c : C) : (uniformListener sem) c = ProbabilityTheory.uniformOn ↑(sem c)

theorem RSA.uniformListener_apply_singleton {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (c : C) (t : T) : ((uniformListener sem) c) {t} = if t ∈ sem c then (↑(sem c).card)⁻¹ else 0

theorem RSA.uniformListener_apply_singleton_le_one {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (c : C) (t : T) : ((uniformListener sem) c) {t} ≤ 1

theorem RSA.uniformListener_apply_singleton_ne_zero {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {c : C} {t : T} (h : t ∈ sem c) : ((uniformListener sem) c) {t} ≠ 0

theorem RSA.literalListener_uniformOn_apply_singleton {T : Type u_1} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Nonempty T] {U : Type u_4} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (m : U → T → ENNReal) (u : U) (t : T) : ((literalListener (ProbabilityTheory.uniformOn Set.univ) m) u) {t} = m u t / ∑ t' : T, m u t'

At a uniform prior a graded meaning normalizes to its share of the row sum: the prior cancels.

theorem RSA.literalListener_uniformOn_ofReal_apply_singleton {T : Type u_1} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Nonempty T] {U : Type u_4} [MeasurableSpace U] [Countable U] [MeasurableSingletonClass U] (m : U → T → ℝ) (u : U) (t : T) (hm : ∀ (t' : T), 0 ≤ m u t') (hpos : 0 < ∑ t' : T, m u t') : ((literalListener (ProbabilityTheory.uniformOn Set.univ) fun (u : U) (t : T) => ENNReal.ofReal (m u t)) u) {t} = ENNReal.ofReal (m u t / ∑ t' : T, m u t')

With real-valued meanings the share is the real ratio of the row.

@[reducible, inline]

noncomputable abbrev RSA.uniformSpeaker {T : Type u_1} {C : Type u_2} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (α : ℝ) : ProbabilityTheory.Kernel T C

The speaker at a uniform prior (eq. 7): best response to uniformListener at no cost.

Equations

• RSA.uniformSpeaker sem α = RSA.speaker α 1 (RSA.uniformListener sem)

theorem RSA.uniformSpeaker_apply_singleton {T : Type u_1} {C : Type u_2} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (α : ℝ) (t : T) (c : C) : ((uniformSpeaker sem α) t) {c} = ((uniformListener sem) c) {t} ^ α / ∑ c' : C, ((uniformListener sem) c') {t} ^ α

theorem RSA.uniformSpeaker_apply_univ_le_one {T : Type u_1} {C : Type u_2} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (α : ℝ) (t : T) : ((uniformSpeaker sem α) t) Set.univ ≤ 1

theorem RSA.isMarkovKernel_uniformSpeaker {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 ≤ α) (hsem : ∀ (t : T), ∃ (c : C), t ∈ sem c) : ProbabilityTheory.IsMarkovKernel (uniformSpeaker sem α)

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

theorem RSA.uniformSpeaker_apply_singleton_eq_zero {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {t : T} {c : C} (h : t ∉ sem c) : ((uniformSpeaker sem α) t) {c} = 0

theorem RSA.uniformSpeaker_apply_singleton_ne_zero {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 ≤ α) {t : T} {c : C} (h : t ∈ sem c) : ((uniformSpeaker sem α) t) {c} ≠ 0

theorem RSA.uniformSpeaker_apply_singleton_eq_one {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {t : T} {c : C} (hmem : t ∈ sem c) (hother : ∀ (c' : C), c' ≠ c → t ∉ sem c') : ((uniformSpeaker sem α) t) {c} = 1

A state truly described by a single choice produces it with certainty.

theorem RSA.speaker_uniformListener_apply_singleton_ne_zero_iff {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {cost : C → ENNReal} (hc0 : ∀ (c : C), cost c ≠ 0) (hctop : ∀ (c : C), cost c ≠ ⊤) (t : T) (c : C) : ((speaker α cost (uniformListener sem)) t) {c} ≠ 0 ↔ t ∈ sem c

With positive finite cost factors, a speaker over the uniform literal listener produces a choice at a state exactly when the choice is true there.

theorem RSA.sum_rpow_uniformListener {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) (t : T) : ∑ c : C, ((uniformListener sem) c) {t} ^ α = Multiset.invPowSum α (profile sem t)

theorem RSA.sum_rpow_uniformListener_toReal {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) (t : T) : ∑ c : C, (((uniformListener sem) c) {t} ^ α).toReal = (Multiset.invPowSum α (profile sem t)).toReal

theorem RSA.uniformSpeaker_apply_singleton_of_profile_eq {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {t t' : T} (hprof : profile sem t = profile sem t') {c : C} (hmem : t ∈ sem c) (hmem' : t' ∈ sem c) : ((uniformSpeaker sem α) t) {c} = ((uniformSpeaker sem α) t') {c}

The speaker share of a true choice depends on the state only through its profile.

theorem RSA.sum_fiber_rpow_uniformListener {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq O] (obs : C → O) {α : ℝ} (hα : 0 < α) (o : O) (t : T) : ∑ c : C with obs c = o, ((uniformListener sem) c) {t} ^ α = Multiset.invPowSum α (fiberProfile sem obs o t)

theorem RSA.sum_fiber_uniformSpeaker {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq O] (obs : C → O) {α : ℝ} (hα : 0 < α) (o : O) (t : T) : ∑ c : C with obs c = o, ((uniformSpeaker sem α) t) {c} = Multiset.invPowSum α (fiberProfile sem obs o t) / Multiset.invPowSum α (profile sem t)

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

theorem RSA.uniformSpeaker_real_singleton {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) (t : T) (c : C) : ((uniformSpeaker sem α) t).real {c} = (if t ∈ sem c then (↑(sem c).card)⁻¹ ^ α else 0) / (Multiset.invPowSum α (profile sem t)).toReal

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

theorem RSA.uniformSpeaker_real_singleton_eq_zero {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {t : T} {c : C} (h : t ∉ sem c) : ((uniformSpeaker sem α) t).real {c} = 0

theorem RSA.sum_uniformSpeaker_real_singleton_le_one {T : Type u_1} {C : Type u_2} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (α : ℝ) (t : T) (S : Finset C) : ∑ c ∈ S, ((uniformSpeaker sem α) t).real {c} ≤ 1

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

theorem RSA.uniformSpeaker_real_singleton_lt_one {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq C] {α : ℝ} (hα : 0 ≤ α) {t : T} {c c' : C} (hne : c' ≠ c) (hmem' : t ∈ sem c') : ((uniformSpeaker sem α) t).real {c} < 1

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

theorem RSA.uniformSpeaker_real_singleton_lt_of_card_lt {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {t : T} {c c' : C} (hmem : t ∈ sem c) (hmem' : t ∈ sem c') (hcard : (sem c').card < (sem c).card) : ((uniformSpeaker sem α) t).real {c} < ((uniformSpeaker sem α) t).real {c'}

Informativity monotonicity ([FB20] 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.uniformSpeaker_real_singleton_of_profile_replicate {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {α : ℝ} (hα : 0 < α) {t : T} {c : C} {m n : ℕ} (hprof : profile sem t = Multiset.replicate m n) (hmem : t ∈ sem c) : ((uniformSpeaker sem α) 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.

theorem RSA.uniformSpeaker_real_singleton_divPowSum {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) {k D : ℕ} [NeZero k] [NeZero D] {t : T} (hdvd : ∀ n ∈ profile sem t, n ∣ D) (c : C) : ((uniformSpeaker sem ↑k) t).real {c} = (if t ∈ sem c then ↑((D / (sem c).card) ^ k) else 0) / ↑(Multiset.divPowSum D k (profile sem t))

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

The listener

@[reducible, inline]

noncomputable abbrev RSA.uniformJointListener {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (obs : C → O) [MeasurableSpace O] [Nonempty T] [Nonempty C] (α : ℝ) : ProbabilityTheory.Kernel O (T × C)

The joint listener at a uniform prior (eqs. 18b/21b): the pragmatic listener of uniformSpeaker, hearing the form of the speaker's choice.

Equations

• RSA.uniformJointListener sem obs α = RSA.jointListener α 1 (RSA.uniformListener sem) (ProbabilityTheory.uniformOn Set.univ) obs

theorem RSA.map_comp_uniformSpeaker_ne_zero {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) (obs : C → O) [MeasurableSpace O] [MeasurableSingletonClass O] {α : ℝ} (hα : 0 ≤ α) {t : T} {c : C} {o : O} (hc : obs c = o) (hmem : t ∈ sem c) : (MeasureTheory.Measure.map obs ((ProbabilityTheory.uniformOn Set.univ).bind ⇑(uniformSpeaker sem α))) {o} ≠ 0

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

theorem RSA.uniformJointListener_snd_real_lt_of_divPowSum {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq O] (obs : C → O) [MeasurableSpace O] [MeasurableSingletonClass O] [Nonempty T] [Nonempty C] (hsem : ∀ (t : T), ∃ (c : C), t ∈ sem c) {k D : ℕ} [NeZero k] [NeZero D] (hdvd : ∀ (t : T), ∀ n ∈ profile sem t, n ∣ D) {o : O} {c₁ c₂ : C} (h₁ : obs c₁ = o) (h₂ : obs c₂ = o) (hlt : pooledDivPowSum sem D k c₁ < pooledDivPowSum sem D k c₂) : ((uniformJointListener sem obs ↑k) o).snd.real {c₁} < ((uniformJointListener sem obs ↑k) o).snd.real {c₂}

The evaluation register for the choice posterior at a natural rationality: 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.uniformJointListener_fst_real_lt_iff_invPowSum {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq O] (obs : C → O) [MeasurableSpace O] [MeasurableSingletonClass O] [Nonempty T] [Nonempty C] (hsem : ∀ (t : T), ∃ (c : C), t ∈ sem c) {α : ℝ} (hα : 0 < α) {o : O} {t₁ t₂ : T} (h₂ : ∃ (c : C), obs c = o ∧ t₂ ∈ sem c) : ((uniformJointListener sem obs α) o).fst.real {t₁} < ((uniformJointListener sem obs α) o).fst.real {t₂} ↔ (Multiset.invPowSum α (fiberProfile sem obs o t₁)).toReal * (Multiset.invPowSum α (profile sem t₂)).toReal < (Multiset.invPowSum α (fiberProfile sem obs o t₂)).toReal * (Multiset.invPowSum α (profile sem t₁)).toReal

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

theorem RSA.uniformJointListener_fst_real_lt_of_prodMul_strictDominates {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq O] (obs : C → O) [MeasurableSpace O] [MeasurableSingletonClass O] [Nonempty T] [Nonempty C] (hsem : ∀ (t : T), ∃ (c : C), t ∈ sem c) {α : ℝ} (hα : 0 < α) {o : O} {t₁ t₂ : T} (hcert : ((fiberProfile sem obs o t₂).prodMul (restProfile sem obs o t₁)).StrictDominates ((fiberProfile sem obs o t₁).prodMul (restProfile sem obs o t₂))) : ((uniformJointListener sem obs α) o).fst.real {t₁} < ((uniformJointListener sem obs α) o).fst.real {t₂}

The certificate register: strict domination of the fibre-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 fibre at t₁ is the support case: any nonempty product strictly dominates 0.

theorem RSA.uniformJointListener_fst_real_lt_of_divPowSum {T : Type u_1} {C : Type u_2} {O : Type u_3} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] (sem : C → Finset T) [DecidableEq O] (obs : C → O) [MeasurableSpace O] [MeasurableSingletonClass O] [Nonempty T] [Nonempty C] (hsem : ∀ (t : T), ∃ (c : C), t ∈ sem c) {k D : ℕ} [NeZero k] [NeZero D] {o : O} {t₁ t₂ : T} (hdvd₁ : ∀ n ∈ profile sem t₁, n ∣ D) (hdvd₂ : ∀ n ∈ profile sem t₂, n ∣ D) (hlt : Multiset.divPowSum D k (fiberProfile sem obs o t₁) * Multiset.divPowSum D k (profile sem t₂) < Multiset.divPowSum D k (fiberProfile sem obs o t₂) * Multiset.divPowSum D k (profile sem t₁)) : ((uniformJointListener sem obs ↑k) o).fst.real {t₁} < ((uniformJointListener sem obs ↑k) o).fst.real {t₂}

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

Latent families at the uniform prior

theorem RSA.familyListener_uniform_apply_singleton_eq_zero {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] [Nonempty T] {Λ : Type u_4} [Fintype Λ] [MeasurableSpace Λ] [DiscreteMeasurableSpace Λ] [Nonempty Λ] (sem : Λ → C → Finset T) {α : ℝ} (hα : 0 < α) {c : C} (hc : ∃ (l : Λ) (t : T), t ∈ sem l c) {p : T × Λ} (hp : p.1 ∉ sem p.2 c) : ((familyListener (fun (l : Λ) => uniformListener (sem l)) α 1 (ProbabilityTheory.uniformOn Set.univ)) c) {p} = 0

A pair whose state the utterance does not describe under its latent receives no posterior mass, as soon as some state is described under some latent.

theorem RSA.familyListener_uniform_fst_apply_singleton_ne_zero_iff {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] [Nonempty T] {Λ : Type u_4} [Fintype Λ] [MeasurableSpace Λ] [DiscreteMeasurableSpace Λ] [Nonempty Λ] (sem : Λ → C → Finset T) {α : ℝ} (hα : 0 < α) {cost : C → ENNReal} (hc0 : ∀ (c : C), cost c ≠ 0) (hctop : ∀ (c : C), cost c ≠ ⊤) {c : C} (hc : ∃ (l : Λ) (t : T), t ∈ sem l c) (t : T) : ((familyListener (fun (l : Λ) => uniformListener (sem l)) α cost (ProbabilityTheory.uniformOn Set.univ)) c).fst {t} ≠ 0 ↔ ∃ (l : Λ), t ∈ sem l c

With positive finite cost factors, the state marginal of the family listener at the uniform prior is positive at a state exactly when some latent makes the choice true there.

theorem RSA.familyListener_uniform_real_lt_of_divPowSum {T : Type u_1} {C : Type u_2} [Fintype T] [DecidableEq T] [MeasurableSpace T] [DiscreteMeasurableSpace T] [Fintype C] [MeasurableSpace C] [DiscreteMeasurableSpace C] [Nonempty T] {Λ : Type u_4} [Fintype Λ] [DecidableEq Λ] [MeasurableSpace Λ] [DiscreteMeasurableSpace Λ] [Nonempty Λ] (sem : Λ → C → Finset T) (hsem : ∀ (l : Λ) (t : T), ∃ (c : C), t ∈ sem l c) {k D : ℕ} [NeZero k] [NeZero D] (hdvd : ∀ (l : Λ) (t : T), ∀ n ∈ profile (sem l) t, n ∣ D) {c : C} {E₁ E₂ : Finset (T × Λ)} (hlt : familyDivPowSum sem D k c E₁ < familyDivPowSum sem D k c E₂) : ((familyListener (fun (l : Λ) => uniformListener (sem l)) (↑k) 1 (ProbabilityTheory.uniformOn Set.univ)) c).real ↑E₁ < ((familyListener (fun (l : Λ) => uniformListener (sem l)) (↑k) 1 (ProbabilityTheory.uniformOn Set.univ)) c).real ↑E₂

The evaluation register for a latent family at a natural rationality and the uniform prior on (state, latent) pairs: posterior preference between two events of pairs is the ℕ-valued common-denominator comparison — a kernel decide. The strict inequality carries its own truth witness.