@[reducible, inline]

abbrev Semantics.Lexical.Adjective.NegationType : Type

Antonymy type: contradictory (no gap) vs contrary (gap). Canonical definition in Core.PropertyDomain.

Equations

• Semantics.Lexical.Adjective.NegationType = Core.NegationType

structure Semantics.Lexical.Adjective.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

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

Equations

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

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

Equations

• Semantics.Lexical.Adjective.instReprThresholdPair = { reprPrec := Semantics.Lexical.Adjective.instReprThresholdPair.repr }

instance Semantics.Lexical.Adjective.instInhabitedThresholdPairOfAutoParamLtNatOfNat_auto_15 {n : ℕ} (h : 0 < n := by omega) : Inhabited (ThresholdPair n)

Equations

• Semantics.Lexical.Adjective.instInhabitedThresholdPairOfAutoParamLtNatOfNat_auto_15 h = { default := { pos := { value := ⟨0, h⟩ }, neg := { value := ⟨0, h⟩ }, gap_exists := ⋯ } }

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

Equations

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

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

Equations

• Semantics.Lexical.Adjective.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.Lexical.Adjective.contradictoryNeg {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Bool

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

Equations

• Semantics.Lexical.Adjective.contradictoryNeg d θ = Semantics.Degree.antonymMeaning d θ

def Semantics.Lexical.Adjective.contraryNeg {max : ℕ} (d : Core.Scale.Degree max) (θ_neg : Core.Scale.Threshold max) : Bool

Contrary negation: "unhappy" = degree < theta_neg.

Equations

• Semantics.Lexical.Adjective.contraryNeg d θ_neg = decide (d < { value := θ_neg.value.castSucc })

def Semantics.Lexical.Adjective.inGapRegion {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Bool

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

Equations

• Semantics.Lexical.Adjective.inGapRegion d tp = (decide ({ value := tp.neg.value.castSucc } ≤ d) && decide (d ≤ { value := tp.pos.value.castSucc }))

def Semantics.Lexical.Adjective.positiveMeaning' {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Bool

Positive meaning with two-threshold model: degree > theta_pos.

Equations

• Semantics.Lexical.Adjective.positiveMeaning' d tp = decide ({ value := tp.pos.value.castSucc } < d)

def Semantics.Lexical.Adjective.contraryNegMeaning {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Bool

Negative meaning with contrary semantics: "unhappy" = degree < theta_neg.

Equations

• Semantics.Lexical.Adjective.contraryNegMeaning d tp = decide (d < { value := tp.neg.value.castSucc })

def Semantics.Lexical.Adjective.notContraryNegMeaning {max : ℕ} (d : Core.Scale.Degree max) (tp : ThresholdPair max) : Bool

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

Equations

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

@[reducible, inline]

abbrev Semantics.Lexical.Adjective.AntonymRelation : Type

The relation between a positive form and its antonym.

Equations

• Semantics.Lexical.Adjective.AntonymRelation = Semantics.Lexical.Adjective.NegationType

inductive Semantics.Lexical.Adjective.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

instance Semantics.Lexical.Adjective.instReprInformationalStrength : Repr InformationalStrength

Equations

• Semantics.Lexical.Adjective.instReprInformationalStrength = { reprPrec := Semantics.Lexical.Adjective.instReprInformationalStrength.repr }

def Semantics.Lexical.Adjective.instReprInformationalStrength.repr : InformationalStrength → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Adjective.instDecidableEqInformationalStrength : DecidableEq InformationalStrength

Equations

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

instance Semantics.Lexical.Adjective.instBEqInformationalStrength : BEq InformationalStrength

Equations

• Semantics.Lexical.Adjective.instBEqInformationalStrength = { beq := Semantics.Lexical.Adjective.instBEqInformationalStrength.beq }

def Semantics.Lexical.Adjective.instBEqInformationalStrength.beq : InformationalStrength → InformationalStrength → Bool

Equations

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

inductive Semantics.Lexical.Adjective.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

instance Semantics.Lexical.Adjective.instDecidableEqSpatialConfigType : DecidableEq SpatialConfigType

Equations

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

def Semantics.Lexical.Adjective.instBEqSpatialConfigType.beq : SpatialConfigType → SpatialConfigType → Bool

Equations

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

instance Semantics.Lexical.Adjective.instBEqSpatialConfigType : BEq SpatialConfigType

Equations

• Semantics.Lexical.Adjective.instBEqSpatialConfigType = { beq := Semantics.Lexical.Adjective.instBEqSpatialConfigType.beq }

instance Semantics.Lexical.Adjective.instReprSpatialConfigType : Repr SpatialConfigType

Equations

• Semantics.Lexical.Adjective.instReprSpatialConfigType = { reprPrec := Semantics.Lexical.Adjective.instReprSpatialConfigType.repr }

def Semantics.Lexical.Adjective.instReprSpatialConfigType.repr : SpatialConfigType → ℕ → Std.Format

Equations

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

structure Semantics.Lexical.Adjective.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 : Core.Dimension
• antonymForm : Option String
• antonymRelation : Option AntonymRelation
• spatialConfigType : Option SpatialConfigType

instance Semantics.Lexical.Adjective.instReprGradableAdjEntry : Repr GradableAdjEntry

Equations

• Semantics.Lexical.Adjective.instReprGradableAdjEntry = { reprPrec := Semantics.Lexical.Adjective.instReprGradableAdjEntry.repr }

def Semantics.Lexical.Adjective.instReprGradableAdjEntry.repr : GradableAdjEntry → ℕ → Std.Format

Equations

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

inductive Semantics.Lexical.Adjective.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

instance Semantics.Lexical.Adjective.instReprDimensionBindingType : Repr DimensionBindingType

Equations

• Semantics.Lexical.Adjective.instReprDimensionBindingType = { reprPrec := Semantics.Lexical.Adjective.instReprDimensionBindingType.repr }

def Semantics.Lexical.Adjective.instReprDimensionBindingType.repr : DimensionBindingType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Adjective.instDecidableEqDimensionBindingType : DecidableEq DimensionBindingType

Equations

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

def Semantics.Lexical.Adjective.instBEqDimensionBindingType.beq : DimensionBindingType → DimensionBindingType → Bool

Equations

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

instance Semantics.Lexical.Adjective.instBEqDimensionBindingType : BEq DimensionBindingType

Equations

• Semantics.Lexical.Adjective.instBEqDimensionBindingType = { beq := Semantics.Lexical.Adjective.instBEqDimensionBindingType.beq }

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

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

Equations

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

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

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

Equations

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

theorem Semantics.Lexical.Adjective.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.Lexical.Adjective.deMorgan_disjunctive_conjunctive {α : Type} (dims : List (α → Bool)) (x : α) : (!disjunctiveBinding dims x) = conjunctiveBinding (List.map (fun (d : α → Bool) (a : α) => !d a) dims) x

def Semantics.Lexical.Adjective.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.Lexical.Adjective.DimensionBindingType.conjunctive.negate = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive
• Semantics.Lexical.Adjective.DimensionBindingType.disjunctive.negate = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive
• Semantics.Lexical.Adjective.DimensionBindingType.mixed.negate = Semantics.Lexical.Adjective.DimensionBindingType.mixed

theorem Semantics.Lexical.Adjective.negate_involutive (b : DimensionBindingType) : b.negate.negate = b

def Semantics.Lexical.Adjective.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.Lexical.Adjective.predictedBinding Semantics.Degree.PositiveStandard.maxEndpoint = Semantics.Lexical.Adjective.DimensionBindingType.conjunctive
• Semantics.Lexical.Adjective.predictedBinding Semantics.Degree.PositiveStandard.minEndpoint = Semantics.Lexical.Adjective.DimensionBindingType.disjunctive
• Semantics.Lexical.Adjective.predictedBinding Semantics.Degree.PositiveStandard.contextual = Semantics.Lexical.Adjective.DimensionBindingType.mixed
• Semantics.Lexical.Adjective.predictedBinding Semantics.Degree.PositiveStandard.functional = Semantics.Lexical.Adjective.DimensionBindingType.mixed

structure Semantics.Lexical.Adjective.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.Lexical.Adjective.marginalityPositive {α : Type u_1} [LinearOrder α] (ml : MLScale α) (norm degree : α) : Prop

Equations

• Semantics.Lexical.Adjective.marginalityPositive ml norm degree = ml.L norm degree

theorem Semantics.Lexical.Adjective.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.Lexical.Adjective.adjMeasure {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) (entry : GradableAdjEntry) : Core.Scale.DirectedMeasure (Core.Scale.Degree max) W

Equations

• Semantics.Lexical.Adjective.adjMeasure μ entry = Core.Scale.DirectedMeasure.kennedyAdjective μ entry.scaleType

theorem Semantics.Lexical.Adjective.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.Lexical.Adjective.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.Lexical.Adjective.degree_nontrivial {max : ℕ} (h : 1 ≤ max) : ∃ (x : Core.Scale.Degree max), x ≠ ⊤

theorem Semantics.Lexical.Adjective.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.Lexical.Adjective.degree_measure_is_id {max : ℕ} {W : Type u_1} (μ : W → Core.Scale.Degree max) : (Core.Scale.DirectedMeasure.kennedyNumeral μ).μ = μ