[GS13] on mathlib PMF

[GS13]

PMF formalization of GS2013 using PMF.hypergeometric as the observation kernel primitive. The model is parameterized over a : Access throughout; each downstream operator (speakerBelief, qualityOk, s1Score, S1g, marginalSpeaker, L1) takes (a, k) where k : Fin (a.val + 1) is the observed count.

PMF stack (one definition each, parameterized)

• worldPrior : PMF WorldState — uniform on 4 states
• obsKernel a w : PMF (Fin (a.val + 1)) — PMF.hypergeometric 3 w.toNat a.val
• speakerBelief a k : PMF WorldState — PMF.posterior (obsKernel a) worldPrior k
• S1g m α a k h : PMF U — softmax-of-expected-log over the speaker's belief
• marginalSpeaker m α a w hCov : PMF U — (obsKernel a w).bind (S1g a)
• L1 m α a u hMarg : PMF WorldState — PMF.posterior (marginalSpeaker a) worldPrior u

Silence-extended findings

All 11 paper findings are stated against the silence-extended utterance space RSA.WithSilence U — the cover hypothesis cover_silent is universal because silence is qOk at every observation. This dissolves the (access, word) cells that GS2013's "sensible situations" restriction excludes, which would otherwise block formalization without silence.

Model substrate: world states, utterance enums, meanings, access

inductive GoodmanStuhlmuller2013.WorldState : Type

World states: how many of 3 objects have the property.

• s0 : WorldState
• s1 : WorldState
• s2 : WorldState
• s3 : WorldState

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidableEqWorldState : DecidableEq WorldState

Equations

• GoodmanStuhlmuller2013.instDecidableEqWorldState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GoodmanStuhlmuller2013.instReprWorldState : Repr WorldState

Equations

• GoodmanStuhlmuller2013.instReprWorldState = { reprPrec := GoodmanStuhlmuller2013.instReprWorldState.repr }

def GoodmanStuhlmuller2013.instReprWorldState.repr : WorldState → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GoodmanStuhlmuller2013.instInhabitedWorldState : Inhabited WorldState

Equations

• GoodmanStuhlmuller2013.instInhabitedWorldState = { default := GoodmanStuhlmuller2013.instInhabitedWorldState.default }

@[instance_reducible]

instance GoodmanStuhlmuller2013.instFintypeWorldState : Fintype WorldState

Equations

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

def GoodmanStuhlmuller2013.WorldState.toNat : WorldState → ℕ

Equations

• GoodmanStuhlmuller2013.WorldState.s0.toNat = 0
• GoodmanStuhlmuller2013.WorldState.s1.toNat = 1
• GoodmanStuhlmuller2013.WorldState.s2.toNat = 2
• GoodmanStuhlmuller2013.WorldState.s3.toNat = 3

theorem GoodmanStuhlmuller2013.WorldState.toNat_le_three (w : WorldState) : w.toNat ≤ 3

inductive GoodmanStuhlmuller2013.QUtt : Type

Quantifier alternative set.

• none_ : QUtt
• some_ : QUtt
• all : QUtt

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidableEqQUtt : DecidableEq QUtt

Equations

• GoodmanStuhlmuller2013.instDecidableEqQUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def GoodmanStuhlmuller2013.instReprQUtt.repr : QUtt → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GoodmanStuhlmuller2013.instReprQUtt : Repr QUtt

Equations

• GoodmanStuhlmuller2013.instReprQUtt = { reprPrec := GoodmanStuhlmuller2013.instReprQUtt.repr }

@[instance_reducible]

instance GoodmanStuhlmuller2013.instInhabitedQUtt : Inhabited QUtt

Equations

• GoodmanStuhlmuller2013.instInhabitedQUtt = { default := GoodmanStuhlmuller2013.instInhabitedQUtt.default }

@[instance_reducible]

instance GoodmanStuhlmuller2013.instFintypeQUtt : Fintype QUtt

Equations

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

def GoodmanStuhlmuller2013.qMeaning : QUtt → WorldState → Prop

Equations

• GoodmanStuhlmuller2013.qMeaning GoodmanStuhlmuller2013.QUtt.none_ x✝ = (x✝.toNat = 0)
• GoodmanStuhlmuller2013.qMeaning GoodmanStuhlmuller2013.QUtt.some_ x✝ = (1 ≤ x✝.toNat)
• GoodmanStuhlmuller2013.qMeaning GoodmanStuhlmuller2013.QUtt.all x✝ = (x✝.toNat = 3)

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning (q : QUtt) : DecidablePred (qMeaning q)

Equations

• GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning GoodmanStuhlmuller2013.QUtt.none_ x✝ = GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning._aux_1 x✝
• GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning GoodmanStuhlmuller2013.QUtt.some_ x✝ = GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning._aux_3 x✝
• GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning GoodmanStuhlmuller2013.QUtt.all x✝ = GoodmanStuhlmuller2013.instDecidablePredWorldStateQMeaning._aux_5 x✝

inductive GoodmanStuhlmuller2013.NumUtt : Type

Numeral alternative set (lower-bound semantics).

• one : NumUtt
• two : NumUtt
• three : NumUtt

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidableEqNumUtt : DecidableEq NumUtt

Equations

• GoodmanStuhlmuller2013.instDecidableEqNumUtt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance GoodmanStuhlmuller2013.instReprNumUtt : Repr NumUtt

Equations

• GoodmanStuhlmuller2013.instReprNumUtt = { reprPrec := GoodmanStuhlmuller2013.instReprNumUtt.repr }

def GoodmanStuhlmuller2013.instReprNumUtt.repr : NumUtt → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance GoodmanStuhlmuller2013.instInhabitedNumUtt : Inhabited NumUtt

Equations

• GoodmanStuhlmuller2013.instInhabitedNumUtt = { default := GoodmanStuhlmuller2013.instInhabitedNumUtt.default }

@[instance_reducible]

instance GoodmanStuhlmuller2013.instFintypeNumUtt : Fintype NumUtt

Equations

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

def GoodmanStuhlmuller2013.lbMeaning : NumUtt → WorldState → Prop

Equations

• GoodmanStuhlmuller2013.lbMeaning GoodmanStuhlmuller2013.NumUtt.one x✝ = (1 ≤ x✝.toNat)
• GoodmanStuhlmuller2013.lbMeaning GoodmanStuhlmuller2013.NumUtt.two x✝ = (2 ≤ x✝.toNat)
• GoodmanStuhlmuller2013.lbMeaning GoodmanStuhlmuller2013.NumUtt.three x✝ = (3 ≤ x✝.toNat)

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning (n : NumUtt) : DecidablePred (lbMeaning n)

Equations

• GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning GoodmanStuhlmuller2013.NumUtt.one x✝ = GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning._aux_1 x✝
• GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning GoodmanStuhlmuller2013.NumUtt.two x✝ = GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning._aux_3 x✝
• GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning GoodmanStuhlmuller2013.NumUtt.three x✝ = GoodmanStuhlmuller2013.instDecidablePredWorldStateLbMeaning._aux_5 x✝

@[reducible, inline]

abbrev GoodmanStuhlmuller2013.Access : Type

Speaker access = number of objects (out of 3) the speaker observes: a Fin 4 indexed at 0..3, so a.val is the access value and Fin (a.val + 1) reduces in type position when a is concrete. The paper restricts to {1, 2, 3}; access 0 (speaker observes nothing) is well-defined but unused.

Equations

• GoodmanStuhlmuller2013.Access = Fin 4

@[reducible, inline]

abbrev GoodmanStuhlmuller2013.Access.a1 : Access

Access value 1 (speaker observes 1 of 3 objects).

Equations

• GoodmanStuhlmuller2013.Access.a1 = 1

@[reducible, inline]

abbrev GoodmanStuhlmuller2013.Access.a2 : Access

Access value 2 (speaker observes 2 of 3 objects).

Equations

• GoodmanStuhlmuller2013.Access.a2 = 2

@[reducible, inline]

abbrev GoodmanStuhlmuller2013.Access.a3 : Access

Access value 3 — full access (speaker observes all 3 objects).

Equations

• GoodmanStuhlmuller2013.Access.a3 = 3

theorem GoodmanStuhlmuller2013.Access.val_le_three (a : Access) : ↑a ≤ 3

theorem GoodmanStuhlmuller2013.Access.a1_val : ↑a1 = 1

theorem GoodmanStuhlmuller2013.Access.a2_val : ↑a2 = 2

theorem GoodmanStuhlmuller2013.Access.a3_val : ↑a3 = 3

World prior — uniform on WorldState

noncomputable def GoodmanStuhlmuller2013.worldPrior : PMF WorldState

Equations

• GoodmanStuhlmuller2013.worldPrior = PMF.uniformOfFintype GoodmanStuhlmuller2013.WorldState

theorem GoodmanStuhlmuller2013.worldPrior_ne_zero (w : WorldState) : worldPrior w ≠ 0

theorem GoodmanStuhlmuller2013.worldPrior_apply (s : WorldState) : worldPrior s = ENNReal.ofReal (1 / 4)

The uniform world prior assigns ENNReal.ofReal (1/4) to every world.

Hypergeometric observation kernel

obsKernel a w : PMF (Fin (a.val + 1)) is the hypergeometric distribution over count outcomes when the speaker observes a.val of the 3 objects, of which w.toNat have the property.

noncomputable def GoodmanStuhlmuller2013.obsKernel (a : Access) (w : WorldState) : PMF (Fin (↑a + 1))

Equations

• GoodmanStuhlmuller2013.obsKernel a w = PMF.hypergeometric 3 w.toNat ↑a ⋯ ⋯

theorem GoodmanStuhlmuller2013.obsKernel_apply (a : Access) (w : WorldState) (k : Fin (↑a + 1)) : (obsKernel a w) k = ↑(w.toNat.choose ↑k * (3 - w.toNat).choose (↑a - ↑k)) / ↑(Nat.choose 3 ↑a)

Closed-form observation kernel value: C(K, k) · C(N-K, n-k) / C(N, n).

theorem GoodmanStuhlmuller2013.obsKernel_apply_ne_zero_iff (a : Access) (w : WorldState) (k : Fin (↑a + 1)) : (obsKernel a w) k ≠ 0 ↔ ↑k ≤ w.toNat ∧ ↑a - ↑k ≤ 3 - w.toNat

The kernel is non-zero iff the count is hypergeometric-feasible.

theorem GoodmanStuhlmuller2013.obsKernel_eq_ofReal (a : Access) (w : WorldState) (k : Fin (↑a + 1)) : (obsKernel a w) k = ENNReal.ofReal (↑(w.toNat.choose ↑k) * ↑((3 - w.toNat).choose (↑a - ↑k)) / ↑(Nat.choose 3 ↑a))

obsKernel value in ENNReal.ofReal form — the shape the value table below reduces to by norm_num.

Observation compatibility and witness worlds

def GoodmanStuhlmuller2013.obsCompatible (a : Access) (k : Fin (↑a + 1)) (s : WorldState) : Prop

A world s is compatible with observing k.val successes out of a.val draws iff the hypergeometric numerator at (K=s.toNat, k=k.val) is non-zero.

Equations

• GoodmanStuhlmuller2013.obsCompatible a k s = (↑k ≤ s.toNat ∧ ↑a - ↑k ≤ 3 - s.toNat)

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidablePredWorldStateObsCompatible (a : Access) (k : Fin (↑a + 1)) : DecidablePred (obsCompatible a k)

Equations

• GoodmanStuhlmuller2013.instDecidablePredWorldStateObsCompatible a k s = GoodmanStuhlmuller2013.instDecidablePredWorldStateObsCompatible._aux_1 a k s

Speaker belief — PMF.posterior of obsKernel

noncomputable def GoodmanStuhlmuller2013.speakerBelief (a : Access) (k : Fin (↑a + 1)) : PMF WorldState

Speaker's posterior over worlds given a count observation.

Equations

• GoodmanStuhlmuller2013.speakerBelief a k = PMF.posterior (GoodmanStuhlmuller2013.obsKernel a) GoodmanStuhlmuller2013.worldPrior k ⋯

Quality filter, literal probabilities, softmax speaker

def GoodmanStuhlmuller2013.qualityOk {U : Type u_1} (m : U → WorldState → Prop) (a : Access) (k : Fin (↑a + 1)) (u : U) : Prop

An utterance u is quality-OK at observation (a, k) iff u is true at every world compatible with (a, k).

Equations

• GoodmanStuhlmuller2013.qualityOk m a k u = ∀ (s : GoodmanStuhlmuller2013.WorldState), GoodmanStuhlmuller2013.obsCompatible a k s → m u s

@[instance_reducible]

instance GoodmanStuhlmuller2013.instDecidablePredQualityOkOfWorldState {U : Type u_1} (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (a : Access) (k : Fin (↑a + 1)) : DecidablePred (qualityOk m a k)

Equations

• GoodmanStuhlmuller2013.instDecidablePredQualityOkOfWorldState m a k u = GoodmanStuhlmuller2013.instDecidablePredQualityOkOfWorldState._aux_1 m a k u

noncomputable def GoodmanStuhlmuller2013.lexReal {U : Type u_1} [Fintype U] (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (u : U) (s : WorldState) : ℝ

Uniform-on-extension literal probability.

Equations

• GoodmanStuhlmuller2013.lexReal m u s = if m u s then (↑(RSA.extensionOf m u).card)⁻¹ else 0

noncomputable def GoodmanStuhlmuller2013.beliefReal (a : Access) (k : Fin (↑a + 1)) (s : WorldState) : ℝ

toReal projection of speakerBelief.

Equations

• GoodmanStuhlmuller2013.beliefReal a k s = ((GoodmanStuhlmuller2013.speakerBelief a k) s).toReal

@[reducible, inline]

noncomputable abbrev GoodmanStuhlmuller2013.s1Score {U : Type u_1} [Fintype U] (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (α : ℝ) (a : Access) (k : Fin (↑a + 1)) (u : U) : ENNReal

Speaker score: softmaxBelief over the literal probabilities, filtered by qualityOk.

Equations

• GoodmanStuhlmuller2013.s1Score m α a k u = RSA.softmaxBelief (GoodmanStuhlmuller2013.lexReal m) (GoodmanStuhlmuller2013.beliefReal a k) α (GoodmanStuhlmuller2013.qualityOk m a k) u

noncomputable def GoodmanStuhlmuller2013.S1g {U : Type u_1} [Fintype U] (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (α : ℝ) (a : Access) (k : Fin (↑a + 1)) (h0 : ∑' (u : U), s1Score m α a k u ≠ 0) : PMF U

Speaker conditional on observation.

Equations

• GoodmanStuhlmuller2013.S1g m α a k h0 = PMF.normalize (fun (x : U) => GoodmanStuhlmuller2013.s1Score m α a k x) h0 ⋯

Marginal speaker and pragmatic listener

Since marginalSpeaker uses PMF.bind (not bindOnSupport), S1g must be defined at every k, not just kernel-supported ones. The cover hypothesis hCov therefore quantifies over all k : Fin (a.val + 1). With WithSilence, this is automatic via cover_silent.

noncomputable def GoodmanStuhlmuller2013.marginalSpeaker {U : Type u_1} [Fintype U] (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (α : ℝ) (a : Access) (w : WorldState) (hCov : ∀ (k : Fin (↑a + 1)), ∃ (u : U), qualityOk m a k u) : PMF U

Equations

• GoodmanStuhlmuller2013.marginalSpeaker m α a w hCov = (GoodmanStuhlmuller2013.obsKernel a w).bind fun (k : Fin (↑a + 1)) => GoodmanStuhlmuller2013.S1g m α a k ⋯

noncomputable def GoodmanStuhlmuller2013.L1 {U : Type u_1} [Fintype U] (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (α : ℝ) (a : Access) (hCov : ∀ (k : Fin (↑a + 1)), ∃ (u : U), qualityOk m a k u) (u : U) (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker m α a w hCov) worldPrior u ≠ 0) : PMF WorldState

Pragmatic listener: Bayesian inversion of the marginal speaker.

Equations

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

theorem GoodmanStuhlmuller2013.cover_silent {U : Type u_1} (m : U → WorldState → Prop) [(u : U) → DecidablePred (m u)] (a : Access) (k : Fin (↑a + 1)) : ∃ (u : RSA.WithSilence U), qualityOk (RSA.liftMeaning m) a k u

Silence is universally qOk — liftMeaning m none holds at every world, so the cover hypothesis is universally satisfiable.

Observation-kernel value table

Closed-form values for obsKernel a w k, derived from obsKernel_eq_ofReal by evaluating the Nat.choose arithmetic. Only the cells the findings below rewrite with are stated.

marginalSpeaker collapse

At full access the kernel concentrates on a single k, so the bind collapses to one S1g evaluation; at partial access it expands to the 2- or 3-term kernel-weighted sum.

Extension cardinalities for the silence-extended models

Generic s1Score evaluation

When qOk u passes, liftMeaning-lifted utterances have a uniform lex value on the belief support (because: qOk ⇒ m u s holds at all compatible s ⊇ belief support ⇒ lex u s = 1/(card extension)). softmaxBelief_uniform_on_support then collapses s1Score = ENNReal.ofReal (1/c).

s1Score value table

Per-(meaning, access, count, utterance) closed forms. Positive cells go through s1Score_uniform_apply; qOk failures are zero by softmaxBelief_eq_zero_of_not_qOk.

Partition functions

S1g value table

Observation-level cancellation (DPI)

The paper's cancellation principle (informal): as the speaker's observation kernel becomes noisier, the listener's posterior moves closer to the prior. The universally provable structural content is observation-level: if the noisy kernel post-processes the informative one (κ_n s = (κ_i s).bind noise), the state–observation mutual information decreases — a per-state corollary of the data processing inequality (PMF.klDiv_bind_le).

The utterance-level form MI(state; utt_n) ≤ MI(state; utt_i) is NOT a clean DPI corollary: the noisy and informative utterances share the observation as a common parent, so there is no Markov chain state → utt_i → utt_n. The per-(world-pair) orderings in the findings below are numerical evaluations of the model, not corollaries of this theorem.

noncomputable def GoodmanStuhlmuller2013.mutualInfoStateObs {W : Type u_2} {Obs : Type u_3} [Fintype W] [MeasurableSpace Obs] (prior : PMF W) (κ : W → PMF Obs) : ENNReal

Per-state-decomposed mutual information between state and observation: MI(state; obs) = ∑ s, prior s · KL(κ s ‖ prior.bind κ) — the conditional-relative-entropy form, which is what makes the per-state DPI argument applicable.

Equations

• GoodmanStuhlmuller2013.mutualInfoStateObs prior κ = ∑ s : W, prior s * (κ s).klDiv (prior.bind κ)

theorem GoodmanStuhlmuller2013.mutualInfoStateObs_bind_noise_le {W : Type u_2} {Obs : Type u_3} [Fintype W] [Fintype Obs] [MeasurableSpace W] [MeasurableSingletonClass W] [MeasurableSpace Obs] [MeasurableSingletonClass Obs] (prior : PMF W) (κ_i : W → PMF Obs) (noise : Obs → PMF Obs) (h_ac : ∀ (s : W), (κ_i s).toMeasure.AbsolutelyContinuous (prior.bind κ_i).toMeasure) : (mutualInfoStateObs prior fun (s : W) => (κ_i s).bind noise) ≤ mutualInfoStateObs prior κ_i

Observation-level cancellation (DPI form): post-processing the observation kernel through a noise channel decreases the mutual information between state and observation. h_ac is per-state absolute continuity of κ_i s w.r.t. the informative observation marginal.

Findings

The 11 paper findings, stated against WithSilence + liftMeaning so the cover hypothesis is automatically satisfied via cover_silent.

These cells are computational evaluations of the model at specific (meaning, access, world-pair, utterance) tuples, in the paper's expository regime (α = 1, uniform prior), not the fitted regime (higher α, non-uniform prior). Where the fitted model predicts only a marginal implicature (access 2), directions can differ from the plotted predictions.

They are NOT corollaries of a single information-theoretic cancellation theorem. The provable structural content is mutualInfoStateObs_bind_noise_le above; the per-(world-pair) orderings these cells encode are utterance-level claims that depend on the specific lex shape, not just on kernel informativity.

theorem GoodmanStuhlmuller2013.some_full_implicature (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning qMeaning) 1 Access.a3 w ⋯) worldPrior (some QUtt.some_) ≠ 0) : (L1 (RSA.liftMeaning qMeaning) 1 Access.a3 ⋯ (some QUtt.some_) hMarg) WorldState.s2 > (L1 (RSA.liftMeaning qMeaning) 1 Access.a3 ⋯ (some QUtt.some_) hMarg) WorldState.s3

Finding 1: at full access, some favors s2 > s3 (scalar implicature).

theorem GoodmanStuhlmuller2013.two_full_upper_bounded (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a3 w ⋯) worldPrior (some NumUtt.two) ≠ 0) : (L1 (RSA.liftMeaning lbMeaning) 1 Access.a3 ⋯ (some NumUtt.two) hMarg) WorldState.s2 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a3 ⋯ (some NumUtt.two) hMarg) WorldState.s3

Finding 4: at full access, two favors s2 > s3 (upper-bounded reading).

theorem GoodmanStuhlmuller2013.one_full_1v2 (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a3 w ⋯) worldPrior (some NumUtt.one) ≠ 0) : (L1 (RSA.liftMeaning lbMeaning) 1 Access.a3 ⋯ (some NumUtt.one) hMarg) WorldState.s1 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a3 ⋯ (some NumUtt.one) hMarg) WorldState.s2

Finding 6: at full access, one favors s1 > s2.

theorem GoodmanStuhlmuller2013.one_full_1v3 (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a3 w ⋯) worldPrior (some NumUtt.one) ≠ 0) : (L1 (RSA.liftMeaning lbMeaning) 1 Access.a3 ⋯ (some NumUtt.one) hMarg) WorldState.s1 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a3 ⋯ (some NumUtt.one) hMarg) WorldState.s3

Finding 7: at full access, one favors s1 > s3.

.a1 minimal-access findings

Each shows marginalSpeaker (smaller-state) ≤ marginalSpeaker (larger-state), so ¬ L1 (smaller) > L1 (larger). At (.a1, k=0) the target utterance has S1g = 0 (qOk fails); at (.a1, k=1) it has S1g = 4/7. So the comparison reduces to obsKernel(smaller)(k=1) ≤ obsKernel(larger)(k=1).

theorem GoodmanStuhlmuller2013.some_minimal_canceled (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning qMeaning) 1 Access.a1 w ⋯) worldPrior (some QUtt.some_) ≠ 0) : ¬(L1 (RSA.liftMeaning qMeaning) 1 Access.a1 ⋯ (some QUtt.some_) hMarg) WorldState.s2 > (L1 (RSA.liftMeaning qMeaning) 1 Access.a1 ⋯ (some QUtt.some_) hMarg) WorldState.s3

Finding 2: at minimal access, some does NOT favor s2 > s3.

theorem GoodmanStuhlmuller2013.one_minimal_1v2_canceled (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a1 w ⋯) worldPrior (some NumUtt.one) ≠ 0) : ¬(L1 (RSA.liftMeaning lbMeaning) 1 Access.a1 ⋯ (some NumUtt.one) hMarg) WorldState.s1 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a1 ⋯ (some NumUtt.one) hMarg) WorldState.s2

Finding 8: at minimal access, one does NOT favor s1 > s2.

theorem GoodmanStuhlmuller2013.one_minimal_1v3_canceled (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a1 w ⋯) worldPrior (some NumUtt.one) ≠ 0) : ¬(L1 (RSA.liftMeaning lbMeaning) 1 Access.a1 ⋯ (some NumUtt.one) hMarg) WorldState.s1 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a1 ⋯ (some NumUtt.one) hMarg) WorldState.s3

Finding 9: at minimal access, one does NOT favor s1 > s3.

.a2 partial-access findings

theorem GoodmanStuhlmuller2013.some_partial_canceled (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning qMeaning) 1 Access.a2 w ⋯) worldPrior (some QUtt.some_) ≠ 0) : ¬(L1 (RSA.liftMeaning qMeaning) 1 Access.a2 ⋯ (some QUtt.some_) hMarg) WorldState.s2 > (L1 (RSA.liftMeaning qMeaning) 1 Access.a2 ⋯ (some QUtt.some_) hMarg) WorldState.s3

Finding 3: at partial access, some does NOT favor s2 > s3 (equality).

theorem GoodmanStuhlmuller2013.two_partial_weakened (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a2 w ⋯) worldPrior (some NumUtt.two) ≠ 0) : ¬(L1 (RSA.liftMeaning lbMeaning) 1 Access.a2 ⋯ (some NumUtt.two) hMarg) WorldState.s2 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a2 ⋯ (some NumUtt.two) hMarg) WorldState.s3

Finding 5: at partial access, two does NOT favor s2 > s3 (weakened).

theorem GoodmanStuhlmuller2013.one_partial_1v3 (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a2 w ⋯) worldPrior (some NumUtt.one) ≠ 0) : (L1 (RSA.liftMeaning lbMeaning) 1 Access.a2 ⋯ (some NumUtt.one) hMarg) WorldState.s1 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a2 ⋯ (some NumUtt.one) hMarg) WorldState.s3

Finding 10 (HEADLINE): at partial access, one favors s1 > s3.

theorem GoodmanStuhlmuller2013.one_partial_1v2_canceled (hMarg : PMF.marginal (fun (w : WorldState) => marginalSpeaker (RSA.liftMeaning lbMeaning) 1 Access.a2 w ⋯) worldPrior (some NumUtt.one) ≠ 0) : ¬(L1 (RSA.liftMeaning lbMeaning) 1 Access.a2 ⋯ (some NumUtt.one) hMarg) WorldState.s1 > (L1 (RSA.liftMeaning lbMeaning) 1 Access.a2 ⋯ (some NumUtt.one) hMarg) WorldState.s2

Finding 11: at partial access, one does NOT favor s1 > s2.