inductive Semantics.Lexical.Adjective.Intensification.EvaluativeValence : Type

Evaluative valence of an adjectival base.

This is distinct from scalar polarity (positive/negative scale direction):

• positive: the adjective denotes a good/desirable property (pleasant, nice)
• negative: the adjective denotes a bad/undesirable property (horrible, terrible)
• neutral: no inherent evaluative content (usual, possible)

@cite{nouwen-2024} argues that evaluative valence, not scalar polarity, determines the intensifier's degree class.

• positive : EvaluativeValence
• negative : EvaluativeValence
• neutral : EvaluativeValence

instance Semantics.Lexical.Adjective.Intensification.instReprEvaluativeValence : Repr EvaluativeValence

Equations

• Semantics.Lexical.Adjective.Intensification.instReprEvaluativeValence = { reprPrec := Semantics.Lexical.Adjective.Intensification.instReprEvaluativeValence.repr }

def Semantics.Lexical.Adjective.Intensification.instReprEvaluativeValence.repr : EvaluativeValence → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Adjective.Intensification.instDecidableEqEvaluativeValence : DecidableEq EvaluativeValence

Equations

• Semantics.Lexical.Adjective.Intensification.instDecidableEqEvaluativeValence x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Adjective.Intensification.instBEqEvaluativeValence : BEq EvaluativeValence

Equations

• Semantics.Lexical.Adjective.Intensification.instBEqEvaluativeValence = { beq := Semantics.Lexical.Adjective.Intensification.instBEqEvaluativeValence.beq }

def Semantics.Lexical.Adjective.Intensification.instBEqEvaluativeValence.beq : EvaluativeValence → EvaluativeValence → Bool

Equations

• Semantics.Lexical.Adjective.Intensification.instBEqEvaluativeValence.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Semantics.Lexical.Adjective.Intensification.EvaluativeMeasure (max : ℕ) : Type

An evaluative measure function assigns a rational-valued "goodness of fit" score to each degree on a scale.

• form: the adjectival base (e.g., "horrible")
• valence: evaluative valence from the Phenomena layer
• mu: the measure function μ : Nat → ℚ (takes degree's Nat value)

The measure function captures how well a degree matches the evaluative meaning of the base adjective.

• form : String
• valence : EvaluativeValence
• mu : ℕ → ℚ

def Semantics.Lexical.Adjective.Intensification.muHorrible (max : ℕ) : EvaluativeMeasure max

Evaluative measure for negative-evaluative bases (horrible, terrible, etc.).

μ_horrible(d) = |d - norm|

Peaks at extremes (d = 0 and d = max), lowest at the norm. Negative-evaluative adjectives evaluate extreme degrees as more salient, which is why "horribly warm" targets high degrees.

Equations

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

def Semantics.Lexical.Adjective.Intensification.muPleasant (max : ℕ) : EvaluativeMeasure max

Evaluative measure for positive-evaluative bases (pleasant, nice, etc.).

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

Peaks at the norm (middle degrees), lowest at extremes. Positive-evaluative adjectives evaluate moderate degrees as best, which is why "pleasantly warm" targets moderate degrees.

Equations

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

def Semantics.Lexical.Adjective.Intensification.intensifiedMeaning {max : ℕ} (eval : EvaluativeMeasure max) (d : Core.Scale.Degree max) (θ_adj θ_eval : Core.Scale.Threshold max) : Bool

Intensified positive meaning (@cite{nouwen-2024}, eq. 45).

⟦ADV-ly ADJ⟧(d, θ_adj, θ_eval) = (d > θ_adj) ∧ (μ_eval(d) > θ_eval)

The intensified form is the conjunction (intersection) of:

1. The base adjective's positive form: d > θ_adj
2. The evaluative threshold: μ_eval(d) > θ_eval

Equations

• Semantics.Lexical.Adjective.Intensification.intensifiedMeaning eval d θ_adj θ_eval = (Semantics.Degree.positiveMeaning d θ_adj && decide (eval.mu d.toNat > ↑θ_eval.toNat))

theorem Semantics.Lexical.Adjective.Intensification.intensified_implies_positive {max : ℕ} (eval : EvaluativeMeasure max) (d : Core.Scale.Degree max) (θ_adj θ_eval : Core.Scale.Threshold max) (h : intensifiedMeaning eval d θ_adj θ_eval = true) : Degree.positiveMeaning d θ_adj = true

Intensified meaning entails the positive form.

If "horribly warm" is true, then "warm" is true. This is because the intensified meaning is a conjunction that includes the positive meaning as one conjunct.

theorem Semantics.Lexical.Adjective.Intensification.muHorrible_peaks_at_extreme_10 : (muHorrible 10).mu 10 ≥ (muHorrible 10).mu 5

The horrible measure peaks at extremes: μ(max) ≥ μ(norm).

Negative-evaluative adjectives assign highest values to extreme degrees.

theorem Semantics.Lexical.Adjective.Intensification.muPleasant_peaks_at_norm_10 : (muPleasant 10).mu 5 ≥ (muPleasant 10).mu 10

The pleasant measure peaks at norm: μ(norm) ≥ μ(max).

Positive-evaluative adjectives assign highest values to moderate degrees.

theorem Semantics.Lexical.Adjective.Intensification.goldilocks_at_extreme_10 : (muHorrible 10).mu 10 ≥ (muPleasant 10).mu 10

Goldilocks structural theorem: at extreme degrees (d = max), the horrible measure exceeds the pleasant measure.

This is the semantic foundation of the Goldilocks effect: extreme degrees are more "horrible" than "pleasant".

theorem Semantics.Lexical.Adjective.Intensification.goldilocks_at_norm_10 : (muPleasant 10).mu 5 ≥ (muHorrible 10).mu 5

Goldilocks structural theorem (converse): at moderate degrees (d = norm), the pleasant measure exceeds the horrible measure.

Moderate degrees are more "pleasant" than "horrible".

theorem Semantics.Lexical.Adjective.Intensification.negative_valence_extreme_peak : (muHorrible 10).valence = EvaluativeValence.negative ∧ (muHorrible 10).mu 10 ≥ (muHorrible 10).mu 5

Bridge between evaluative valence and evaluative measure behavior: negative-evaluative measures peak at extremes, positive at the norm.

This connects the Phenomena-layer EvaluativeValence to the Theory-layer EvaluativeMeasure structural properties.

theorem Semantics.Lexical.Adjective.Intensification.positive_valence_norm_peak : (muPleasant 10).valence = EvaluativeValence.positive ∧ (muPleasant 10).mu 5 ≥ (muPleasant 10).mu 10