@cite{nouwen-2024} on mathlib PMF — chained-RSA structural shell

@cite{nouwen-2024} @cite{lassiter-goodman-2017}

@cite{nouwen-2024} ("The semantics and probabilistic pragmatics of deadjectival intensifiers", Semantics & Pragmatics 17:2, 1-45, 2024) gives an intersective semantic analysis of intensified adjectives (horribly warm, pleasantly warm) plus a chained-Bayesian pragmatic update. This file formalises a structural skeleton of the §4 Bayesian machinery, with explicit acknowledgment of what it does and does not capture.

Scope (honest reckoning, post-audit)

The file's priorAfterEvalPos + seqAdjL1HorriblyWarm correctly implement the two-update Bayesian chain of @cite{nouwen-2024} Eq. 73 (p. 2:41): first update Π = stage-1 L1 at .eval_pos, then second update ρ = stage-2 L1 with Π as prior. The L&G "two priors" pattern (Π enters both stage-2 L0 via L0LassiterGoodman AND stage-2 L1 via PMF.posterior) is structurally faithful.

However, the file is NOT a faithful Nouwen 2024 formalisation. It is "L&G two-priors chain typed against Height", missing three core pieces of Nouwen's actual contribution:

1. Eq. 44/45 intersecting positive forms — NOT formalised. Nouwen's novel semantic proposal (paper p. 2:21) is the conjunction (μ_A(x) ≥ θ_i) ∧ (μ_D(λw.μ_A(x)(@) = μ_A(x)(w)) ≥ θ_j). The second conjunct is a Wheeler-style factive embedding of the proposition "x has its actual measure" — explicitly motivated as the fix for the soup-too-warm-to-eat counterexample to Nouwen 2010 Eq. 35. The file's stage-1 evaluative meaning predicates muHorrible of heights directly, without the propositional embedding. Without Eq. 44b's factive layer, the prediction is L&G's, not Nouwen's. Stub theorem eq_44b_factive_embedding_NOT_FORMALISED below documents the gap.
2. Eq. 49 QUD partition Q^A_X — NOT formalised. Nouwen's σ/ρ are defined over equivalence classes [w]_~^A_X where w ~^A_X w' iff μ_A(x)(w) ≈ μ_A(x)(w') (with explicit granularity). The file operates over raw Height with no quotient/equivalence relation. At small Height-cardinality the partition collapses to identity and the shortcut is vacuously fine for the toy example, but the file cannot extend to Nouwen's Figures 4-7 construction (which depends on the QUD partition + measure-function-on-cells distinction). Stub theorem eq_49_qud_partition_NOT_FORMALISED below documents the gap.
3. muHorrible is monotone-decreasing, NOT Nouwen's f(x) = x² quadratic. Nouwen's Figure 4(b) (p. 2:27) handcrafts f(x) = x² so BOTH extremes (low + high temperature) are evaluated as horrible — this is what produces the Goldilocks shape in Figures 5-7. The file's muHorrible (deg 0) = 3, deg 5 = 0 is monotone in h.toNat, NOT quadratic-in-distance-from-mean. The file's seq_horribly_shifts_upward_pmf is therefore the WRONG headline shape for Goldilocks: it captures monotone shift, not extremes-vs- middle. UNVERIFIED-NOTE: the bundled Nouwen2024.lean's muHorrible was originally built for the bundled-API Goldilocks demo and may itself need correction.

Also not captured (substrate gaps):

• Zwicky's generalisation (paper §5, the third of Nouwen's three desiderata p. 2:15) — the vacuity argument for positive modal adverbs (usually, normally, possibly) is entirely absent. No modal lex, no usually utterance, no theorem stating that usually warm ≈ warm because the adverb's update is vacuous against a normality-shaped prior.
• Positive-valence Goldilocks half (Figure 8, pleasantly warm → narrow moderate peak) — only the negative-valence case is built in the PMF face. The bundled Nouwen2024.lean has the positive-valence symmetric pair; lifting it to PMF requires rebuilding stage-2 with muPleasant + corrected f.

Connection to LassiterGoodman2017PMF.lean

@cite{nouwen-2024} §4 explicitly adopts the @cite{lassiter-goodman-2017} RSA framework and modifies it to sequential two-update inference (vs L&G's single-step joint posterior over (world, threshold)). The structural relationship:

• L&G 2017 PMF: single-step posterior κ μ b against a uniform threshold prior
• Nouwen 2024 PMF (this file): chained posterior κ₂ (posterior κ₁ μ b₁) b₂

The chained-posterior decomposition lemma PMF.posterior_chained_lt_iff_score_lt in Core/Probability/Posterior.lean (modeled on mathlib's Mathlib.Probability.Kernel.Posterior.posterior_comp) characterises this shape; the headline below uses it.

Cross-framework positioning (linglib's "make incompatibilities visible")

@cite{nouwen-2024} §3.1 surveys four contenders for intensifier semantics, Nouwen's own intersection proposal being the FOURTH:

1. Wheeler 1972 factive: horrible(λw. μ_warm(t)(w) = μ_warm(t)(@)) (Eq. 32)
2. Morzycki 2008 extreme: horribly warm = "horrible how extremely warm"
3. Nouwen 2010 existential boost: ∃d[μ_warm(t)(@) ≥ d ∧ horrible(λw.μ_warm(t)(w) ≥ d)] (Eq. 33-35)
4. Nouwen 2024 intersection: Eq. 44/45 (this file's nominal target)

NONE of (1)-(3) are formalised in linglib. Theories/Semantics/Gradability/Intensification.lean ships only Nouwen 2024's intersection as intensifiedMeaning — silently adopting one of the four contenders as if uncontested. The cross-framework auditor flagged this as a broader linglib gap; the fix is an IntensifierSemantics typeclass at the Theory level (deferred — out of scope for this file).

Proof obligations (sorry'd, honestly motivated)

• seq_horribly_shifts_upward_pmf (numeric arithmetic core) — same wall as LassiterGoodman2017PMF's headline; structural decomposition reaches product-of-scores via posterior_chained_lt_iff_score_lt, then halts.
• eq_44b_factive_embedding_NOT_FORMALISED — Nouwen's novel contribution.
• eq_49_qud_partition_NOT_FORMALISED — explicit substrate gap.

Reused from Nouwen2024.lean (bundled formalization)

• Height, Threshold, EvalUtterance, evalMeaning, muHorrible, tallMeaning, heightPrior — data + Boolean meanings
• evalCost, adjCost — cost values

§1. Height prior as a PMF

noncomputable def RSA.Nouwen2024.PMF.heightPriorENN (h : Height) : ENNReal

Height prior weights as ℝ≥0∞. Reuses heightPrior : Height → ℚ from Nouwen2024.lean (a discretized bell curve, weights summing to 52).

Equations

• RSA.Nouwen2024.PMF.heightPriorENN h = ENNReal.ofReal ↑(RSA.Nouwen2024.heightPrior h)

theorem RSA.Nouwen2024.PMF.heightPriorENN_pos (h : Height) : heightPriorENN h ≠ 0

theorem RSA.Nouwen2024.PMF.heightPriorENN_finite (h : Height) : heightPriorENN h ≠ ⊤

noncomputable def RSA.Nouwen2024.PMF.heightPriorPMF : PMF Height

The height prior as a normalized PMF Height. Built directly from mathlib's PMF.normalize with the Fintype-shape tsum discharges: tsum_ne_zero_iff (witness form) and tsum_ne_top_of_fintype.

Equations

• RSA.Nouwen2024.PMF.heightPriorPMF = PMF.normalize RSA.Nouwen2024.PMF.heightPriorENN RSA.Nouwen2024.PMF.heightPriorPMF._proof_2 RSA.Nouwen2024.PMF.heightPriorPMF._proof_3

theorem RSA.Nouwen2024.PMF.heightPriorPMF_pos (h : Height) : heightPriorPMF h ≠ 0

§2. ValidThreshold subtype + conversion

@[reducible, inline]

abbrev RSA.Nouwen2024.PMF.ValidThreshold : Type

The latent threshold restricted to values with non-empty .eval_pos extension under muHorrible / muPleasant. Both measures have max value 3, so θ.toNat ∈ {0,1,2} are the only thresholds that produce non-empty literal-listener extensions (per ## Empty-extension in the module docstring).

Equations

• RSA.Nouwen2024.PMF.ValidThreshold = Fin 3

def RSA.Nouwen2024.PMF.validToThreshold (vt : ValidThreshold) : Threshold

Convert ValidThreshold into the original Threshold = Fin 6 type (via Fin.castLE 3 ≤ 6).

Equations

• RSA.Nouwen2024.PMF.validToThreshold vt = { value := Fin.castLE RSA.Nouwen2024.PMF.validToThreshold._proof_1 vt }

noncomputable def RSA.Nouwen2024.PMF.thresholdPriorPMF : PMF ValidThreshold

Uniform prior over ValidThreshold.

Equations

• RSA.Nouwen2024.PMF.thresholdPriorPMF = PMF.uniformOfFintype RSA.Nouwen2024.PMF.ValidThreshold

§3. Stage 1 — evaluative L0/S1/L1 (under muHorrible)

Pattern: Boolean evalLex → L&G L0 with heightPriorPMF (L0LassiterGoodman) → S1Belief rpow speaker with evalCostFactor and α=4 → marginalize over ValidThreshold via marginalizeKernel → PMF.posterior.

def RSA.Nouwen2024.PMF.evalLex (evalMu : Height → ℕ) (θ : Threshold) (u : EvalUtterance) (h : Height) : Bool

Evaluative Boolean lex at threshold θ (just argument-reordering of Nouwen2024.evalMeaning). Type matches L0LassiterGoodman's shape.

Equations

• RSA.Nouwen2024.PMF.evalLex evalMu θ u h = RSA.Nouwen2024.evalMeaning evalMu u h θ

theorem RSA.Nouwen2024.PMF.evalLex_horrible_extension_pos (vt : ValidThreshold) (u : EvalUtterance) : (∑' (h : Height), heightPriorPMF h * if evalLex muHorrible (validToThreshold vt) u h = true then 1 else 0) ≠ 0

Witness for the L0LassiterGoodman positivity hypothesis at any valid θ and any utterance: deg 0 is in every extension. For .silent trivially; for .eval_pos because muHorrible (deg 0) = 3 > θ.toNat for θ ∈ {0,1,2}.

noncomputable def RSA.Nouwen2024.PMF.evalL0_horribleAt (vt : ValidThreshold) : EvalUtterance → PMF Height

Stage 1 literal listener under muHorrible at valid threshold vt.

Equations

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

noncomputable def RSA.Nouwen2024.PMF.evalCostFactor (u : EvalUtterance) : ENNReal

Cost factor for the rpow speaker form: cost u → exp(-α · cost u). Hardcodes Nouwen's evalCost (eval_pos = 1, silent = 0) and α = 4.

Equations

• RSA.Nouwen2024.PMF.evalCostFactor u = ENNReal.ofReal (Real.exp (-4 * ↑(RSA.Nouwen2024.evalCost u)))

theorem RSA.Nouwen2024.PMF.evalCostFactor_pos (u : EvalUtterance) : evalCostFactor u ≠ 0

theorem RSA.Nouwen2024.PMF.evalCostFactor_finite (u : EvalUtterance) : evalCostFactor u ≠ ⊤

noncomputable def RSA.Nouwen2024.PMF.evalSpeaker_horribleAt (vt : ValidThreshold) (w : Height) : PMF EvalUtterance

Stage 1 speaker under muHorrible at valid threshold vt. Per-θ S1Belief, normalized over utterances at each Height. Positivity discharges via .silent witness using RSA.L0LassiterGoodman_apply_of_meaning_true (which says: L0 at .silent equals the prior unchanged, since evalLex .silent is identically true).

Equations

• RSA.Nouwen2024.PMF.evalSpeaker_horribleAt vt w = RSA.S1Belief (RSA.Nouwen2024.PMF.evalL0_horribleAt vt) RSA.Nouwen2024.PMF.evalCostFactor 4 w ⋯ ⋯

noncomputable def RSA.Nouwen2024.PMF.evalSpeakerMarginalHorrible : Height → PMF EvalUtterance

Marginalize Stage 1 speaker over ValidThreshold (uniform prior). Eq 70's marginalization step, restricted to thresholds with non-empty extension.

Equations

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

noncomputable def RSA.Nouwen2024.PMF.evalL1Horrible (u : EvalUtterance) : PMF Height

Stage 1 L1 = pragmatic listener via PMF.posterior. The prior is heightPriorPMF; the speaker kernel is the threshold-marginalized evalSpeakerMarginalHorrible.

Equations

• RSA.Nouwen2024.PMF.evalL1Horrible u = PMF.posterior RSA.Nouwen2024.PMF.evalSpeakerMarginalHorrible RSA.Nouwen2024.PMF.heightPriorPMF u ⋯

§4. Sequential composition: Π = stage 1 L1 at .eval_pos

This Π becomes the prior for stage 2 (Nouwen eq 73). The L&G "two priors" pattern then has Π appearing both inside the stage-2 L0 (via L0LassiterGoodman Π adjLex) and outside in the stage-2 L1 (via PMF.posterior _ Π).

noncomputable def RSA.Nouwen2024.PMF.priorAfterEvalPos : PMF Height

Π — stage 1 L1 at .eval_pos, used as stage 2's prior.

Equations

• RSA.Nouwen2024.PMF.priorAfterEvalPos = RSA.Nouwen2024.PMF.evalL1Horrible RSA.Nouwen2024.EvalUtterance.eval_pos

§5. Stage 2 — adjective L0/S1/L1 (under tallMeaning/warm)

Mirrors stage 1 with prior Π instead of heightPriorPMF, and with the bare-warm Boolean tallMeaning instead of evalMeaning.

def RSA.Nouwen2024.PMF.adjLex (θ : Threshold) (u : AdjUtterance) (h : Height) : Bool

Adjective Boolean lex at threshold θ. Reuses Nouwen's AdjUtterance (warm | silent) and adjMeaning.

Equations

• RSA.Nouwen2024.PMF.adjLex θ u h = RSA.Nouwen2024.adjMeaning u h θ

theorem RSA.Nouwen2024.PMF.priorAfterEvalPos_pos_at_horrible_pos {h : Height} (hpos : 0 < muHorrible h) : priorAfterEvalPos h ≠ 0

Restricted version of "Π is positive": Π is positive at heights with non-zero muHorrible (the eval listener concludes the height is in the "horribly" extension). At heights where muHorrible h = 0 (e.g. deg 3), Π(h) = 0 — those are precisely the heights "ruled out" by the .eval_pos observation. The unrestricted priorAfterEvalPos_pos would be FALSE at deg 3, which was the bug in the original sorry'd statement.

theorem RSA.Nouwen2024.PMF.adjLex_warm_extension_pos (vt : ValidThreshold) (u : AdjUtterance) : (∑' (h : Height), priorAfterEvalPos h * if adjLex (validToThreshold vt) u h = true then 1 else 0) ≠ 0

Witness for stage 2's L0LassiterGoodman positivity: at threshold θ ∈ {0,1,2} and utterance .warm, the height deg 5 (or any h with tallMeaning θ h = true) gives non-zero contribution.

noncomputable def RSA.Nouwen2024.PMF.adjL0_warmAt (vt : ValidThreshold) : AdjUtterance → PMF Height

Stage 2 literal listener with prior Π (the L&G "two priors" pattern: Π enters here, AND will enter again at the L1 stage).

Equations

• RSA.Nouwen2024.PMF.adjL0_warmAt vt u = RSA.L0LassiterGoodman RSA.Nouwen2024.PMF.priorAfterEvalPos (RSA.Nouwen2024.PMF.adjLex (RSA.Nouwen2024.PMF.validToThreshold vt)) u ⋯

noncomputable def RSA.Nouwen2024.PMF.adjCostFactor (u : AdjUtterance) : ENNReal

Equations

• RSA.Nouwen2024.PMF.adjCostFactor u = ENNReal.ofReal (Real.exp (-4 * ↑(RSA.Nouwen2024.adjCost u)))

noncomputable def RSA.Nouwen2024.PMF.adjSpeaker_warmAt (vt : ValidThreshold) (w : Height) : PMF AdjUtterance

Stage 2 speaker under tallMeaning at valid threshold vt.

Conditional fallback at degenerate worlds: at world w where Π(w) = 0 (e.g., w = deg 3 since muHorrible(deg 3) = 0 so deg 3 has zero posterior under "eval_pos"), all adjL0_warmAt vt u w = 0 (reweight against zero-mass prior gives zero), so S1Belief's positivity hypothesis fails. At those degenerate worlds the speaker is irrelevant to the L1 (since the prior is 0 there too), so we fall back to a vacuous uniform PMF. This is the bundled API's if l0 = 0 then 0 guard, lifted to the type level via dite.

Equations

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

noncomputable def RSA.Nouwen2024.PMF.adjSpeakerMarginal : Height → PMF AdjUtterance

Marginalize Stage 2 speaker over ValidThreshold.

Equations

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

noncomputable def RSA.Nouwen2024.PMF.seqAdjL1HorriblyWarm (u : AdjUtterance) : PMF Height

Sequential L1 for "horribly warm". Stage 2 L1 with prior Π (= stage 1 L1 at .eval_pos). The L&G "two priors" pattern: Π appears in stage 2's L0 (via L0LassiterGoodman inside adjL0_warmAt) AND in stage 2's L1 (the priorAfterEvalPos argument to PMF.posterior here).

Equations

• RSA.Nouwen2024.PMF.seqAdjL1HorriblyWarm u = PMF.posterior RSA.Nouwen2024.PMF.adjSpeakerMarginal RSA.Nouwen2024.PMF.priorAfterEvalPos u ⋯

§6. Predictions (sorry'd, with honest scope notes)

The headline below states that "horribly warm" shifts probability toward high heights (deg 5 > deg 2). HONEST SCOPE: this is the monotone-shift shape, NOT the Goldilocks shape that Nouwen 2024 Figures 5-7 actually depict. Goldilocks would require BOTH extremes (very cold AND very hot) to be evaluated as horrible — Nouwen's f(x) = x² quadratic from Figure 4(b). The file's muHorrible is monotone-decreasing in h.toNat, so the headline is mathematically the right statement for THIS model but the WRONG statement for Nouwen's actual Goldilocks claim. See module docstring §3 of "Scope (honest reckoning)".

theorem RSA.Nouwen2024.PMF.seq_horribly_shifts_upward_pmf : (seqAdjL1HorriblyWarm AdjUtterance.warm) (Core.Scale.deg 5 ⋯) > (seqAdjL1HorriblyWarm AdjUtterance.warm) (Core.Scale.deg 2 ⋯)

The headline shift prediction in PMF form: "horribly warm" pushes probability toward higher heights (under the file's monotone muHorrible).

Discharge structure (as far as structural decomposition reaches):

The chained posterior κ₂ (posterior κ₁ μ b₁) b₂ shape decomposes via PMF.posterior_chained_lt_iff_score_lt (the PMF analogue of mathlib's posterior_comp for chained Bayesian updates) — this is a single rw step that cancels both the inner and outer marginal denominators in one move, reducing the headline to a comparison of products of unnormalised scores μ a · κ₁ a b₁ · κ₂ a b₂.

The remaining residue is the genuine "numeric arithmetic core": each side is a Real.exp-weighted sum over ValidThreshold whose value depends on the marginalised speaker computation. Same wall as LassiterGoodman2017PMF's headline; same wall as the bundled-RSAConfig counterpart (Nouwen2024.seq_horribly_shifts_upward) — bundled passes via rsa_predict reflection on rational arithmetic; PMF face inherits the barrier and sorrys out.

§6'. Substrate gaps documented as sorry'd theorems (Nouwen 2024 not-formalised)

The following stubs explicitly mark what the file does NOT capture from Nouwen 2024. Each is the formal statement of the substrate gap; closing them would require substrate work documented in the module docstring.

theorem RSA.Nouwen2024.PMF.eq_44b_factive_embedding_NOT_FORMALISED : True

Eq. 44b factive embedding (Nouwen 2024 §3.2) — NOT FORMALISED.

Nouwen's novel semantic proposal (paper p. 2:21) requires the adverb's positive form to embed the proposition λw. μ_A(x)(@) = μ_A(x)(w) (Wheeler-style factive layer). The conjunction (μ_A(x) ≥ θ_i) ∧ (μ_D(λw. μ_A(x)(@) = μ_A(x)(w)) ≥ θ_j) is what distinguishes Nouwen 2024's intersection from L&G's straight positive form.

This file's stage-1 evaluative meaning predicates muHorrible of heights directly (evalLex evalMu θ u h := muHorrible h > θ.toNat), without the propositional embedding. Without Eq. 44b's factive layer, the prediction is L&G's, not Nouwen's. Closing requires a Prop/Bool-valued lex over propositions, not just heights — substantial substrate refactor.

theorem RSA.Nouwen2024.PMF.eq_49_qud_partition_NOT_FORMALISED : True

Eq. 49 QUD partition Q^A_X (Nouwen 2024 §4) — NOT FORMALISED.

Nouwen's σ/ρ are defined over equivalence classes of worlds, not raw worlds. The partition Q^A_X = {[w]_~^A_X | w ∈ W} is built from the equivalence w ~^A_X w' iff μ_A(x)(w) ≈ μ_A(x)(w') with explicit granularity ≈ (Nouwen rounds to one decimal in Figure 3).

The file operates over raw Height with no quotient or equivalence relation. At small Height cardinality the partition collapses to identity and the shortcut is vacuously fine for the toy example, but the file cannot extend to Nouwen's Figures 4-7 (which depend on the QUD partition + measure-function-on-cells distinction). Closing requires defining Quotient-typed prior + kernels — substantial substrate refactor.

§7. Structural-decomposition demos (lemma library witnesses)

The following theorems exercise the inequality-decomposition lemmas added in 0.230.387. Each one proves a structural claim about the model that the new lemmas dispatch in 1-2 lines — no numeric arithmetic required. The contrast with seq_horribly_shifts_upward_pmf (which sorrys out the numeric core) is the point: structural shell handles structural claims; the numeric core is reflection territory, regardless of bundling.

theorem RSA.Nouwen2024.PMF.adjL0_warm_meaning_pos_lt_iff_prior_lt (vt : ValidThreshold) (w₁ w₂ : Height) (h₁ : adjLex (validToThreshold vt) AdjUtterance.warm w₁ = true) (h₂ : adjLex (validToThreshold vt) AdjUtterance.warm w₂ = true) : (adjL0_warmAt vt AdjUtterance.warm) w₁ < (adjL0_warmAt vt AdjUtterance.warm) w₂ ↔ priorAfterEvalPos w₁ < priorAfterEvalPos w₂

Order on the stage-2 .warm literal listener at worlds where the adjective extension holds reduces to order on the (eval-stage) prior. Demonstrates L0LassiterGoodman_apply_lt_iff_prior_lt: when the indicator is true at both points, only the prior matters.

In linguistic terms: the literal listener's "warm-ranking" of two heights that BOTH satisfy the threshold inherits the eval-stage L1's ordering. The L0's normalisation by the warm-extension partition cancels.

theorem RSA.Nouwen2024.PMF.adjL0_silent_eq_prior (vt : ValidThreshold) (w : Height) : (adjL0_warmAt vt AdjUtterance.silent) w = priorAfterEvalPos w

The silent utterance's literal listener IS the eval-stage prior pointwise. Direct application of L0LassiterGoodman_apply_of_meaning_true (the silent utterance has trivially-true meaning at every world).

This is the "vacuous-utterance reduction": informationally-empty utterances leave the listener's beliefs unchanged from the prior.