[Nou24] Deadjectival Intensifiers

[LG17] [Nou24]

"The semantics and probabilistic pragmatics of deadjectival intensifiers" Semantics and Pragmatics, Volume 17, Article 2.

Empirical Generalizations

1. Goldilocks effect: Negative-evaluative bases (horrible, terrible) yield high-degree intensifiers; positive-evaluative bases (pleasant, nice) yield moderate-degree intensifiers.

2. Zwicky's generalization: Modal adjectives with negative polarity (unusual, surprising, impossible) can intensify, but their positive counterparts (usual, expected, possible) cannot.

RSA Model

Extends [LG17] threshold RSA with evaluative measures: deadjectival adverbs (horribly, pleasantly) derive their degree function from the evaluative meaning of their adjectival base.

Measure function simplification: The paper uses f(x) = x² for negative evaluation and a Gaussian for positive evaluation (handcrafted proof-of-concept functions). Our formalization uses |d − norm| and norm − |d − norm| respectively (linear/triangular). Both preserve the qualitative shape: negative measures peak at extremes, positive measures peak at the norm.

Probabilistic model

The RSA model — the rejected simultaneous dual-threshold configuration (Nouwen's (49)) and the paper's final sequential/backgrounded chain (eqs. 50–51) — lives on the mathlib-PMF face in the "Probabilistic model" sections below, where the predictions are proven structurally: ratio cancellation collapses each marginalised speaker to a mass-monotone sum over the licensed thresholds, and informativity monotonicity beats the prior ratio. This file houses the semantic layer: the intensifier lexicon, the meaning functions and their theory-layer grounding, the exact Goldilocks boundary, the Wheeler leak, and the licensing-support order.

inductive Nouwen2024.Intensifiers.IntensifierClass : Type

Intensifier degree class (Figure 2).

• H (high): targets extreme degrees ("horribly warm" ≈ very warm)
• M (moderate): targets moderate degrees ("pleasantly warm" ≈ nicely warm)

• H : IntensifierClass
• M : IntensifierClass

@[implicit_reducible]

instance Nouwen2024.Intensifiers.instReprIntensifierClass : Repr IntensifierClass

Equations

• Nouwen2024.Intensifiers.instReprIntensifierClass = { reprPrec := Nouwen2024.Intensifiers.instReprIntensifierClass.repr }

def Nouwen2024.Intensifiers.instReprIntensifierClass.repr : IntensifierClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Nouwen2024.Intensifiers.instDecidableEqIntensifierClass : DecidableEq IntensifierClass

Equations

• Nouwen2024.Intensifiers.instDecidableEqIntensifierClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Nouwen2024.Intensifiers.BaseKind : Type

Classification of adjectival base for deadjectival intensifiers ([Nou24] §2.4).

• evaluative: core case — horrible, pleasant, nice
• mirative: non-evaluative but extremity-sensitive — unusual, surprising, remarkable
• modal: epistemic modals — impossible, possible, usual, expected
• dimensional: degree adjectives — tall, short (not productive as intensifiers)

• evaluative : BaseKind
• mirative : BaseKind
• modal : BaseKind
• dimensional : BaseKind

@[implicit_reducible]

instance Nouwen2024.Intensifiers.instReprBaseKind : Repr BaseKind

Equations

• Nouwen2024.Intensifiers.instReprBaseKind = { reprPrec := Nouwen2024.Intensifiers.instReprBaseKind.repr }

def Nouwen2024.Intensifiers.instReprBaseKind.repr : BaseKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Nouwen2024.Intensifiers.instDecidableEqBaseKind : DecidableEq BaseKind

Equations

• Nouwen2024.Intensifiers.instDecidableEqBaseKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

structure Nouwen2024.Intensifiers.IntensifierEntry : Type

A deadjectival intensifier entry.

Records the adverb form, its adjectival base, evaluative properties, modal status, and attestation pattern.

• adverb : String

  Adverb form

• adjBase : String

  Adjectival base

• valence : Features.EvaluativeValence

  Evaluative valence of the base

• class_ : IntensifierClass

  Degree class as intensifier

• baseKind : BaseKind

  Base classification: evaluative, mirative, modal, or dimensional

• deviationPolarity : Option Features.EvaluativeValence

  Deviation polarity: whether the base denotes deviation from or conformity with expectation/norm.

  • some .negative = deviation (unusual, impossible, horrible)
  • some .positive = conformity (usual, expected, possible)
  • none = not applicable (evaluative bases without modal/mirative content) Named deviationPolarity rather than modalPolarity because miratives are not modal (§2.4.2) — the shared property is deviation from norm.
• bleached : Bool

  Whether the evaluative content is bleached in adverbial use

• attested : Bool

  Whether the intensifier use is attested

• goldilocksException : Bool

  Goldilocks exception: extreme positive evaluatives (remarkable, stunning) are H-degree despite positive valence. The paper acknowledges (p. 2:9) that extreme evaluations and manner implicatures can override the default valence→class mapping.

@[implicit_reducible]

instance Nouwen2024.Intensifiers.instReprIntensifierEntry : Repr IntensifierEntry

Equations

• Nouwen2024.Intensifiers.instReprIntensifierEntry = { reprPrec := Nouwen2024.Intensifiers.instReprIntensifierEntry.repr }

def Nouwen2024.Intensifiers.instReprIntensifierEntry.repr : IntensifierEntry → ℕ → Std.Format

Equations

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

def Nouwen2024.Intensifiers.horribly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.terribly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.awfully : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.dreadfully : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.frighteningly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.pleasantly : IntensifierEntry

Equations

• Nouwen2024.Intensifiers.pleasantly = { adverb := "pleasantly", adjBase := "pleasant", valence := Features.EvaluativeValence.positive, class_ := Nouwen2024.Intensifiers.IntensifierClass.M }

def Nouwen2024.Intensifiers.nicely : IntensifierEntry

Equations

• Nouwen2024.Intensifiers.nicely = { adverb := "nicely", adjBase := "nice", valence := Features.EvaluativeValence.positive, class_ := Nouwen2024.Intensifiers.IntensifierClass.M }

def Nouwen2024.Intensifiers.decently : IntensifierEntry

Equations

• Nouwen2024.Intensifiers.decently = { adverb := "decently", adjBase := "decent", valence := Features.EvaluativeValence.positive, class_ := Nouwen2024.Intensifiers.IntensifierClass.M }

def Nouwen2024.Intensifiers.unusually : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.surprisingly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.impossibly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.remarkably : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.usually_ : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.expectedly_ : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.possibly_ : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.disgustingly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.annoyingly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.unpleasantly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.scarily : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.wonderfully : IntensifierEntry

Equations

• Nouwen2024.Intensifiers.wonderfully = { adverb := "wonderfully", adjBase := "wonderful", valence := Features.EvaluativeValence.positive, class_ := Nouwen2024.Intensifiers.IntensifierClass.M }

def Nouwen2024.Intensifiers.beautifully_ : IntensifierEntry

Equations

• Nouwen2024.Intensifiers.beautifully_ = { adverb := "beautifully", adjBase := "beautiful", valence := Features.EvaluativeValence.positive, class_ := Nouwen2024.Intensifiers.IntensifierClass.M }

def Nouwen2024.Intensifiers.delightfully : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.gorgeously : IntensifierEntry

Equations

• Nouwen2024.Intensifiers.gorgeously = { adverb := "gorgeously", adjBase := "gorgeous", valence := Features.EvaluativeValence.positive, class_ := Nouwen2024.Intensifiers.IntensifierClass.M }

def Nouwen2024.Intensifiers.stunningly : IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.allEntries : List IntensifierEntry

Equations

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

def Nouwen2024.Intensifiers.goldilocksHolds (e : IntensifierEntry) : Bool

The Goldilocks effect (§2.3): base kind and valence determine degree class.

• Negative-evaluative bases yield high-degree (H) intensifiers
• Positive-evaluative bases yield moderate-degree (M) intensifiers
• Miratives always yield H (deviation from expectation targets extremes; §2.4.2)
• Modals: negative deviation → H, positive (conformity) → M
• Goldilocks exceptions (e.g., remarkably, stunningly): extreme positive evaluatives that yield H despite positive valence (p. 2:9)

Equations

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

theorem Nouwen2024.Intensifiers.horribly_goldilocks : goldilocksHolds horribly = true

theorem Nouwen2024.Intensifiers.terribly_goldilocks : goldilocksHolds terribly = true

theorem Nouwen2024.Intensifiers.awfully_goldilocks : goldilocksHolds awfully = true

theorem Nouwen2024.Intensifiers.dreadfully_goldilocks : goldilocksHolds dreadfully = true

theorem Nouwen2024.Intensifiers.frighteningly_goldilocks : goldilocksHolds frighteningly = true

theorem Nouwen2024.Intensifiers.disgustingly_goldilocks : goldilocksHolds disgustingly = true

theorem Nouwen2024.Intensifiers.annoyingly_goldilocks : goldilocksHolds annoyingly = true

theorem Nouwen2024.Intensifiers.unpleasantly_goldilocks : goldilocksHolds unpleasantly = true

theorem Nouwen2024.Intensifiers.scarily_goldilocks : goldilocksHolds scarily = true

theorem Nouwen2024.Intensifiers.pleasantly_goldilocks : goldilocksHolds pleasantly = true

theorem Nouwen2024.Intensifiers.nicely_goldilocks : goldilocksHolds nicely = true

theorem Nouwen2024.Intensifiers.decently_goldilocks : goldilocksHolds decently = true

theorem Nouwen2024.Intensifiers.wonderfully_goldilocks : goldilocksHolds wonderfully = true

theorem Nouwen2024.Intensifiers.beautifully_goldilocks : goldilocksHolds beautifully_ = true

theorem Nouwen2024.Intensifiers.delightfully_goldilocks : goldilocksHolds delightfully = true

theorem Nouwen2024.Intensifiers.gorgeously_goldilocks : goldilocksHolds gorgeously = true

theorem Nouwen2024.Intensifiers.unusually_goldilocks : goldilocksHolds unusually = true

theorem Nouwen2024.Intensifiers.surprisingly_goldilocks : goldilocksHolds surprisingly = true

theorem Nouwen2024.Intensifiers.impossibly_goldilocks : goldilocksHolds impossibly = true

theorem Nouwen2024.Intensifiers.remarkably_goldilocks : goldilocksHolds remarkably = true

theorem Nouwen2024.Intensifiers.stunningly_goldilocks : goldilocksHolds stunningly = true

def Nouwen2024.Intensifiers.zwickyHolds (e : IntensifierEntry) : Bool

Zwicky's generalization (§2.5, [zwicky-1970]): among modal/mirative adjectives, only those denoting deviation from expectation (negative deviation polarity) can serve as intensifiers; conformity-denoting ones (positive deviation polarity) cannot.

• "unusually warm" ✓ (deviation → attested)
• "impossibly warm" ✓ (deviation → attested)
• "*usually warm" ✗ (conformity → unattested)

This restriction does NOT extend to evaluatives (§2.5, (28)-(30)): both "pleasantly warm" and "unpleasantly warm" are attested.

Equations

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

theorem Nouwen2024.Intensifiers.unusually_zwicky : zwickyHolds unusually = true

theorem Nouwen2024.Intensifiers.surprisingly_zwicky : zwickyHolds surprisingly = true

theorem Nouwen2024.Intensifiers.impossibly_zwicky : zwickyHolds impossibly = true

theorem Nouwen2024.Intensifiers.usually_zwicky : zwickyHolds usually_ = true

theorem Nouwen2024.Intensifiers.expectedly_zwicky : zwickyHolds expectedly_ = true

theorem Nouwen2024.Intensifiers.possibly_zwicky : zwickyHolds possibly_ = true

def Nouwen2024.Intensifiers.attestedCount : ℕ

Count of attested intensifiers

Equations

• Nouwen2024.Intensifiers.attestedCount = (List.filter (fun (x : Nouwen2024.Intensifiers.IntensifierEntry) => x.attested) Nouwen2024.Intensifiers.allEntries).length

def Nouwen2024.Intensifiers.unattestedCount : ℕ

Count of unattested intensifiers

Equations

• Nouwen2024.Intensifiers.unattestedCount = (List.filter (fun (x : Nouwen2024.Intensifiers.IntensifierEntry) => !x.attested) Nouwen2024.Intensifiers.allEntries).length

def Nouwen2024.Intensifiers.IntensifierEntry.fragmentEntry (e : IntensifierEntry) : Option Semantics.Gradability.GradableAdjective

Look up the Fragment adjective entry for an intensifier's adjectival base.

Equations

• e.fragmentEntry = English.Predicates.Adjectival.lookup e.adjBase

theorem Nouwen2024.Intensifiers.pleasant_valence_bridge : (pleasantly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

Bridge: pleasant's Fragment entry has positive evaluative valence, matching the intensifier layer's valence for pleasantly.

theorem Nouwen2024.Intensifiers.nice_valence_bridge : (nicely.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

Bridge: nice's Fragment entry has positive evaluative valence, matching the intensifier layer's valence for nicely.

theorem Nouwen2024.Intensifiers.decent_valence_bridge : (decently.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

Bridge: decent's Fragment entry has positive evaluative valence, matching the intensifier layer's valence for decently.

theorem Nouwen2024.Intensifiers.beautiful_valence_bridge : (beautifully_.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

Bridge: beautiful's Fragment entry has positive evaluative valence, matching the intensifier layer's valence for beautifully.

theorem Nouwen2024.Intensifiers.horrible_valence_bridge : (horribly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.terrible_valence_bridge : (terribly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.awful_valence_bridge : (awfully.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.dreadful_valence_bridge : (dreadfully.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.frightening_valence_bridge : (frighteningly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.disgusting_valence_bridge : (disgustingly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.annoying_valence_bridge : (annoyingly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.unpleasant_valence_bridge : (unpleasantly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.scary_valence_bridge : (scarily.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.negative

theorem Nouwen2024.Intensifiers.wonderful_valence_bridge : (wonderfully.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

theorem Nouwen2024.Intensifiers.delightful_valence_bridge : (delightfully.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

theorem Nouwen2024.Intensifiers.gorgeous_valence_bridge : (gorgeously.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

theorem Nouwen2024.Intensifiers.unusual_valence_bridge : (unusually.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.neutral

theorem Nouwen2024.Intensifiers.surprising_valence_bridge : (surprisingly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.neutral

theorem Nouwen2024.Intensifiers.remarkable_valence_bridge : (remarkably.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

theorem Nouwen2024.Intensifiers.stunning_valence_bridge : (stunningly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.positive

theorem Nouwen2024.Intensifiers.usual_valence_bridge : (usually_.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.neutral

theorem Nouwen2024.Intensifiers.expected_valence_bridge : (expectedly_.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.neutral

theorem Nouwen2024.Intensifiers.possible_valence_bridge : (possibly_.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.neutral

theorem Nouwen2024.Intensifiers.impossible_valence_bridge : (impossibly.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) = some Features.EvaluativeValence.neutral

theorem Nouwen2024.Intensifiers.all_bases_resolve : (allEntries.all fun (x : IntensifierEntry) => x.fragmentEntry.isSome) = true

Every intensifier entry's adjectival base resolves to a Fragment entry.

theorem Nouwen2024.Intensifiers.all_valences_agree : (allEntries.all fun (e : IntensifierEntry) => (e.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.evaluativeValence) == some e.valence) = true

Every intensifier entry's evaluative valence matches its Fragment entry's. This is the key integration theorem: changes to either the intensifier data or the Fragment entries will break this if they disagree.

theorem Nouwen2024.Intensifiers.all_bases_open_scale : (allEntries.all fun (e : IntensifierEntry) => match e.fragmentEntry with | some a => a.scaleType == Core.Order.Boundedness.open_ | none => false) = true

All intensifier bases have open scales (§2.1, fn. 3: "I will restrict my attention to adjectives with open-ended scales"). Derived from the Fragment. Decent also derives an open .value scale: its necessity standard ([KMcN05]) is a standardOverride, not scale boundedness, so it no longer needs the exception the earlier lower-bounded modeling required.

theorem Nouwen2024.Intensifiers.bleached_implies_negative : ((List.filter (fun (x : IntensifierEntry) => x.bleached) allEntries).all fun (x : IntensifierEntry) => x.valence == Features.EvaluativeValence.negative) = true

All bleached intensifiers have negative evaluative bases (§2.2–2.3). Bleaching is a diachronic process: the negative evaluative content ("it is horrible that...") is lost, leaving only the degree function (extremity). This historical process systematically targeted negative evaluatives, not positive ones. Derived from the data.

theorem Nouwen2024.Intensifiers.zwicky_evaluative_both_attested : ((List.filter (fun (x : IntensifierEntry) => x.baseKind == BaseKind.evaluative) allEntries).all fun (x : IntensifierEntry) => x.attested) = true

Zwicky's restriction does NOT extend to evaluatives (§2.5, (28)–(30)): "The weather was pleasantly / unpleasantly warm." Both positive and negative evaluative intensifiers are attested.

theorem Nouwen2024.Intensifiers.evaluative_has_both_polarities : (List.filter (fun (e : IntensifierEntry) => e.baseKind == BaseKind.evaluative && e.valence == Features.EvaluativeValence.positive) allEntries).length > 0 ∧ (List.filter (fun (e : IntensifierEntry) => e.baseKind == BaseKind.evaluative && e.valence == Features.EvaluativeValence.negative) allEntries).length > 0

Evaluative intensifiers come in both positive and negative valence. (Contrast with modals, where only deviation-denoting bases intensify.)

theorem Nouwen2024.Intensifiers.goldilocks_universal : allEntries.all goldilocksHolds = true

The Goldilocks effect holds universally across all entries (including exceptions, which are handled by the goldilocksException flag).

theorem Nouwen2024.Intensifiers.zwicky_universal : allEntries.all zwickyHolds = true

Zwicky's generalization holds for all modal/mirative entries.

theorem Nouwen2024.Intensifiers.goldilocks_exceptions_are_positive_H : ((List.filter (fun (x : IntensifierEntry) => x.goldilocksException) allEntries).all fun (e : IntensifierEntry) => e.valence == Features.EvaluativeValence.positive && e.class_ == IntensifierClass.H) = true

Goldilocks exceptions are all positive-evaluative H-degree adverbs. They represent extreme positive evaluation (remarkable, stunning) where the extremity of the evaluation, rather than its polarity, determines the degree class.

theorem Nouwen2024.Intensifiers.antonym_pairs_resolve : (allEntries.all fun (e : IntensifierEntry) => match e.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjective) => x.antonymForm with | some ant => (English.Predicates.Adjectival.lookup ant).isSome | none => true) = true

Antonym consistency: every intensifier entry whose Fragment base has an antonym can also look up that antonym in the Fragment.

instance RSA.Nouwen2024.instNeZeroNatOfNat_linglib : NeZero 6

@[reducible, inline]

abbrev RSA.Nouwen2024.Height : Type

Equations

• RSA.Nouwen2024.Height = Degree.Degree 6

@[reducible, inline]

abbrev RSA.Nouwen2024.Threshold : Type

Equations

• RSA.Nouwen2024.Threshold = Degree.Threshold 6

def RSA.Nouwen2024.tallMeaning (θ : Threshold) (h : Height) : Bool

⟦tall⟧(θ)(x) = 1 iff height(x) > θ, specialized to scale 6.

Equations

• RSA.Nouwen2024.tallMeaning θ h = decide (Degree.positiveMeaning h θ)

def RSA.Nouwen2024.heightPrior (h : Height) : ℚ

Height prior: discretized bell curve centered at h3 (norm for scale 6). Weights: [1, 5, 10, 20, 10, 5, 1] (sum = 52).

Equations

• RSA.Nouwen2024.heightPrior h = match Degree.Degree.toNat h with | 0 => 1 | 1 => 5 | 2 => 10 | 3 => 20 | 4 => 10 | 5 => 5 | x => 1

inductive RSA.Nouwen2024.Utterance : Type

Utterances about warmth with optional deadjectival intensifier.

The utterance set extends bare "warm" with intensified variants.

• bare_warm : Utterance
• horribly_warm : Utterance
• pleasantly_warm : Utterance
• silent : Utterance

def RSA.Nouwen2024.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RSA.Nouwen2024.instReprUtterance : Repr Utterance

Equations

• RSA.Nouwen2024.instReprUtterance = { reprPrec := RSA.Nouwen2024.instReprUtterance.repr }

@[implicit_reducible]

instance RSA.Nouwen2024.instDecidableEqUtterance : DecidableEq Utterance

Equations

• RSA.Nouwen2024.instDecidableEqUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RSA.Nouwen2024.instFintypeUtterance : Fintype Utterance

Equations

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

def RSA.Nouwen2024.allUtterances : List Utterance

Equations

• RSA.Nouwen2024.allUtterances = [RSA.Nouwen2024.Utterance.bare_warm, RSA.Nouwen2024.Utterance.horribly_warm, RSA.Nouwen2024.Utterance.pleasantly_warm, RSA.Nouwen2024.Utterance.silent]

def RSA.Nouwen2024.muHorrible (h : Height) : ℕ

Evaluative measure for "horrible" applied to the Height domain.

μ_horrible(h) = |h - norm|

Heights far from the norm (3) are evaluated as more "horrible". Agrees with Intensification.muHorrible 6 (see meaning_grounded_horribly).

Equations

• RSA.Nouwen2024.muHorrible h = if Degree.Degree.toNat h ≥ 3 then Degree.Degree.toNat h - 3 else 3 - Degree.Degree.toNat h

def RSA.Nouwen2024.muPleasant (h : Height) : ℕ

Evaluative measure for "pleasant" applied to the Height domain.

μ_pleasant(h) = norm - |h - norm|

Heights near the norm (3) are evaluated as more "pleasant". Agrees with Intensification.muPleasant 6 (see meaning_grounded_pleasantly).

Equations

• RSA.Nouwen2024.muPleasant h = if Degree.Degree.toNat h ≥ 3 then 6 - Degree.Degree.toNat h else Degree.Degree.toNat h

def RSA.Nouwen2024.meaning (u : Utterance) (h : Height) (θ θ_e : Threshold) : Bool

Full meaning function.

• bare_warm: h > θ (standard [LG17])
• horribly_warm: (h > θ) ∧ (μ_horrible(h) > θ_e)
• pleasantly_warm: (h > θ) ∧ (μ_pleasant(h) > θ_e)
• silent: always true

Equations

• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.bare_warm h θ θ_e = RSA.Nouwen2024.tallMeaning θ h
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.horribly_warm h θ θ_e = (RSA.Nouwen2024.tallMeaning θ h && decide (RSA.Nouwen2024.muHorrible h > Degree.Threshold.toNat θ_e))
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.pleasantly_warm h θ θ_e = (RSA.Nouwen2024.tallMeaning θ h && decide (RSA.Nouwen2024.muPleasant h > Degree.Threshold.toNat θ_e))
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.silent h θ θ_e = true

theorem RSA.Nouwen2024.meaning_grounded_horribly (h : Height) (θ θ_e : Threshold) : meaning Utterance.horribly_warm h θ θ_e = true ↔ Semantics.Gradability.Intensification.intensifiedMeaning (Semantics.Gradability.Intensification.muHorrible 6) h θ θ_e

The local horribly_warm meaning agrees with theory-layer intensifiedMeaning for all inputs. This bridges the ℕ-valued local measures to the ℚ-valued theory-layer Intensification.muHorrible.

theorem RSA.Nouwen2024.meaning_grounded_pleasantly (h : Height) (θ θ_e : Threshold) : meaning Utterance.pleasantly_warm h θ θ_e = true ↔ Semantics.Gradability.Intensification.intensifiedMeaning (Semantics.Gradability.Intensification.muPleasant 6) h θ θ_e

The local pleasantly_warm meaning agrees with theory-layer intensifiedMeaning for all inputs. This bridges the ℕ-valued local measures to the ℚ-valued theory-layer Intensification.muPleasant.

The Goldilocks effect as a set-theoretic fact

[Nou24] p. 21: "horribly warm will end up being compatible only with the higher degrees in this range. Note that extremely low temperatures are also horrible, but they are not in the interval [d, d′], because we arrived at that interval using the positive form of the adjective." The paper calls Goldilocks "merely a tendency" (p. 9; fn. 14 notes the expressive-taboo exception). On this scale the tendency has an exact boundary — θ + θ_e ≥ 2 (horriblyWarm_upperClosed_iff): below it the intensified meaning leaks into the cold tail, which is precisely the Wheeler problem of the paper's Fig. 5 (wheeler_cold_leak).

def RSA.Nouwen2024.UpwardClosedWithin (S B : Height → Bool) : Prop

S is upward closed within B: any B-world at least as high as some S-world is itself in S.

Equations

• RSA.Nouwen2024.UpwardClosedWithin S B = ∀ (h h' : RSA.Nouwen2024.Height), S h = true → B h' = true → Degree.Degree.toNat h ≤ Degree.Degree.toNat h' → S h' = true

@[implicit_reducible]

instance RSA.Nouwen2024.instDecidableUpwardClosedWithin (S B : Height → Bool) : Decidable (UpwardClosedWithin S B)

Equations

• RSA.Nouwen2024.instDecidableUpwardClosedWithin S B = id inferInstance

theorem RSA.Nouwen2024.horriblyWarm_upperClosed_iff (θ θ_e : Threshold) : (UpwardClosedWithin (fun (h : Height) => meaning Utterance.horribly_warm h θ θ_e) fun (h : Height) => meaning Utterance.bare_warm h θ θ_e) ↔ 2 ≤ Degree.Threshold.toNat θ + Degree.Threshold.toNat θ_e

Goldilocks, exactly: horribly warm is an upper set within warm iff the adjectival and evaluative thresholds jointly reach the norm − 1 boundary (θ + θ_e ≥ 2 on the Degree-6 scale, norm = 3). The U-shaped μ_horrible targets both scale extremes, but the positive form of warm has already cut off the cold end whenever the thresholds are high enough.

theorem RSA.Nouwen2024.pleasantlyWarm_never_upperClosed (θ θ_e : Threshold) (hne : ∃ (h : Height), meaning Utterance.pleasantly_warm h θ θ_e = true) : ¬UpwardClosedWithin (fun (h : Height) => meaning Utterance.pleasantly_warm h θ θ_e) fun (h : Height) => meaning Utterance.bare_warm h θ θ_e

Positive evaluations are "reserved for the middle of a scale" ([Nou24] p. 21): whenever pleasantly warm is satisfiable at all, it is never an upper set within warm — the mid-peaked μ_pleasant cannot produce upper-tail intensification. (The nonemptiness guard excludes the vacuous θ_e ≥ 3 cases, where no height is pleasant enough.)

theorem RSA.Nouwen2024.wheeler_cold_leak : ∃ (θ : Threshold) (θ_e : Threshold) (h : Height), Degree.Degree.toNat h < 3 ∧ meaning Utterance.horribly_warm h θ θ_e = true

The Wheeler leak ([Nou24] Fig. 5, p. 27: "horribly warm is not (entirely) incompatible with things being horribly cold"): below the Goldilocks boundary, horribly warm is true at cold heights. This is the semantic root of the problem the paper's backgrounded (sequential) update is designed to mitigate.

Licensing support: the proof engine for the pragmatic shifts

The latent pairs licensing an utterance at a world form the rectangle [0, h) × [0, μ(h)), so support inclusion is componentwise dominance in the two measures: higher-and-more-extreme worlds license strictly more latents — the structural mechanism behind upward intensification (the pragmatic listener sums over licensed latents).

def RSA.Nouwen2024.licensingSet (u : Utterance) (h : Height) : Finset (Threshold × Threshold)

The latent threshold pairs at which u is true at h.

Equations

• RSA.Nouwen2024.licensingSet u h = {l : RSA.Nouwen2024.Threshold × RSA.Nouwen2024.Threshold | RSA.Nouwen2024.meaning u h l.1 l.2 = true}

theorem RSA.Nouwen2024.licensingSet_horribly_mono {w₂ w₁ : Height} (hw : Degree.Degree.toNat w₂ ≤ Degree.Degree.toNat w₁) (hμ : muHorrible w₂ ≤ muHorrible w₁) : licensingSet Utterance.horribly_warm w₂ ⊆ licensingSet Utterance.horribly_warm w₁

Componentwise measure dominance yields licensing-support inclusion: if w₁ is at least as high and at least as extreme as w₂, every latent licensing horribly warm at w₂ licenses it at w₁.

theorem RSA.Nouwen2024.licensingSet_deg2_ssubset_deg5 : licensingSet Utterance.horribly_warm (Degree.deg 2 ⋯) ⊂ licensingSet Utterance.horribly_warm (Degree.deg 5 ⋯)

The file's key comparison pair has strict support inclusion: the extreme height deg 5 licenses strictly more latents than the moderate deg 2.

theorem RSA.Nouwen2024.licensingSet_not_totalOrder : ¬licensingSet Utterance.horribly_warm (Degree.deg 1 ⋯) ⊆ licensingSet Utterance.horribly_warm (Degree.deg 2 ⋯) ∧ ¬licensingSet Utterance.horribly_warm (Degree.deg 2 ⋯) ⊆ licensingSet Utterance.horribly_warm (Degree.deg 1 ⋯)

Licensing support is not totally ordered: below the norm, lower heights are warmer-false but more extreme, so their supports are incomparable — the inclusion order is exactly componentwise dominance, not a chain.

def RSA.Nouwen2024.muUsual : Semantics.Gradability.Intensification.EvaluativeMeasure 6

Constant evaluative measure (no evaluative content).

Models adverbs like "*usually" — a constant measure provides no discriminating information about degree, which is why "*usually warm" is vacuous (Zwicky's generalization).

Equations

• RSA.Nouwen2024.muUsual = { form := "usual", valence := Features.EvaluativeValence.neutral, mu := fun (x : ℕ) => 3 }

theorem RSA.Nouwen2024.usual_constant (h₁ h₂ : Height) : muUsual.mu (Degree.Degree.toNat h₁) = muUsual.mu (Degree.Degree.toNat h₂)

A constant evaluative measure provides no information: for any two heights, the measure value is identical.

def RSA.Nouwen2024.utteranceCost : Utterance → ℚ

Intensified utterances are costlier than bare utterances.

assumes that "horribly warm" has higher production cost than "warm" because it contains more morphological material. This cost differential drives the pragmatic reasoning.

Equations

• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.bare_warm = 1
• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.horribly_warm = 2
• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.pleasantly_warm = 2
• RSA.Nouwen2024.utteranceCost RSA.Nouwen2024.Utterance.silent = 0

Sequential Dual-Threshold Model — types

[Nou24]'s key innovation: the evaluative adverb and base adjective apply sequentially — the listener first updates on the evaluative measure, then applies the adjective threshold to the resulting posterior (eqs. 50–51). The chain itself and its predictions live in the probabilistic-model sections below; this section provides the stage utterance types, meanings, and costs they consume.

inductive RSA.Nouwen2024.EvalUtterance : Type

Utterances for the evaluative step: either the evaluative positive form ("the degree is horribly/pleasantly X") or silence.

• eval_pos : EvalUtterance
• silent : EvalUtterance

@[implicit_reducible]

instance RSA.Nouwen2024.instReprEvalUtterance : Repr EvalUtterance

Equations

• RSA.Nouwen2024.instReprEvalUtterance = { reprPrec := RSA.Nouwen2024.instReprEvalUtterance.repr }

def RSA.Nouwen2024.instReprEvalUtterance.repr : EvalUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RSA.Nouwen2024.instDecidableEqEvalUtterance : DecidableEq EvalUtterance

Equations

• RSA.Nouwen2024.instDecidableEqEvalUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RSA.Nouwen2024.instFintypeEvalUtterance : Fintype EvalUtterance

Equations

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

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

Evaluative meaning for step 1. The evaluative positive form checks only μ_eval(h) > θ_e, without the base adjective. This is the decomposed evaluative component.

Equations

• RSA.Nouwen2024.evalMeaning evalMu RSA.Nouwen2024.EvalUtterance.eval_pos h θ_e = decide (evalMu h > Degree.Threshold.toNat θ_e)
• RSA.Nouwen2024.evalMeaning evalMu RSA.Nouwen2024.EvalUtterance.silent h θ_e = true

def RSA.Nouwen2024.evalCost : EvalUtterance → ℚ

Evaluative step cost: the evaluative adverb costs 1, silence costs 0.

Equations

• RSA.Nouwen2024.evalCost RSA.Nouwen2024.EvalUtterance.eval_pos = 1
• RSA.Nouwen2024.evalCost RSA.Nouwen2024.EvalUtterance.silent = 0

inductive RSA.Nouwen2024.AdjUtterance : Type

Utterances for the adjective step.

• warm : AdjUtterance
• silent : AdjUtterance

@[implicit_reducible]

instance RSA.Nouwen2024.instReprAdjUtterance : Repr AdjUtterance

Equations

• RSA.Nouwen2024.instReprAdjUtterance = { reprPrec := RSA.Nouwen2024.instReprAdjUtterance.repr }

def RSA.Nouwen2024.instReprAdjUtterance.repr : AdjUtterance → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance RSA.Nouwen2024.instDecidableEqAdjUtterance : DecidableEq AdjUtterance

Equations

• RSA.Nouwen2024.instDecidableEqAdjUtterance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance RSA.Nouwen2024.instFintypeAdjUtterance : Fintype AdjUtterance

Equations

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

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

Adjective meaning for step 2: just the base positive form h > θ.

Equations

• RSA.Nouwen2024.adjMeaning RSA.Nouwen2024.AdjUtterance.warm h θ = RSA.Nouwen2024.tallMeaning θ h
• RSA.Nouwen2024.adjMeaning RSA.Nouwen2024.AdjUtterance.silent h θ = true

def RSA.Nouwen2024.adjCost : AdjUtterance → ℚ

Equations

• RSA.Nouwen2024.adjCost RSA.Nouwen2024.AdjUtterance.warm = 1
• RSA.Nouwen2024.adjCost RSA.Nouwen2024.AdjUtterance.silent = 0

The probabilistic model on mathlib PMF

[Nou24] [LG17]

[Nou24] ("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. The sections below formalise 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 [Nou24] 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 linear |h − norm|, NOT Nouwen's f(x) = x² quadratic. Nouwen's Figure 4(b) handcrafts f(x) = x²; the file's muHorrible = |h − 3| (deg 0 ↦ 3, deg 3 ↦ 0, deg 6 ↦ 3) is the linear-V simplification. Both are U-shaped — both extremes count as horrible, which is what the Wheeler leak (wheeler_cold_leak in the bundled file) and the Goldilocks boundary depend on — but slopes and hence fitted magnitudes differ. Paper (p. 31): the model is "a proof of concept"; the theorems here are shape-generic where possible.

Also captured (§5d–§5g):

• Zwicky's generalisation (paper §5): the constant measure's update is the identity (priorAfterEvalPosUsual_eq_prior), so "usually warm" collapses to bare "warm" (seqUsually_eq_bare), while μ_unusual = μ_horrible definitionally and the extreme-measure update strictly boosts the extreme above its prior (eval_unusual_boosts_extreme).
• Positive-valence half (Figure 8): seq_pleasantly_prefers_moderate — a support fact (μ_pleasant (deg 6) = 0 licenses no threshold).

Connection to LassiterGoodman2017PMF.lean

[Nou24] §4 explicitly adopts the [LG17] 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")

[Nou24] §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. 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

• seq_horribly_shifts_upward — PROVEN structurally (§5b ratio cancellation): the height factor cancels in each per-threshold speaker, collapsing the marginals to mass-monotone sums over the licensed thresholds; informativity (gval 1 > gval 0) beats the 2:1 prior ratio. No numeric reflection.
• eq_44b_factive_embedding_NOT_FORMALISED — Nouwen's novel contribution.
• eq_49_qud_partition_NOT_FORMALISED — explicit substrate gap.

Reused from the semantic layer above

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

§1. Height prior as a PMF

noncomputable def RSA.Nouwen2024.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.heightPriorENN h = ENNReal.ofReal ↑(RSA.Nouwen2024.heightPrior h)

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

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

noncomputable def RSA.Nouwen2024.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.heightPriorPMF = PMF.normalize RSA.Nouwen2024.heightPriorENN RSA.Nouwen2024.heightPriorPMF._proof_2 RSA.Nouwen2024.heightPriorPMF._proof_3

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

§2. ValidThreshold subtype + conversion

@[reducible, inline]

abbrev RSA.Nouwen2024.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.ValidThreshold = Fin 3

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

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

Equations

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

noncomputable def RSA.Nouwen2024.thresholdPriorPMF : PMF ValidThreshold

Uniform prior over ValidThreshold.

Equations

• RSA.Nouwen2024.thresholdPriorPMF = PMF.uniformOfFintype RSA.Nouwen2024.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.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.evalLex evalMu θ u h = RSA.Nouwen2024.evalMeaning evalMu u h θ

theorem RSA.Nouwen2024.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.evalL0_horribleAt (vt : ValidThreshold) : EvalUtterance → PMF Height

Stage 1 literal listener under muHorrible at valid threshold vt.

Equations

• RSA.Nouwen2024.evalL0_horribleAt vt u = RSA.L0LassiterGoodman RSA.Nouwen2024.heightPriorPMF (RSA.Nouwen2024.evalLex RSA.Nouwen2024.muHorrible (RSA.Nouwen2024.validToThreshold vt)) u ⋯

noncomputable def RSA.Nouwen2024.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.evalCostFactor u = ENNReal.ofReal (Real.exp (-4 * ↑(RSA.Nouwen2024.evalCost u)))

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

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

noncomputable def RSA.Nouwen2024.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.evalSpeaker_horribleAt vt w = RSA.S1Belief (RSA.Nouwen2024.evalL0_horribleAt vt) RSA.Nouwen2024.evalCostFactor 4 w ⋯ ⋯

noncomputable def RSA.Nouwen2024.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.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.evalL1Horrible u = PMF.posterior RSA.Nouwen2024.evalSpeakerMarginalHorrible RSA.Nouwen2024.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.priorAfterEvalPos : PMF Height

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

Equations

• RSA.Nouwen2024.priorAfterEvalPos = RSA.Nouwen2024.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.adjLex (θ : Threshold) (u : AdjUtterance) (h : Height) : Bool

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

Equations

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

theorem RSA.Nouwen2024.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.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.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.adjL0_warmAt vt u = RSA.L0LassiterGoodman RSA.Nouwen2024.priorAfterEvalPos (RSA.Nouwen2024.adjLex (RSA.Nouwen2024.validToThreshold vt)) u ⋯

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

Equations

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

noncomputable def RSA.Nouwen2024.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.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.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.seqAdjL1HorriblyWarm u = PMF.posterior RSA.Nouwen2024.adjSpeakerMarginal RSA.Nouwen2024.priorAfterEvalPos u ⋯

§5b. Ratio cancellation: the structural core

Because the L&G literal listener carries the prior multiplicatively (L0(u) h = P h · 1[u true at h] / mass(u)), the height factor P h cancels in the speaker's normalisation: on its support, each per-threshold speaker value depends only on the prior MASS of the utterance's extension at that threshold. Each marginalised speaker is therefore a sum of a mass-monotone value over the licensed thresholds, and the headline product comparison follows from mass monotonicity alone — no numeric reflection.

noncomputable def RSA.Nouwen2024.evalMass (vt : ValidThreshold) : ENNReal

Prior mass of the .eval_pos extension at threshold vt (exactly the L0LassiterGoodman normaliser for stage 1).

Equations

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

theorem RSA.Nouwen2024.evalMass_ne_zero (vt : ValidThreshold) : evalMass vt ≠ 0

theorem RSA.Nouwen2024.evalMass_ne_top (vt : ValidThreshold) : evalMass vt ≠ ⊤

noncomputable def RSA.Nouwen2024.adjMass (vt : ValidThreshold) : ENNReal

Π-mass of the .warm extension at threshold vt (the stage-2 L0LassiterGoodman normaliser, against the backgrounded prior).

Equations

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

theorem RSA.Nouwen2024.adjMass_ne_zero (vt : ValidThreshold) : adjMass vt ≠ 0

theorem RSA.Nouwen2024.adjMass_ne_top (vt : ValidThreshold) : adjMass vt ≠ ⊤

noncomputable def RSA.Nouwen2024.gval (vt : ValidThreshold) : ENNReal

Stage-1 speaker value at .eval_pos on its support: a function of the extension mass only (the height factor has cancelled).

Equations

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

noncomputable def RSA.Nouwen2024.fval (vt : ValidThreshold) : ENNReal

Stage-2 speaker value at .warm on its support.

Equations

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

theorem RSA.Nouwen2024.evalCostFactor_silent : evalCostFactor EvalUtterance.silent = 1

theorem RSA.Nouwen2024.adjCostFactor_silent : adjCostFactor AdjUtterance.silent = 1

theorem RSA.Nouwen2024.evalSpeaker_apply_of_true (vt : ValidThreshold) (w : Height) (hw : evalLex muHorrible (validToThreshold vt) EvalUtterance.eval_pos w = true) : (evalSpeaker_horribleAt vt w) EvalUtterance.eval_pos = gval vt

Ratio cancellation, stage 1: on its support the eval speaker's value is gval vt — independent of the height.

theorem RSA.Nouwen2024.evalSpeaker_apply_of_false (vt : ValidThreshold) (w : Height) (hw : evalLex muHorrible (validToThreshold vt) EvalUtterance.eval_pos w = false) : (evalSpeaker_horribleAt vt w) EvalUtterance.eval_pos = 0

Ratio cancellation, stage 1, off support: value 0.

theorem RSA.Nouwen2024.adjSpeaker_apply_of_true (vt : ValidThreshold) (w : Height) (hw : adjLex (validToThreshold vt) AdjUtterance.warm w = true) (hPi : priorAfterEvalPos w ≠ 0) : (adjSpeaker_warmAt vt w) AdjUtterance.warm = fval vt

Ratio cancellation, stage 2: on its support (and at a non-degenerate world, Π(w) ≠ 0) the adjective speaker's value is fval vt.

theorem RSA.Nouwen2024.adjSpeaker_apply_of_false (vt : ValidThreshold) (w : Height) (hw : adjLex (validToThreshold vt) AdjUtterance.warm w = false) (hPi : priorAfterEvalPos w ≠ 0) : (adjSpeaker_warmAt vt w) AdjUtterance.warm = 0

Stage-2 speaker value off support (at a non-degenerate world): 0.

Mass monotonicity — structural, no value computation

The .eval_pos extension shrinks strictly from threshold 0 to threshold 1 (deg 2 has μ_horrible = 1, licensed at 0 but not at 1), so the eval mass drops strictly; the speaker value gval rises strictly (informativity).

theorem RSA.Nouwen2024.evalMass_one_lt_zero : evalMass 1 < evalMass 0

theorem RSA.Nouwen2024.gval_zero_lt_one : gval 0 < gval 1

Informativity is threshold-monotone at the eval stage: the strictly smaller mass at threshold 1 yields a strictly larger speaker value.

Marginal expansions over the licensed thresholds

theorem RSA.Nouwen2024.gval_ne_top (vt : ValidThreshold) : gval vt ≠ ⊤

theorem RSA.Nouwen2024.fval_ne_top (vt : ValidThreshold) : fval vt ≠ ⊤

theorem RSA.Nouwen2024.fval_ne_zero (vt : ValidThreshold) : fval vt ≠ 0

theorem RSA.Nouwen2024.heightPriorPMF_deg2_eq : heightPriorPMF (Degree.deg 2 ⋯) = 2 * heightPriorPMF (Degree.deg 5 ⋯)

The raw prior ratio P(deg 2) = 2 · P(deg 5) (weights 10 vs 5) — no normaliser computation needed.

theorem RSA.Nouwen2024.evalMarginal_deg2 : (evalSpeakerMarginalHorrible (Degree.deg 2 ⋯)) EvalUtterance.eval_pos = 3⁻¹ * gval 0

theorem RSA.Nouwen2024.evalMarginal_deg5 : (evalSpeakerMarginalHorrible (Degree.deg 5 ⋯)) EvalUtterance.eval_pos = 3⁻¹ * gval 0 + 3⁻¹ * gval 1

theorem RSA.Nouwen2024.adjMarginal_deg2 : (adjSpeakerMarginal (Degree.deg 2 ⋯)) AdjUtterance.warm = 3⁻¹ * fval 0 + 3⁻¹ * fval 1

theorem RSA.Nouwen2024.adjMarginal_deg5 : (adjSpeakerMarginal (Degree.deg 5 ⋯)) AdjUtterance.warm = 3⁻¹ * fval 0 + 3⁻¹ * fval 1 + 3⁻¹ * fval 2

§5c. The backgrounding contrast: why the paper rejects (49)

[Nou24] p. 28: "the source of this problem lies in the simple conjunctive analysis I assume in (49)… the two thresholds are resolved in tandem… all we need to do is update the two positive forms successively rather than simultaneously." Made structural: in the REJECTED simultaneous model, per-latent dominance FAILS on the shared licensing support — at a shared latent where every utterance is true at both worlds, ratio cancellation makes the speaker values exactly equal, so the raw height prior's 2:1 preference for the moderate world wins the term comparison (sim_sharedSupport_dominance_fails). In the final sequential model the same per-latent comparison HOLDS (seq_horribly_shifts_upward's §5b engine): the backgrounded evaluative posterior has already re-loaded the prior toward the extremes. Backgrounding is exactly what makes intensification term-by-term derivable.

noncomputable def RSA.Nouwen2024.simCostFactor (u : Utterance) : ENNReal

Cost factor for the simultaneous model's four utterances.

Equations

• RSA.Nouwen2024.simCostFactor u = ENNReal.ofReal (Real.exp (-4 * ↑(RSA.Nouwen2024.utteranceCost u)))

theorem RSA.Nouwen2024.simCostFactor_pos (u : Utterance) : simCostFactor u ≠ 0

theorem RSA.Nouwen2024.simCostFactor_finite (u : Utterance) : simCostFactor u ≠ ⊤

noncomputable def RSA.Nouwen2024.simL0At (l : Threshold × Threshold) (u : Utterance) : PMF Height

Simultaneous-model literal listener at latent (θ, θ_e), gated on the utterance's extension being nonempty (the four-utterance L&G L0).

Equations

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

noncomputable def RSA.Nouwen2024.simSpeakerAt (l : Threshold × Threshold) (h : Height) : PMF Utterance

Simultaneous-model speaker at latent (θ, θ_e) and world h (total, with the vacuous fallback at degenerate cells, as in adjSpeaker_warmAt).

Equations

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

noncomputable def RSA.Nouwen2024.simTerm (l : Threshold × Threshold) (h : Height) : ENNReal

Per-latent joint term of the simultaneous model for "horribly warm": prior × speaker — one latent cell's contribution to the (49)-listener's world score.

Equations

• RSA.Nouwen2024.simTerm l h = RSA.Nouwen2024.heightPriorPMF h * (RSA.Nouwen2024.simSpeakerAt l h) RSA.Nouwen2024.Utterance.horribly_warm

noncomputable def RSA.Nouwen2024.simMass (l : Threshold × Threshold) (u : Utterance) : ENNReal

Extension mass of utterance u at latent l (the simL0At normaliser).

Equations

• RSA.Nouwen2024.simMass l u = ∑' (h : RSA.Nouwen2024.Height), RSA.Nouwen2024.heightPriorPMF h * if RSA.Nouwen2024.meaning u h l.1 l.2 = true then 1 else 0

theorem RSA.Nouwen2024.sim_sharedSupport_dominance_fails : ¬∀ l ∈ licensingSet Utterance.horribly_warm (Degree.deg 2 ⋯), simTerm l (Degree.deg 2 ⋯) ≤ simTerm l (Degree.deg 5 ⋯)

The failure half of the backgrounding contrast ([Nou24] p. 28: in (49) "the two thresholds are resolved in tandem"): in the rejected simultaneous model, per-latent dominance fails on the shared licensing support. At the shared latent (θ, θ_e) = (1, 0) every utterance is true at both deg 2 and deg 5, so ratio cancellation makes the speaker values exactly equal — and the raw height prior's 2:1 preference for the moderate world decides the term comparison. Contrast the sequential model (seq_horribly_shifts_upward): after backgrounding, the same per-latent comparisons run against the evaluative posterior, which has already re-loaded the prior toward the extremes. Backgrounding, not parameter tuning, is what makes intensification term-by-term derivable.

§5d. Measure-generic evaluative stage; the pleasantly chain

The horrible chain (§3–§5) instantiates the architecture with measure-specific definitions; the dite-total generic forms below serve the remaining measures (μ_pleasant here, μ_usual for the Zwicky section) without threading extension-positivity hypotheses.

noncomputable def RSA.Nouwen2024.evalL0At (evalMu : Height → ℕ) (vt : ValidThreshold) (u : EvalUtterance) : PMF Height

Measure-generic stage-1 literal listener (dite-total).

Equations

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

noncomputable def RSA.Nouwen2024.evalSpeakerAt (evalMu : Height → ℕ) (vt : ValidThreshold) (w : Height) : PMF EvalUtterance

Measure-generic stage-1 speaker (dite-total).

Equations

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

noncomputable def RSA.Nouwen2024.evalMarginalAt (evalMu : Height → ℕ) : Height → PMF EvalUtterance

Measure-generic marginalized stage-1 speaker.

Equations

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

theorem RSA.Nouwen2024.evalL0At_silent (evalMu : Height → ℕ) (vt : ValidThreshold) (w : Height) : (evalL0At evalMu vt EvalUtterance.silent) w = heightPriorPMF w

theorem RSA.Nouwen2024.evalSpeakerAt_apply_of_false (evalMu : Height → ℕ) (vt : ValidThreshold) (w : Height) (hne : (∑' (h : Height), heightPriorPMF h * if evalLex evalMu (validToThreshold vt) EvalUtterance.eval_pos h = true then 1 else 0) ≠ 0) (hw : evalLex evalMu (validToThreshold vt) EvalUtterance.eval_pos w = false) : (evalSpeakerAt evalMu vt w) EvalUtterance.eval_pos = 0

Generic off-support zero (given a nonempty .eval_pos extension).

theorem RSA.Nouwen2024.evalSpeakerAt_apply_ne_zero_of_true (evalMu : Height → ℕ) (vt : ValidThreshold) (w : Height) (hne : (∑' (h : Height), heightPriorPMF h * if evalLex evalMu (validToThreshold vt) EvalUtterance.eval_pos h = true then 1 else 0) ≠ 0) (hw : evalLex evalMu (validToThreshold vt) EvalUtterance.eval_pos w = true) : (evalSpeakerAt evalMu vt w) EvalUtterance.eval_pos ≠ 0

Generic on-support positivity (given a nonempty .eval_pos extension).

theorem RSA.Nouwen2024.evalMass_pleasant_ne_zero (vt : ValidThreshold) : (∑' (h : Height), heightPriorPMF h * if evalLex muPleasant (validToThreshold vt) EvalUtterance.eval_pos h = true then 1 else 0) ≠ 0

Nonempty .eval_pos extension for μ_pleasant at every valid threshold (witness deg 3, where μ_pleasant = 3).

noncomputable def RSA.Nouwen2024.priorAfterEvalPosPleasant : PMF Height

Backgrounded prior for "pleasantly": stage-1 posterior under μ_pleasant.

Equations

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

theorem RSA.Nouwen2024.priorAfterEvalPosPleasant_pos_at {h : Height} (hpos : 0 < muPleasant h) : priorAfterEvalPosPleasant h ≠ 0

Π_pleasant is positive at heights with positive μ_pleasant.

noncomputable def RSA.Nouwen2024.adjL0PleasantAt (vt : ValidThreshold) (u : AdjUtterance) : PMF Height

Stage-2 literal listener for the pleasantly chain (dite-total, prior Π_pleasant).

Equations

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

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

Stage-2 speaker for the pleasantly chain (dite-total).

Equations

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

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

Marginalized stage-2 speaker for the pleasantly chain.

Equations

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

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

Sequential L1 for "pleasantly warm" (mirrors seqAdjL1HorriblyWarm).

Equations

• RSA.Nouwen2024.seqAdjL1PleasantlyWarm u = PMF.posterior RSA.Nouwen2024.adjMarginalPleasant RSA.Nouwen2024.priorAfterEvalPosPleasant u ⋯

theorem RSA.Nouwen2024.seq_pleasantly_prefers_moderate : (seqAdjL1PleasantlyWarm AdjUtterance.warm) (Degree.deg 4 ⋯) > (seqAdjL1PleasantlyWarm AdjUtterance.warm) (Degree.deg 6 ⋯)

"Pleasantly warm" prefers the moderate deg 4 over the extreme deg 6 ([Nou24] Fig. 8: positive evaluations concentrate mass mid-scale). The proof is a support fact: μ_pleasant (deg 6) = 0 licenses no evaluative threshold, so the extreme world's evaluative marginal — hence its whole chained score — is zero, while the moderate world's is positive.

§5e. Zwicky vacuity as an identity; the usually chain

[Nou24] p. 22: the simple account "wrongly predict[s] that usually tall means the same as tall but not unusually tall". Model-side content: a constant evaluative measure licenses every threshold at every height, so the evaluative update is the IDENTITY (priorAfterEvalPosUsual_eq_prior) — "usually warm" reduces to bare "warm" exactly — while μ_unusual = μ_horrible holds definitionally, so "unusually warm" IS the horribly chain and inherits its upward shift. The old cross-model inequality pair is subsumed by these identities plus the single-model shift theorems.

def RSA.Nouwen2024.muUsualN : Height → ℕ

ℕ-valued constant measure ("usual"): no height discrimination.

Equations

• RSA.Nouwen2024.muUsualN x✝ = 3

def RSA.Nouwen2024.muUnusualN : Height → ℕ

μ_unusual has μ_horrible's shape: deviation measures pattern with negative evaluatives ([Nou24] §5).

Equations

• RSA.Nouwen2024.muUnusualN = RSA.Nouwen2024.muHorrible

theorem RSA.Nouwen2024.muUnusualN_eq_muHorrible : muUnusualN = muHorrible

theorem RSA.Nouwen2024.evalL0At_usual (vt : ValidThreshold) (u : EvalUtterance) (w : Height) : (evalL0At muUsualN vt u) w = heightPriorPMF w

The constant-measure literal listener is the prior at every utterance.

theorem RSA.Nouwen2024.evalSpeakerAt_usual_apply (vt : ValidThreshold) (w : Height) : (evalSpeakerAt muUsualN vt w) EvalUtterance.eval_pos = evalCostFactor EvalUtterance.eval_pos / (evalCostFactor EvalUtterance.eval_pos + 1)

Constant-measure speaker value: closed form, height-independent.

theorem RSA.Nouwen2024.evalMarginalAt_usual_const (w : Height) : (evalMarginalAt muUsualN w) EvalUtterance.eval_pos = evalCostFactor EvalUtterance.eval_pos / (evalCostFactor EvalUtterance.eval_pos + 1)

The marginalised constant-measure kernel is constant across heights.

noncomputable def RSA.Nouwen2024.priorAfterEvalPosUsual : PMF Height

Backgrounded prior for "usually".

Equations

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

theorem RSA.Nouwen2024.priorAfterEvalPosUsual_eq_prior : priorAfterEvalPosUsual = heightPriorPMF

Zwicky's vacuity as an identity: the constant measure's evaluative update is the identity — Π_usual IS the prior. This is the deep form of the old eval_constant_preserves_peak (whose inequality is now a corollary of the prior's own shape) and the first half of "usually warm ≈ warm".

theorem RSA.Nouwen2024.eval_constant_preserves_peak : priorAfterEvalPosUsual (Degree.deg 3 ⋯) > priorAfterEvalPosUsual (Degree.deg 6 ⋯)

The old eval_constant_preserves_peak, now a prior fact: the constant measure's stage-1 posterior at the norm exceeds it at the extreme because the prior does (20 : 1 weights) — the evaluative step contributed nothing.

§5f. Prior-generic adjective stage; the bare and usually chains

noncomputable def RSA.Nouwen2024.adjL0WithPrior (Pi : PMF Height) (vt : ValidThreshold) (u : AdjUtterance) : PMF Height

Prior-generic stage-2 literal listener (dite-total).

Equations

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

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

Prior-generic stage-2 speaker (dite-total).

Equations

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

noncomputable def RSA.Nouwen2024.adjMarginalWithPrior (Pi : PMF Height) : Height → PMF AdjUtterance

Prior-generic marginalized stage-2 speaker.

Equations

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

theorem RSA.Nouwen2024.adjL0WithPrior_silent (Pi : PMF Height) (vt : ValidThreshold) (w : Height) : (adjL0WithPrior Pi vt AdjUtterance.silent) w = Pi w

noncomputable def RSA.Nouwen2024.adjMassP (Pi : PMF Height) (vt : ValidThreshold) : ENNReal

Π-mass of the .warm extension at threshold vt.

Equations

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

noncomputable def RSA.Nouwen2024.fvalP (Pi : PMF Height) (vt : ValidThreshold) : ENNReal

Prior-generic stage-2 speaker value on support: mass form.

Equations

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

theorem RSA.Nouwen2024.adjSpeakerWithPrior_apply_of_true (Pi : PMF Height) (vt : ValidThreshold) (w : Height) (hw : adjLex (validToThreshold vt) AdjUtterance.warm w = true) (hPw : Pi w ≠ 0) : (adjSpeakerWithPrior Pi vt w) AdjUtterance.warm = fvalP Pi vt

Ratio cancellation, prior-generic stage 2: on support, at a non-degenerate world, the speaker's value is fvalP Pi vt — independent of the world.

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

Baseline chain: bare "warm" over the raw height prior.

Equations

• RSA.Nouwen2024.bareAdjL1 u = PMF.posterior (RSA.Nouwen2024.adjMarginalWithPrior RSA.Nouwen2024.heightPriorPMF) RSA.Nouwen2024.heightPriorPMF u ⋯

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

The "usually warm" chain: stage 2 over the (identity) usual posterior.

Equations

• RSA.Nouwen2024.seqAdjL1Usually u = PMF.posterior (RSA.Nouwen2024.adjMarginalWithPrior RSA.Nouwen2024.priorAfterEvalPosUsual) RSA.Nouwen2024.priorAfterEvalPosUsual u ⋯

theorem RSA.Nouwen2024.seqUsually_eq_bare (u : AdjUtterance) : seqAdjL1Usually u = bareAdjL1 u

"Usually warm" IS bare "warm": the second half of Zwicky's vacuity — with the identity evaluative update (priorAfterEvalPosUsual_eq_prior), the whole sequential chain collapses to the baseline. Together with seq_unusually_shifts_extreme this subsumes the old cross-model discrimination pair without any cross-model numeric comparison.

theorem RSA.Nouwen2024.bare_warm_prefers_moderate : (bareAdjL1 AdjUtterance.warm) (Degree.deg 4 ⋯) > (bareAdjL1 AdjUtterance.warm) (Degree.deg 6 ⋯)

Bare "warm" prefers the moderate deg 4 over the extreme deg 6: both worlds license every valid threshold, so the marginalised speaker values coincide (ratio cancellation) and the raw prior (10 : 1) decides.

§5g. The posterior-boost fact

μ_unusual = μ_horrible holds by definition (muUnusualN_eq_muHorrible), so every "unusually" prediction is the corresponding horribly theorem verbatim; no duplicates are stated. The remaining content of the old cross-measure comparison is the posterior-vs-prior boost below.

theorem RSA.Nouwen2024.gval_ne_zero (vt : ValidThreshold) : gval vt ≠ 0

theorem RSA.Nouwen2024.evalMarginal_deg6 : (evalSpeakerMarginalHorrible (Degree.deg 6 ⋯)) EvalUtterance.eval_pos = 3⁻¹ * gval 0 + 3⁻¹ * gval 1 + 3⁻¹ * gval 2

theorem RSA.Nouwen2024.evalMarginal_deg3 : (evalSpeakerMarginalHorrible (Degree.deg 3 ⋯)) EvalUtterance.eval_pos = 0

theorem RSA.Nouwen2024.eval_unusual_boosts_extreme : priorAfterEvalPos (Degree.deg 6 ⋯) > heightPriorPMF (Degree.deg 6 ⋯)

The evaluative update boosts the extreme above its prior — the deep form of the old eval_unusual_boosts_extreme: the constant-measure update is the identity (priorAfterEvalPosUsual_eq_prior), so the old cross-measure comparison at deg 6 is posterior-vs-prior. Average argument: no height beats the extreme's marginal (evalMarginal_le_deg6) and the norm contributes zero (evalMarginal_deg3), so the normaliser sits strictly below the extreme's kernel value.

§6. Predictions

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.seq_horribly_shifts_upward : (seqAdjL1HorriblyWarm AdjUtterance.warm) (Degree.deg 5 ⋯) > (seqAdjL1HorriblyWarm AdjUtterance.warm) (Degree.deg 2 ⋯)

The headline shift prediction in PMF form: "horribly warm" pushes probability toward the high extreme (deg 5 over the moderate deg 2).

Fully structural discharge — no numeric reflection. The chained posterior κ₂ (posterior κ₁ μ b₁) b₂ shape decomposes via PMF.posterior_chained_lt_iff_score_lt to a product comparison μ(2)·E(2)·A(2) < μ(5)·E(5)·A(5); the ratio-cancellation lemmas (§5b) collapse each marginal to a sum of the mass-monotone speaker value over the licensed thresholds (E(h) = Σ_{θ_e < μ_H(h)} gval θ_e, A(h) = Σ_{θ < h} fval θ), and the raw prior ratio μ(2) = 2·μ(5) is beaten by informativity alone: gval 1 > gval 0 (strictly smaller extension mass at the higher threshold), so (g₀+g₁)(f₀+f₁+f₂) > 2·g₀·(f₀+f₁).

§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.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.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 (closed structurally via §5b) is the point: structural shell handles structural claims; the numeric core is reflection territory, regardless of bundling.

theorem RSA.Nouwen2024.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.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.