@cite{nouwen-2024} Deadjectival Intensifiers

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

"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 @cite{lassiter-goodman-2017} 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.

Two-Threshold Simultaneous Model

P_L1(h, θ, θ_e | u) ∝ P_S1(u | h, θ, θ_e) × P(h) × P(θ) × P(θ_e)

The listener jointly infers height h, adjective threshold θ, and evaluative threshold θ_e. The meaning function is an intersection:

• bare_warm: h > θ
• horribly_warm: (h > θ) ∧ (μ_horrible(h) > θ_e)
• pleasantly_warm: (h > θ) ∧ (μ_pleasant(h) > θ_e)
• silent: ⊤

Sequential Model (@cite{nouwen-2024}'s key innovation)

The evaluative adverb updates the prior before the adjective threshold applies: Step 1 infers P₁(h | "horribly"), Step 2 infers P₂(h | "warm") using P₁ as prior.

RSAConfig Mapping

• U = Utterance (bare_warm, horribly_warm, pleasantly_warm, silent)
• W = Height (Degree 6, 7 values: h0–h6)
• Latent = Threshold × Threshold (36 values: θ_adj × θ_eval)
• s1Score = beliefAction: exp(α · (log L0 − C(u)))
• α = 4 (matching @cite{lassiter-goodman-2017})
• C(bare) = 1, C(horribly/pleasantly) = 2, C(∅) = 0

Performance Note

Uses scale n=6 (7 heights, 6 thresholds) rather than the paper's continuous distribution or @cite{lassiter-goodman-2017}'s n=10, giving 4.4× fewer L0 cells in the simultaneous model (1008 vs 4400) and 2.6× fewer in the sequential model. All qualitative Goldilocks predictions are preserved.

inductive Phenomena.Gradability.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 Phenomena.Gradability.Intensifiers.instReprIntensifierClass : Repr IntensifierClass

Equations

• Phenomena.Gradability.Intensifiers.instReprIntensifierClass = { reprPrec := Phenomena.Gradability.Intensifiers.instReprIntensifierClass.repr }

def Phenomena.Gradability.Intensifiers.instReprIntensifierClass.repr : IntensifierClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gradability.Intensifiers.instDecidableEqIntensifierClass : DecidableEq IntensifierClass

Equations

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

inductive Phenomena.Gradability.Intensifiers.BaseKind : Type

Classification of adjectival base for deadjectival intensifiers (@cite{nouwen-2024} §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

def Phenomena.Gradability.Intensifiers.instReprBaseKind.repr : BaseKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gradability.Intensifiers.instReprBaseKind : Repr BaseKind

Equations

• Phenomena.Gradability.Intensifiers.instReprBaseKind = { reprPrec := Phenomena.Gradability.Intensifiers.instReprBaseKind.repr }

@[implicit_reducible]

instance Phenomena.Gradability.Intensifiers.instDecidableEqBaseKind : DecidableEq BaseKind

Equations

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

structure Phenomena.Gradability.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.

def Phenomena.Gradability.Intensifiers.instReprIntensifierEntry.repr : IntensifierEntry → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Gradability.Intensifiers.instReprIntensifierEntry : Repr IntensifierEntry

Equations

• Phenomena.Gradability.Intensifiers.instReprIntensifierEntry = { reprPrec := Phenomena.Gradability.Intensifiers.instReprIntensifierEntry.repr }

def Phenomena.Gradability.Intensifiers.horribly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.terribly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.awfully : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.dreadfully : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.frighteningly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.pleasantly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.nicely : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.decently : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.unusually : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.surprisingly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.impossibly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.remarkably : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.usually_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.expectedly_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.possibly_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.disgustingly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.annoyingly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.unpleasantly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.scarily : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.wonderfully : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.beautifully_ : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.delightfully : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.gorgeously : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.stunningly : IntensifierEntry

Equations

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

def Phenomena.Gradability.Intensifiers.allEntries : List IntensifierEntry

Equations

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

def Phenomena.Gradability.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 Phenomena.Gradability.Intensifiers.horribly_goldilocks : goldilocksHolds horribly = true

theorem Phenomena.Gradability.Intensifiers.terribly_goldilocks : goldilocksHolds terribly = true

theorem Phenomena.Gradability.Intensifiers.awfully_goldilocks : goldilocksHolds awfully = true

theorem Phenomena.Gradability.Intensifiers.dreadfully_goldilocks : goldilocksHolds dreadfully = true

theorem Phenomena.Gradability.Intensifiers.frighteningly_goldilocks : goldilocksHolds frighteningly = true

theorem Phenomena.Gradability.Intensifiers.disgustingly_goldilocks : goldilocksHolds disgustingly = true

theorem Phenomena.Gradability.Intensifiers.annoyingly_goldilocks : goldilocksHolds annoyingly = true

theorem Phenomena.Gradability.Intensifiers.unpleasantly_goldilocks : goldilocksHolds unpleasantly = true

theorem Phenomena.Gradability.Intensifiers.scarily_goldilocks : goldilocksHolds scarily = true

theorem Phenomena.Gradability.Intensifiers.pleasantly_goldilocks : goldilocksHolds pleasantly = true

theorem Phenomena.Gradability.Intensifiers.nicely_goldilocks : goldilocksHolds nicely = true

theorem Phenomena.Gradability.Intensifiers.decently_goldilocks : goldilocksHolds decently = true

theorem Phenomena.Gradability.Intensifiers.wonderfully_goldilocks : goldilocksHolds wonderfully = true

theorem Phenomena.Gradability.Intensifiers.beautifully_goldilocks : goldilocksHolds beautifully_ = true

theorem Phenomena.Gradability.Intensifiers.delightfully_goldilocks : goldilocksHolds delightfully = true

theorem Phenomena.Gradability.Intensifiers.gorgeously_goldilocks : goldilocksHolds gorgeously = true

theorem Phenomena.Gradability.Intensifiers.unusually_goldilocks : goldilocksHolds unusually = true

theorem Phenomena.Gradability.Intensifiers.surprisingly_goldilocks : goldilocksHolds surprisingly = true

theorem Phenomena.Gradability.Intensifiers.impossibly_goldilocks : goldilocksHolds impossibly = true

theorem Phenomena.Gradability.Intensifiers.remarkably_goldilocks : goldilocksHolds remarkably = true

theorem Phenomena.Gradability.Intensifiers.stunningly_goldilocks : goldilocksHolds stunningly = true

def Phenomena.Gradability.Intensifiers.zwickyHolds (e : IntensifierEntry) : Bool

Zwicky's generalization (§2.5, @cite{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 Phenomena.Gradability.Intensifiers.unusually_zwicky : zwickyHolds unusually = true

theorem Phenomena.Gradability.Intensifiers.surprisingly_zwicky : zwickyHolds surprisingly = true

theorem Phenomena.Gradability.Intensifiers.impossibly_zwicky : zwickyHolds impossibly = true

theorem Phenomena.Gradability.Intensifiers.usually_zwicky : zwickyHolds usually_ = true

theorem Phenomena.Gradability.Intensifiers.expectedly_zwicky : zwickyHolds expectedly_ = true

theorem Phenomena.Gradability.Intensifiers.possibly_zwicky : zwickyHolds possibly_ = true

def Phenomena.Gradability.Intensifiers.attestedCount : ℕ

Count of attested intensifiers

Equations

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

def Phenomena.Gradability.Intensifiers.unattestedCount : ℕ

Count of unattested intensifiers

Equations

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

def Phenomena.Gradability.Intensifiers.IntensifierEntry.fragmentEntry (e : IntensifierEntry) : Option Semantics.Gradability.GradableAdjEntry

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Phenomena.Gradability.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 Phenomena.Gradability.Intensifiers.all_valences_agree : (allEntries.all fun (e : IntensifierEntry) => (e.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjEntry) => 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 Phenomena.Gradability.Intensifiers.non_necessity_bases_open_scale : ((List.filter (fun (e : IntensifierEntry) => e.adjBase != "decent") allEntries).all fun (e : IntensifierEntry) => match e.fragmentEntry with | some a => a.scaleType == Core.Scale.Boundedness.open_ | none => false) = true

All intensifier bases except necessity-standard evaluatives have open scales (§2.1, fn. 3: "I will restrict my attention to adjectives with open-ended scales"). "Decent" is the one exception: it has a lower-bounded scale (@cite{kennedy-mcnally-2005} necessity standard). Derived from Fragment.

theorem Phenomena.Gradability.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 Phenomena.Gradability.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 Phenomena.Gradability.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 Phenomena.Gradability.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 Phenomena.Gradability.Intensifiers.zwicky_universal : allEntries.all zwickyHolds = true

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

theorem Phenomena.Gradability.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 Phenomena.Gradability.Intensifiers.antonym_pairs_resolve : (allEntries.all fun (e : IntensifierEntry) => match e.fragmentEntry.bind fun (x : Semantics.Gradability.GradableAdjEntry) => x.antonymForm with | some ant => (Fragments.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 = Core.Scale.Degree 6

@[reducible, inline]

abbrev RSA.Nouwen2024.Threshold : Type

Equations

• RSA.Nouwen2024.Threshold = Core.Scale.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 (Semantics.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 Core.Scale.Degree.toNat h with | 0 => 1 | 1 => 5 | 2 => 10 | 3 => 20 | 4 => 10 | 5 => 5 | x => 1

noncomputable def RSA.Nouwen2024.heightPriorR (h : Height) : ℝ

Equations

• RSA.Nouwen2024.heightPriorR h = ↑(RSA.Nouwen2024.heightPrior h)

theorem RSA.Nouwen2024.heightPriorR_nonneg (h : Height) : 0 ≤ heightPriorR h

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 Core.Scale.Degree.toNat h ≥ 3 then Core.Scale.Degree.toNat h - 3 else 3 - Core.Scale.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 Core.Scale.Degree.toNat h ≥ 3 then 6 - Core.Scale.Degree.toNat h else Core.Scale.Degree.toNat h

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

Full meaning function.

• bare_warm: h > θ (standard @cite{lassiter-goodman-2017})
• 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 > Core.Scale.Threshold.toNat θ_e))
• RSA.Nouwen2024.meaning RSA.Nouwen2024.Utterance.pleasantly_warm h θ θ_e = (RSA.Nouwen2024.tallMeaning θ h && decide (RSA.Nouwen2024.muPleasant h > Core.Scale.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.

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 (Core.Scale.Degree.toNat h₁) = muUsual.mu (Core.Scale.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

noncomputable def RSA.Nouwen2024.utteranceCostR (u : Utterance) : ℝ

Equations

• RSA.Nouwen2024.utteranceCostR u = ↑(RSA.Nouwen2024.utteranceCost u)

noncomputable def RSA.Nouwen2024.intensifierS1Score : (Utterance → Height → ℝ) → ℝ → Threshold × Threshold → Height → Utterance → ℝ

S1 scoring rule: exp(α · (log L0(h|u,θ,θ_e) − C(u))), gated at L0=0. Identical to @cite{lassiter-goodman-2017}'s beliefAction but with Latent = Threshold × Threshold for the dual-threshold model.

Equations

• RSA.Nouwen2024.intensifierS1Score l0 α x✝ w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - RSA.Nouwen2024.utteranceCostR u))

theorem RSA.Nouwen2024.intensifierS1Score_nonneg (l0 : Utterance → Height → ℝ) (α : ℝ) (l : Threshold × Threshold) (w : Height) (u : Utterance) : (∀ (u' : Utterance) (w' : Height), 0 ≤ l0 u' w') → 0 < α → 0 ≤ intensifierS1Score l0 α l w u

@[reducible]

noncomputable def RSA.Nouwen2024.nouwenCfg : RSAConfig Utterance Height

RSAConfig for the simultaneous dual-threshold model.

Extends @cite{lassiter-goodman-2017} threshold RSA with a second threshold for the evaluative adverb. L1 jointly infers height, adjective threshold, and evaluative threshold:

P_L1(h, θ, θ_e | u) ∝ P_S1(u | h, θ, θ_e) · P(h) · P(θ) · P(θ_e)

The meaning function uses local ℕ-valued evaluative measures, proved equivalent to Intensification.intensifiedMeaning by meaning_grounded_horribly and meaning_grounded_pleasantly.

Equations

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

H-adverb: "horribly warm" shifts height toward extremes

The Goldilocks effect for negative-evaluative bases: μ_horrible(h) = |h − norm| peaks at extremes, so L1 hearing "horribly warm" concentrates probability on extreme heights. Heights near the norm (h=3) have μ_horrible = 0 and cannot satisfy the evaluative positive form at any θ_e.

theorem RSA.Nouwen2024.horribly_shifts_upward : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 5 ⋯) > nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 2 ⋯)

theorem RSA.Nouwen2024.horribly_implies_warm : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 5 ⋯) > nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 1 ⋯)

M-adverb: "pleasantly warm" concentrates at moderate heights

The Goldilocks effect for positive-evaluative bases: μ_pleasant(h) = norm − |h − norm| peaks at the norm (h=3), so L1 hearing "pleasantly warm" concentrates probability on moderate heights. Extreme heights (h=5,6) have low μ_pleasant and cannot satisfy the evaluative positive form.

theorem RSA.Nouwen2024.pleasantly_prefers_moderate : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 6 ⋯)

theorem RSA.Nouwen2024.pleasantly_implies_warm : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 1 ⋯)

Cross-utterance Goldilocks predictions

The core Goldilocks effect is a cross-utterance phenomenon: intensifiers redistribute probability mass relative to the bare adjective. "Horribly warm" assigns MORE probability to extreme heights than "warm" does; "pleasantly warm" assigns MORE to moderate heights than "warm" does.

theorem RSA.Nouwen2024.horribly_above_bare_at_extreme : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 5 ⋯) > nouwenCfg.L1 Utterance.bare_warm (Core.Scale.deg 5 ⋯)

At extreme heights, "horribly warm" assigns more probability than "warm".

theorem RSA.Nouwen2024.pleasantly_above_bare_at_moderate : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.bare_warm (Core.Scale.deg 4 ⋯)

At moderate heights, "pleasantly warm" assigns more probability than "warm".

theorem RSA.Nouwen2024.horribly_dominates_pleasantly_at_extreme : nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 6 ⋯) > nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 6 ⋯)

At extreme heights, "horribly warm" dominates "pleasantly warm".

theorem RSA.Nouwen2024.pleasantly_dominates_horribly_at_moderate : nouwenCfg.L1 Utterance.pleasantly_warm (Core.Scale.deg 4 ⋯) > nouwenCfg.L1 Utterance.horribly_warm (Core.Scale.deg 4 ⋯)

At moderate heights, "pleasantly warm" dominates "horribly warm".

Sequential Dual-Threshold Model

key theoretical contribution: the evaluative adverb and base adjective apply sequentially rather than simultaneously. The listener first updates beliefs via the evaluative measure, then applies the adjective threshold to the resulting posterior:

Step 1: P₁(h | "horribly") ∝ P_S1(eval_pos | h, θ_e) · P(h) · P(θ_e) Step 2: P₂(h | "warm") ∝ P_S1(warm | h, θ) · P₁(h) · P(θ)

This sequential model makes the same Goldilocks predictions as the simultaneous model for simple cases, but differs for complex constructions (e.g., "horribly pleasantly warm").

Implementation

Two RSAConfigs composed: the evaluative step's L1 posterior feeds as the adjective step's worldPrior. This uses RSAConfig composition rather than the Ctx/transition machinery, which is designed for sequential production (word-by-word S1 choices), not sequential comprehension (listener updating beliefs step by step).

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 > Core.Scale.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

noncomputable def RSA.Nouwen2024.evalCostR (u : EvalUtterance) : ℝ

Equations

• RSA.Nouwen2024.evalCostR u = ↑(RSA.Nouwen2024.evalCost u)

noncomputable def RSA.Nouwen2024.evalS1Score : (EvalUtterance → Height → ℝ) → ℝ → Threshold → Height → EvalUtterance → ℝ

Equations

• RSA.Nouwen2024.evalS1Score l0 α x✝ w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - RSA.Nouwen2024.evalCostR u))

theorem RSA.Nouwen2024.evalS1Score_nonneg (l0 : EvalUtterance → Height → ℝ) (α : ℝ) (l : Threshold) (w : Height) (u : EvalUtterance) : (∀ (u' : EvalUtterance) (w' : Height), 0 ≤ l0 u' w') → 0 < α → 0 ≤ evalS1Score l0 α l w u

@[reducible]

noncomputable def RSA.Nouwen2024.evalCfg (evalMu : Height → ℕ) : RSAConfig EvalUtterance Height

RSAConfig for the evaluative step with a given measure function.

L1 hears the evaluative form and infers a posterior over heights, marginalizing over the evaluative threshold θ_e.

Equations

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

inductive RSA.Nouwen2024.AdjUtterance : Type

Utterances for the adjective step.

• warm : AdjUtterance
• silent : AdjUtterance

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.instReprAdjUtterance : Repr AdjUtterance

Equations

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

@[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

noncomputable def RSA.Nouwen2024.adjCostR (u : AdjUtterance) : ℝ

Equations

• RSA.Nouwen2024.adjCostR u = ↑(RSA.Nouwen2024.adjCost u)

noncomputable def RSA.Nouwen2024.adjS1Score : (AdjUtterance → Height → ℝ) → ℝ → Threshold → Height → AdjUtterance → ℝ

Equations

• RSA.Nouwen2024.adjS1Score l0 α x✝ w u = if l0 u w = 0 then 0 else Real.exp (α * (Real.log (l0 u w) - RSA.Nouwen2024.adjCostR u))

theorem RSA.Nouwen2024.adjS1Score_nonneg (l0 : AdjUtterance → Height → ℝ) (α : ℝ) (l : Threshold) (w : Height) (u : AdjUtterance) : (∀ (u' : AdjUtterance) (w' : Height), 0 ≤ l0 u' w') → 0 < α → 0 ≤ adjS1Score l0 α l w u

@[reducible]

noncomputable def RSA.Nouwen2024.seqAdjCfg (evalMu : Height → ℕ) : RSAConfig AdjUtterance Height

RSAConfig for the adjective step with the evaluative posterior as L0 prior AND L1 worldPrior.

Implements @cite{nouwen-2024} eq (73): the second update applies L&G's pragmatic listener (eq 71) with prior Π = (evalCfg evalMu).L1 .eval_pos. Per L&G, that prior enters in TWO places — inside the literal listener's normalization (via meaning) AND in the pragmatic listener's Bayesian inversion (via worldPrior). Both copies are intentional and faithful to the paper, NOT double-counting. The expanded formula is:

P₂(h | "warm") ∝ Π(h) · Σ_θ P(θ) · S1("warm" | h, θ, Π)

where S1 has Π baked in via the literal listener π in its log-utility ln π(h | "warm", θ, Π) - cost. The "P_S1 · L1_eval · P(θ)" shorthand from the prose section above is true at the L1 layer but elides the L1_eval that also lives inside P_S1's own L&G-style L0 normalization.

Future direction: when the in-flight RSA → mathlib-PMF migration (project_rsa_pmf_migration.md, Phase 3-5) reaches Phase 5 consumer migration, this file's evalCfg and seqAdjCfg will be expressed as PMF.posterior chained via PMF.bind (the listener-side L1 → next prior pattern). Until then the L&G two-prior structure is encoded inline by writing evalCfg.L1 in both fields, which the rsa_predict tactic handles correctly.

Equations

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

noncomputable def RSA.Nouwen2024.seqL1_horribly (h : Height) : ℝ

Sequential L1 posterior for "horribly warm": evaluative step uses μ_horrible, then adjective step applies the base "warm" meaning.

Equations

• RSA.Nouwen2024.seqL1_horribly h = (RSA.Nouwen2024.seqAdjCfg RSA.Nouwen2024.muHorrible).L1 RSA.Nouwen2024.AdjUtterance.warm h

noncomputable def RSA.Nouwen2024.seqL1_pleasantly (h : Height) : ℝ

Sequential L1 posterior for "pleasantly warm": evaluative step uses μ_pleasant, then adjective step applies the base "warm" meaning.

Equations

• RSA.Nouwen2024.seqL1_pleasantly h = (RSA.Nouwen2024.seqAdjCfg RSA.Nouwen2024.muPleasant).L1 RSA.Nouwen2024.AdjUtterance.warm h

Sequential Goldilocks: same qualitative predictions as simultaneous

The sequential model produces the same Goldilocks pattern: "horribly warm" shifts probability toward extremes, "pleasantly warm" concentrates at moderate heights. The sequential decomposition affects the quantitative distribution but preserves the qualitative ordering.

theorem RSA.Nouwen2024.seq_horribly_shifts_upward : (seqAdjCfg muHorrible).L1 AdjUtterance.warm (Core.Scale.deg 5 ⋯) > (seqAdjCfg muHorrible).L1 AdjUtterance.warm (Core.Scale.deg 2 ⋯)

Sequential "horribly warm" shifts upward (Goldilocks).

theorem RSA.Nouwen2024.seq_pleasantly_prefers_moderate : (seqAdjCfg muPleasant).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > (seqAdjCfg muPleasant).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

Sequential "pleasantly warm" prefers moderate heights (Goldilocks).

Zwicky Vacuity: Derived from RSA

§5: Positive modal adverbs (*usually, *expectedly) cannot serve as intensifiers because their evaluative measure is constant across heights, providing no discriminating information about degree. In the sequential model, the evaluative step with a constant measure preserves the prior's bell-curve shape — "usually warm" offers no intensifying information beyond bare "warm".

In contrast, negative modal measures (unusual ≈ horrible) peak at extremes, shifting the evaluative posterior away from the norm and producing genuine intensification. This is why negative modals pattern with negative evaluatives in the Goldilocks effect.

The theorems below derive Zwicky's generalization from the sequential RSA model, connecting the data-layer check (zwickyHolds) to L1 posterior predictions.

def RSA.Nouwen2024.muUsualN : Height → ℕ

ℕ-valued constant measure for the sequential model. Models "usual": μ_usual(h) = 3 for all h (no height discrimination).

Equations

• RSA.Nouwen2024.muUsualN x✝ = 3

def RSA.Nouwen2024.muUnusualN : Height → ℕ

μ_unusual has the same shape as μ_horrible: peaks at extremes. Deviation-denoting adjectives (unusual, impossible) pattern with negative evaluatives (horrible, terrible) because both assign high values to heights far from the norm (§5).

Equations

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

theorem RSA.Nouwen2024.muUnusualN_eq_muHorrible : muUnusualN = muHorrible

Deviation measures and negative evaluative measures are structurally identical. This is the semantic foundation of why both types make good intensifiers — "the corresponding measure function has a shape similar to that of negative evaluatives" (§5).

@[reducible]

noncomputable def RSA.Nouwen2024.bareAdjCfg : RSAConfig AdjUtterance Height

Bare adjective RSAConfig: "warm" vs silence with the original height prior. This is the baseline — what "warm" means without any evaluative step.

Equations

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

Evaluative Step: Constant vs Extreme Measures

theorem RSA.Nouwen2024.eval_constant_preserves_peak : (evalCfg muUsualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 3 ⋯) > (evalCfg muUsualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 6 ⋯)

Constant-measure evaluative step preserves the prior's peak at the norm.

theorem RSA.Nouwen2024.eval_unusual_boosts_extreme : (evalCfg muUnusualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 6 ⋯) > (evalCfg muUsualN).L1 EvalUtterance.eval_pos (Core.Scale.deg 6 ⋯)

Extreme measure (unusual/horrible) boosts extreme heights in L1 beyond what the constant measure assigns.

Sequential Model: Zwicky Predictions

theorem RSA.Nouwen2024.usually_warm_prefers_moderate : (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

"Usually warm" preserves moderate-height preference (like bare "warm").

theorem RSA.Nouwen2024.unusually_warm_shifts_extreme : (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 5 ⋯) > (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 2 ⋯)

"Unusually warm" shifts toward extremes (like "horribly warm"). Note: muUnusualN = muHorrible by muUnusualN_eq_muHorrible, so this is structurally the same prediction as seq_horribly_shifts_upward.

theorem RSA.Nouwen2024.zwicky_extreme_discrimination : (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯) > (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

Zwicky's generalization, derived: at extreme heights, "unusually warm" assigns more probability than "usually warm". Negative modal intensifiers are more informative than positive modal ones because μ_unusual discriminates heights while μ_usual does not.

theorem RSA.Nouwen2024.zwicky_moderate_discrimination : (seqAdjCfg muUsualN).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > (seqAdjCfg muUnusualN).L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯)

Converse: at moderate heights, "usually warm" dominates "unusually warm". The constant measure concentrates mass near the prior peak, while the extreme measure depletes mass at moderate heights.

theorem RSA.Nouwen2024.bare_warm_prefers_moderate : bareAdjCfg.L1 AdjUtterance.warm (Core.Scale.deg 4 ⋯) > bareAdjCfg.L1 AdjUtterance.warm (Core.Scale.deg 6 ⋯)

Bare "warm" baseline: prefers moderate heights (deg 4 > deg 6). Demonstrates that the bare model and "usually warm" agree qualitatively.