@cite{yoon-etal-2020} on mathlib PMF (Phase 2 stress test, S1 submodel)

@cite{yoon-etal-2020}

Fifth stress test for the Phase-2 architecture. Yoon's politeness model contributes one new ingredient: a graded literal meaning (real-valued in [0, 1], not Boolean), driving the L0 layer through RSA.L0OfMeaning rather than RSA.L0OfBoolMeaning. This is the first PMF migration to exercise the ℝ≥0∞-valued meaning operator.

The S1 utility has a different shape from the previous four pilots:

U_S1(u, s; φ) = φ · log L0(u, s) + (1−φ) · E_L0[V|u] − cost(u)

This decomposition (informativity weight · log + social weight · expected value − cost) does not fit RSA.softmaxBelief (no expected-log over a belief; the log is at the true world) and does not fit Kao's rpow (it's exp ∘ linear, not power). It is the fifth distinct S1 shape across five PMF migrations:

Paper	S1 shape	Operator
FG2012	uniform on extension (no rpow)	L0OfBool
Kao2014	(qudProj L0)^α	rpow only
GS2013	exp(α · Σ_s belief · log L0)	softmaxBel.
ScontrasPearl21	(qudProj L0)^α	rpow only
YoonEtAl2020	exp(α · (φ·log + (1-φ)·E[V] - c))	none — custom

This data point is the strongest argument against extracting Yoon's S1 as a sixth shared operator: every model has its own utility decomposition, and they do not factor cleanly through a common abstraction beyond PMF.normalize of an unnormalised score.

PMF stack

• worldPrior : PMF HeartState — uniform on the four heart states
• meaningE : Utterance → HeartState → ℝ≥0∞ — ENNReal.ofReal lift of utteranceSemantics
• L0 : Utterance → PMF HeartState — RSA.L0OfMeaning of meaningE
• s1Score : Phi → HeartState → Utterance → ℝ≥0∞ — Yoon's utility, lifted via ENNReal.ofReal (because the social term mixes log and linear, which only make sense on ℝ)
• S1g : Phi → HeartState → PMF Utterance — PMF.normalize of s1Score
• marginalSpeaker : HeartState → PMF Utterance — PMF.bind over a phiPrior : PMF Phi
• L1 : Utterance → PMF HeartState — PMF.posterior of marginal speaker

Coverage discharge

The .terrible utterance has positive meaning at every state under negation (1 - p w is positive whenever p w < 1, and terrible's meaning is 0 at .h2 → notTerrible .h2 = 1). Combined with Real.exp being strictly positive, this gives every L0 sum non-zero and every S1g support non-empty.

Scope

S1 submodel only (§2 of the original file). The S2 full model (§3) adds a third utility term (ω_pres · log L1(φ̂|u)) and recomputes via combinedUtility — its own migration target. The 8 S1 inference theorems (terrible_map_h0_vs_h3, bad_map_h1_vs_h0, etc.) become L1 inequalities left as sorry pending the PMF-shaped rsa_predict tactic.

Reused from YoonEtAl2020.lean

• HeartState, Utterance, Adjective, Phi — types
• utteranceSemantics, subjectiveValue, utteranceCost, Phi.val
• meaning_bounded — 0 ≤ utteranceSemantics u w ≤ 1

§1. World prior — uniform on HeartState

noncomputable def YoonEtAl2020.PMF.worldPrior : PMF HeartState

Equations

• YoonEtAl2020.PMF.worldPrior = PMF.uniformOfFintype YoonEtAl2020.HeartState

theorem YoonEtAl2020.PMF.worldPrior_ne_zero (w : HeartState) : worldPrior w ≠ 0

§2. Lifted meaning function

The literal semantics is ℚ-valued (point-estimate acceptance proportions from the norming task). Lifted to ℝ≥0∞ via ENNReal.ofReal for PMF.normalize.

noncomputable def YoonEtAl2020.PMF.meaningE (u : Utterance) (w : HeartState) : ENNReal

Equations

• YoonEtAl2020.PMF.meaningE u w = ENNReal.ofReal ↑(YoonEtAl2020.utteranceSemantics u w)

theorem YoonEtAl2020.PMF.meaningE_ne_top (u : Utterance) (w : HeartState) : meaningE u w ≠ ⊤

def YoonEtAl2020.PMF.witnessState : Utterance → HeartState

Witness for the L0 normalisation positivity: every utterance has at least one heart state where its meaning is non-zero. Concretely: terrible is true at .h0, bad at .h0, good/amazing at .h3, and the negated forms get their witness from a state where the base adjective is false (e.g. notTerrible at .h2 because terrible .h2 = 0).

Equations

• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.terrible = YoonEtAl2020.HeartState.h0
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.bad = YoonEtAl2020.HeartState.h0
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.good = YoonEtAl2020.HeartState.h3
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.amazing = YoonEtAl2020.HeartState.h3
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.notTerrible = YoonEtAl2020.HeartState.h2
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.notBad = YoonEtAl2020.HeartState.h2
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.notGood = YoonEtAl2020.HeartState.h0
• YoonEtAl2020.PMF.witnessState YoonEtAl2020.Utterance.notAmazing = YoonEtAl2020.HeartState.h0

theorem YoonEtAl2020.PMF.meaningE_witness_ne_zero (u : Utterance) : meaningE u (witnessState u) ≠ 0

theorem YoonEtAl2020.PMF.meaningE_tsum_ne_zero (u : Utterance) : ∑' (w : HeartState), meaningE u w ≠ 0

theorem YoonEtAl2020.PMF.meaningE_tsum_ne_top (u : Utterance) : ∑' (w : HeartState), meaningE u w ≠ ⊤

§3. L0 — literal listener via RSA.L0OfMeaning

The graded soft-semantic version of L0: mass proportional to acceptance probability, normalised over heart states. This is the FIRST PMF migration to exercise L0OfMeaning (the ℝ≥0∞ variant); the previous four all used L0OfBoolMeaning because their meanings happened to be 0/1.

noncomputable def YoonEtAl2020.PMF.L0 (u : Utterance) : PMF HeartState

Equations

• YoonEtAl2020.PMF.L0 u = RSA.L0OfMeaning YoonEtAl2020.PMF.meaningE u ⋯ ⋯

@[simp]

theorem YoonEtAl2020.PMF.L0_apply (u : Utterance) (w : HeartState) : (L0 u) w = meaningE u w * (∑' (w' : HeartState), meaningE u w')⁻¹

theorem YoonEtAl2020.PMF.L0_eq_zero_iff (u : Utterance) (w : HeartState) : (L0 u) w = 0 ↔ meaningE u w = 0

theorem YoonEtAl2020.PMF.L0_witness_ne_zero (u : Utterance) : (L0 u) (witnessState u) ≠ 0

§4. S1 score — Yoon's custom utility decomposition

s1Score φ w u = if L0(u, w) = 0 ∧ φ ≠ p0 then 0 else exp(α · (φ.val · log L0(u,w) + (1-φ.val) · E_L0[V|u] - cost(u)))

where E_L0[V|u] = Σ_w' L0(u, w') · V(w'). The φ=0 gate keeps utterances with zero literal mass viable for the pure-social speaker (whose log weight is 0, making 0 · log 0 = 0 non-issues).

Real-valued internally, lifted to ℝ≥0∞ at the PMF.normalize boundary. The score is positive iff L0(u, w) ≠ 0 ∨ φ = p0 — the cover witness shape needed for the PMF.normalize precondition.

noncomputable def YoonEtAl2020.PMF.alpha : ℝ

α = 3 matches the S1 submodel's value (paper uses BDA-fitted ≈4.47).

Equations

• YoonEtAl2020.PMF.alpha = 3

theorem YoonEtAl2020.PMF.alpha_pos : 0 < alpha

noncomputable def YoonEtAl2020.PMF.L0Real (u : Utterance) (w : HeartState) : ℝ

Real projection of L0 (drops the ENNReal wrapping).

Equations

• YoonEtAl2020.PMF.L0Real u w = ((YoonEtAl2020.PMF.L0 u) w).toReal

theorem YoonEtAl2020.PMF.L0Real_nonneg (u : Utterance) (w : HeartState) : 0 ≤ L0Real u w

noncomputable def YoonEtAl2020.PMF.expectedValue (u : Utterance) : ℝ

Expected subjective value under the literal listener.

Equations

• YoonEtAl2020.PMF.expectedValue u = ∑ w' : YoonEtAl2020.HeartState, YoonEtAl2020.PMF.L0Real u w' * ↑(YoonEtAl2020.subjectiveValue w')

noncomputable def YoonEtAl2020.PMF.s1Utility (φ : Phi) (w : HeartState) (u : Utterance) : ℝ

Yoon's S1 utility (the argument of exp).

Equations

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

noncomputable def YoonEtAl2020.PMF.s1Score (φ : Phi) (w : HeartState) (u : Utterance) : ENNReal

The unnormalised speaker score, with the φ=0 gate.

Equations

• YoonEtAl2020.PMF.s1Score φ w u = if YoonEtAl2020.PMF.L0Real u w = 0 ∧ φ ≠ YoonEtAl2020.Phi.p0 then 0 else ENNReal.ofReal (Real.exp (YoonEtAl2020.PMF.s1Utility φ w u))

theorem YoonEtAl2020.PMF.s1Score_ne_top (φ : Phi) (w : HeartState) (u : Utterance) : s1Score φ w u ≠ ⊤

theorem YoonEtAl2020.PMF.s1Score_tsum_ne_top (φ : Phi) (w : HeartState) : ∑' (u : Utterance), s1Score φ w u ≠ ⊤

Cover discharge

For each (φ, w), we need a witness utterance u with s1Score φ w u ≠ 0.

The simplest cover: pick u such that L0Real u w ≠ 0. Then the φ-gate is bypassed and the score is exp(...) > 0.

For each heart state, some utterance has positive L0 mass (verified by inspection: e.g. terrible at .h0, bad at .h0, good at .h2, amazing at .h3). We package this as a per-state witness function.

def YoonEtAl2020.PMF.coverUtterance : HeartState → Utterance

Equations

• YoonEtAl2020.PMF.coverUtterance YoonEtAl2020.HeartState.h0 = YoonEtAl2020.Utterance.terrible
• YoonEtAl2020.PMF.coverUtterance YoonEtAl2020.HeartState.h1 = YoonEtAl2020.Utterance.bad
• YoonEtAl2020.PMF.coverUtterance YoonEtAl2020.HeartState.h2 = YoonEtAl2020.Utterance.good
• YoonEtAl2020.PMF.coverUtterance YoonEtAl2020.HeartState.h3 = YoonEtAl2020.Utterance.amazing

theorem YoonEtAl2020.PMF.meaningE_coverUtterance_ne_zero (w : HeartState) : meaningE (coverUtterance w) w ≠ 0

theorem YoonEtAl2020.PMF.L0_coverUtterance_ne_zero (w : HeartState) : (L0 (coverUtterance w)) w ≠ 0

theorem YoonEtAl2020.PMF.L0Real_coverUtterance_ne_zero (w : HeartState) : L0Real (coverUtterance w) w ≠ 0

theorem YoonEtAl2020.PMF.s1Score_coverUtterance_ne_zero (φ : Phi) (w : HeartState) : s1Score φ w (coverUtterance w) ≠ 0

theorem YoonEtAl2020.PMF.s1Score_tsum_ne_zero (φ : Phi) (w : HeartState) : ∑' (u : Utterance), s1Score φ w u ≠ 0

Per-utterance witness (for the L1 marginal direction)

Dual to coverUtterance: for each utterance u, witnessState u is a heart state where L0(u) has positive mass, giving s1Score φ (witnessState u) u ≠ 0 for any φ. Used to discharge L1_marginal_ne_zero.

theorem YoonEtAl2020.PMF.L0Real_witness_ne_zero (u : Utterance) : L0Real u (witnessState u) ≠ 0

theorem YoonEtAl2020.PMF.s1Score_witness_ne_zero (φ : Phi) (u : Utterance) : s1Score φ (witnessState u) u ≠ 0

§5. S1g — speaker conditional on (φ, world)

noncomputable def YoonEtAl2020.PMF.S1g (φ : Phi) (w : HeartState) : PMF Utterance

Equations

• YoonEtAl2020.PMF.S1g φ w = PMF.normalize (YoonEtAl2020.PMF.s1Score φ w) ⋯ ⋯

theorem YoonEtAl2020.PMF.mem_support_S1g_iff (φ : Phi) (w : HeartState) (u : Utterance) : u ∈ (S1g φ w).support ↔ s1Score φ w u ≠ 0

theorem YoonEtAl2020.PMF.S1g_coverUtterance_ne_zero (φ : Phi) (w : HeartState) : (S1g φ w) (coverUtterance w) ≠ 0

§6. Marginal speaker — PMF.bind over a kindness prior

The speaker marginalises over their (latent) kindness weight.

noncomputable def YoonEtAl2020.PMF.marginalSpeaker (phiPrior : PMF Phi) (w : HeartState) : PMF Utterance

Equations

• YoonEtAl2020.PMF.marginalSpeaker phiPrior w = phiPrior.bind fun (φ : YoonEtAl2020.Phi) => YoonEtAl2020.PMF.S1g φ w

theorem YoonEtAl2020.PMF.marginalSpeaker_coverUtterance_ne_zero {phiPrior : PMF Phi} {φ : Phi} (hφ : phiPrior φ ≠ 0) (w : HeartState) : (marginalSpeaker phiPrior w) (coverUtterance w) ≠ 0

§7. L1 — Bayesian inversion via PMF.posterior

theorem YoonEtAl2020.PMF.L1_marginal_ne_zero {phiPrior : PMF Phi} {φ : Phi} (hφ : phiPrior φ ≠ 0) (u : Utterance) : PMF.marginal (marginalSpeaker phiPrior) worldPrior u ≠ 0

noncomputable def YoonEtAl2020.PMF.L1 {phiPrior : PMF Phi} {φ : Phi} (hφ : phiPrior φ ≠ 0) (u : Utterance) : PMF HeartState

Pragmatic listener: PMF.posterior of the φ-marginalised speaker against the world prior. The "L1 = Bayesian inversion" claim is true by construction.

Equations

• YoonEtAl2020.PMF.L1 hφ u = PMF.posterior (YoonEtAl2020.PMF.marginalSpeaker phiPrior) YoonEtAl2020.PMF.worldPrior u ⋯