structure Semantics.Gradability.ThresholdPair (max : ℕ) : Type

A threshold pair for contrary antonyms.

For contrary pairs like happy/unhappy:

• theta_pos: threshold for positive form (degree > theta_pos -> "happy")
• theta_neg: threshold for negative form (degree < theta_neg -> "unhappy")
• Constraint: theta_neg <= theta_pos (gap exists when theta_neg < theta_pos)

• pos : Core.Scale.Threshold max
• neg : Core.Scale.Threshold max
• gap_exists : self.neg ≤ self.pos

@[implicit_reducible]

instance Semantics.Gradability.instReprThresholdPair {max✝ : ℕ} : Repr (ThresholdPair max✝)

Equations

• Semantics.Gradability.instReprThresholdPair = { reprPrec := Semantics.Gradability.instReprThresholdPair.repr }

def Semantics.Gradability.instReprThresholdPair.repr {max✝ : ℕ} : ThresholdPair max✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instInhabitedThresholdPairOfAutoParamLtNatOfNat_auto_13 {n : ℕ} (h : 0 < n := by omega) : Inhabited (ThresholdPair n)

Equations

• Semantics.Gradability.instInhabitedThresholdPairOfAutoParamLtNatOfNat_auto_13 h = { default := { pos := { value := ⟨0, h⟩ }, neg := { value := ⟨0, h⟩ }, gap_exists := ⋯ } }

@[implicit_reducible]

instance Semantics.Gradability.instBEqThresholdPair {n : ℕ} : BEq (ThresholdPair n)

Equations

• Semantics.Gradability.instBEqThresholdPair = { beq := fun (t1 t2 : Semantics.Gradability.ThresholdPair n) => t1.pos == t2.pos && t1.neg == t2.neg }

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqThresholdPair {n : ℕ} : DecidableEq (ThresholdPair n)

Equations

• Semantics.Gradability.instDecidableEqThresholdPair t1 t2 = if hp : t1.pos = t2.pos then if hn : t1.neg = t2.neg then isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Semantics.Gradability.contradictoryNeg {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Prop

Contradictory negation: "not happy" = degree ≤ theta. Alias for Semantics.Degree.antonymMeaning — same comparison, named for its role in the contradictory/contrary distinction.

Equations

• Semantics.Gradability.contradictoryNeg d θ = Semantics.Degree.antonymMeaning d θ

@[reducible, inline]

abbrev Semantics.Gradability.contraryNeg {max : ℕ} (d : Core.Scale.Degree max) (θ_neg : Core.Scale.Threshold max) : Prop

Contrary negation: "unhappy" = degree < theta_neg. Alias for Semantics.Degree.negativeMeaning.

Equations

• Semantics.Gradability.contraryNeg d θ_neg = Semantics.Degree.negativeMeaning d θ_neg

@[reducible, inline]

abbrev Semantics.Gradability.inGapRegion {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Prop

Check if a degree is in the gap region (neither positive nor negative).

Equations

• Semantics.Gradability.inGapRegion d tp = ({ value := tp.neg.value.castSucc } ≤ d ∧ d ≤ { value := tp.pos.value.castSucc })

@[reducible, inline]

abbrev Semantics.Gradability.positiveMeaning' {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Prop

Positive meaning in the two-threshold model: degree > theta_pos. Alias for Semantics.Degree.positiveMeaning projected through tp.pos.

Equations

• Semantics.Gradability.positiveMeaning' d tp = Semantics.Degree.positiveMeaning d tp.pos

@[reducible, inline]

abbrev Semantics.Gradability.contraryNegMeaning {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Prop

Negative meaning in the two-threshold model: degree < theta_neg. Alias for Semantics.Degree.negativeMeaning projected through tp.neg.

Equations

• Semantics.Gradability.contraryNegMeaning d tp = Semantics.Degree.negativeMeaning d tp.neg

@[reducible, inline]

abbrev Semantics.Gradability.notContraryNegMeaning {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Prop

Negation of contrary negative: "not unhappy" = degree >= theta_neg.

Equations

• Semantics.Gradability.notContraryNegMeaning d tp = ({ value := tp.neg.value.castSucc } ≤ d)

@[reducible, inline]

abbrev Semantics.Gradability.AntonymRelation : Type

The relation between a positive form and its antonym.

Equations

• Semantics.Gradability.AntonymRelation = Features.NegationType

inductive Semantics.Gradability.InformationalStrength : Type

Informational strength of a gradable adjective within its scale.

Weak adjectives (e.g., "large", "clean") occupy a broader region of the scale. Strong adjectives (e.g., "gigantic", "pristine") occupy a narrower, more extreme region.

A strong adjective entails its weak counterpart on the same pole: "x is gigantic" ⟹ "x is large", but not vice versa.

This distinction is orthogonal to scale structure (relative vs absolute) and polarity (positive vs negative).

Source: @cite{alexandropoulou-gotzner-2024}, @cite{horn-1972}

• weak : InformationalStrength
• strong : InformationalStrength

def Semantics.Gradability.instReprInformationalStrength.repr : InformationalStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instReprInformationalStrength : Repr InformationalStrength

Equations

• Semantics.Gradability.instReprInformationalStrength = { reprPrec := Semantics.Gradability.instReprInformationalStrength.repr }

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqInformationalStrength : DecidableEq InformationalStrength

Equations

• Semantics.Gradability.instDecidableEqInformationalStrength x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Semantics.Gradability.SpatialConfigType : Type

Spatial configuration type for adjectives in resultative constructions (@cite{levin-2026}). Only adjectives describing spatially instantiated states license intr-push open resultatives.

• barrierConfig : SpatialConfigType
• unattachment : SpatialConfigType
• surfaceOrient : SpatialConfigType

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqSpatialConfigType : DecidableEq SpatialConfigType

Equations

• Semantics.Gradability.instDecidableEqSpatialConfigType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Semantics.Gradability.instReprSpatialConfigType : Repr SpatialConfigType

Equations

• Semantics.Gradability.instReprSpatialConfigType = { reprPrec := Semantics.Gradability.instReprSpatialConfigType.repr }

def Semantics.Gradability.instReprSpatialConfigType.repr : SpatialConfigType → ℕ → Std.Format

Equations

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

structure Semantics.Gradability.GradableAdjEntry : Type

A gradable adjective lexical entry. Bundles surface form, scale structure, and antonym information. The actual threshold is NOT part of the lexical entry — it's contextual.

• form : String
• scaleType : Core.Scale.Boundedness
• dimension : Features.Dimension
• antonymForm : Option String
• antonymRelation : Option AntonymRelation
• spatialConfigType : Option SpatialConfigType
• evaluativeValence : Option Features.EvaluativeValence

  Evaluative valence of the adjective, when applicable. Determines intensifier degree class (@cite{nouwen-2024}): negative-evaluative bases yield H-degree intensifiers, positive-evaluative bases yield M-degree intensifiers.

@[implicit_reducible]

instance Semantics.Gradability.instReprGradableAdjEntry : Repr GradableAdjEntry

Equations

• Semantics.Gradability.instReprGradableAdjEntry = { reprPrec := Semantics.Gradability.instReprGradableAdjEntry.repr }

def Semantics.Gradability.instReprGradableAdjEntry.repr : GradableAdjEntry → ℕ → Std.Format

Equations

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

inductive Semantics.Gradability.DimensionBindingType : Type

How a multidimensional adjective binds its dimensions (@cite{sassoon-2013}).

• conjunctive: entity must meet standard in ALL dimensions (e.g., healthy)
• disjunctive: entity must meet standard in SOME dimension (e.g., sick)
• mixed: context determines ∀ vs ∃ (e.g., intelligent)

• conjunctive : DimensionBindingType
• disjunctive : DimensionBindingType
• mixed : DimensionBindingType

def Semantics.Gradability.instReprDimensionBindingType.repr : DimensionBindingType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Gradability.instReprDimensionBindingType : Repr DimensionBindingType

Equations

• Semantics.Gradability.instReprDimensionBindingType = { reprPrec := Semantics.Gradability.instReprDimensionBindingType.repr }

@[implicit_reducible]

instance Semantics.Gradability.instDecidableEqDimensionBindingType : DecidableEq DimensionBindingType

Equations

• Semantics.Gradability.instDecidableEqDimensionBindingType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Gradability.conjunctiveBinding {α : Type} (dims : List (α → Bool)) (x : α) : Bool

Conjunctive binding: ∀Q ∈ DIM(P,c). Q(x).

Equations

• Semantics.Gradability.conjunctiveBinding dims x = dims.all fun (x_1 : α → Bool) => x_1 x

def Semantics.Gradability.disjunctiveBinding {α : Type} (dims : List (α → Bool)) (x : α) : Bool

Disjunctive binding: ∃Q ∈ DIM(P,c). Q(x).

Equations

• Semantics.Gradability.disjunctiveBinding dims x = dims.any fun (x_1 : α → Bool) => x_1 x

theorem Semantics.Gradability.deMorgan_conjunctive_disjunctive {α : Type} (dims : List (α → Bool)) (x : α) : (!conjunctiveBinding dims x) = disjunctiveBinding (List.map (fun (d : α → Bool) (a : α) => !d a) dims) x

De Morgan: negating conjunctive binding yields disjunctive binding over negated dimension predicates. This is the formal core of @cite{sassoon-2013}'s Hypothesis 2 — under a negation theory of antonymy, if the positive form is conjunctive, the negative antonym (its negation) is disjunctive.

theorem Semantics.Gradability.deMorgan_disjunctive_conjunctive {α : Type} (dims : List (α → Bool)) (x : α) : (!disjunctiveBinding dims x) = conjunctiveBinding (List.map (fun (d : α → Bool) (a : α) => !d a) dims) x

def Semantics.Gradability.DimensionBindingType.negate : DimensionBindingType → DimensionBindingType

The predicted binding type for a negative antonym, given its positive counterpart's binding type. Follows from De Morgan under the negation theory of antonymy.

Equations

• Semantics.Gradability.DimensionBindingType.conjunctive.negate = Semantics.Gradability.DimensionBindingType.disjunctive
• Semantics.Gradability.DimensionBindingType.disjunctive.negate = Semantics.Gradability.DimensionBindingType.conjunctive
• Semantics.Gradability.DimensionBindingType.mixed.negate = Semantics.Gradability.DimensionBindingType.mixed

theorem Semantics.Gradability.negate_involutive (b : DimensionBindingType) : b.negate.negate = b

def Semantics.Gradability.predictedBinding : Degree.PositiveStandard → DimensionBindingType

@cite{sassoon-2013} Hypothesis 3: standard type predicts binding type. Total (max standard) → conjunctive, partial (min standard) → disjunctive, relative (contextual) → mixed.

Equations

• Semantics.Gradability.predictedBinding Semantics.Degree.PositiveStandard.maxEndpoint = Semantics.Gradability.DimensionBindingType.conjunctive
• Semantics.Gradability.predictedBinding Semantics.Degree.PositiveStandard.minEndpoint = Semantics.Gradability.DimensionBindingType.disjunctive
• Semantics.Gradability.predictedBinding Semantics.Degree.PositiveStandard.contextual = Semantics.Gradability.DimensionBindingType.mixed
• Semantics.Gradability.predictedBinding Semantics.Degree.PositiveStandard.functional = Semantics.Gradability.DimensionBindingType.mixed

structure Semantics.Gradability.GradableMLScale (α : Type u_1) [LinearOrder α] (W : Type u_2) extends Core.Scale.DirectedMeasure α W : Type (max u_1 u_2)

• boundedness : Boundedness
• μ : W → α
• direction : ScalePolarity
• ml : MLScale α

def Semantics.Gradability.marginalityPositive {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) : Prop

Equations

• Semantics.Gradability.marginalityPositive ml norm degree = ml.L norm degree

theorem Semantics.Gradability.marginality_entails_standard {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) (h : marginalityPositive ml norm degree) : norm < degree

Connecting concrete Degree max to abstract DirectedMeasure

Degree max has LinearOrder and BoundedOrder (from Core.MeasurementScale), so the abstract theorems in MeasurementScale.lean apply directly to concrete RSA degree computations.

def Semantics.Gradability.adjMeasure {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) (entry : GradableAdjEntry) : Core.Scale.DirectedMeasure (Core.Scale.Degree max) W

Equations

• Semantics.Gradability.adjMeasure μ entry = Core.Scale.DirectedMeasure.adjective μ entry.scaleType

theorem Semantics.Gradability.closedAdj_licensed {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) (entry : GradableAdjEntry) (h : entry.scaleType = Core.Scale.Boundedness.closed) : (adjMeasure μ entry).licensed = true

theorem Semantics.Gradability.openAdj_blocked {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) (entry : GradableAdjEntry) (h : entry.scaleType = Core.Scale.Boundedness.open_) : (adjMeasure μ entry).licensed = false

theorem Semantics.Gradability.degree_nontrivial {max : ℕ} (h : 1 ≤ max) : ∃ (x : Core.Scale.Degree max), x ≠ ⊤

theorem Semantics.Gradability.degree_admits_optimum {max : ℕ} (h : 1 ≤ max) : ∃ (P : Core.Scale.Degree max → Prop), (∀ (x y : Core.Scale.Degree max), x ≤ y → P x → P y) ∧ ¬∀ (x y : Core.Scale.Degree max), P x ↔ P y

theorem Semantics.Gradability.degree_measure_is_id {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Core.Scale.DirectedMeasure.numeral μ).μ = μ