@cite{alexandropoulou-gotzner-2024} — Negated Gradable Adjectives

@cite{alexandropoulou-gotzner-2024}

Extension gap (contrary antonyms, two thresholds) is the structural precondition for polarity asymmetry under negation. Contradictory antonyms (single threshold) produce symmetric negation.

Load-bearing connections

• positiveMeaning' / contraryNegMeaning (Theory.lean) = positiveMeaning / negativeMeaning (Core.lean) applied to ThresholdPair projections (§4)
• Three-region exhaustive partition from ThresholdPair (§5)
• Contradictory complement: positiveMeaning ∨ antonymMeaning always (§6)
• positiveMeaning_monotone grounds strength entailment and precision DPL (§7, §9)

inductive Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.EvaluativePolarity : Type

• positive : EvaluativePolarity
• negative : EvaluativePolarity

instance Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprEvaluativePolarity : Repr EvaluativePolarity

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprEvaluativePolarity = { reprPrec := Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprEvaluativePolarity.repr }

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprEvaluativePolarity.repr : EvaluativePolarity → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instDecidableEqEvaluativePolarity : DecidableEq EvaluativePolarity

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instDecidableEqEvaluativePolarity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instBEqEvaluativePolarity.beq : EvaluativePolarity → EvaluativePolarity → Bool

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instBEqEvaluativePolarity.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instBEqEvaluativePolarity : BEq EvaluativePolarity

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instBEqEvaluativePolarity = { beq := Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instBEqEvaluativePolarity.beq }

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.classifyAdj (entry : Semantics.Lexical.Adjective.GradableAdjEntry) : Bool

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.classifyAdj entry = match entry.antonymRelation with | some Core.NegationType.contrary => true | x => false

structure Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.Condition : Type

• adjective : Semantics.Lexical.Adjective.GradableAdjEntry
• strength : Semantics.Lexical.Adjective.InformationalStrength
• polarity : EvaluativePolarity
• negated : Bool

instance Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprCondition : Repr Condition

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprCondition = { reprPrec := Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprCondition.repr }

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprCondition.repr : Condition → ℕ → Std.Format

Equations

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

structure Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.AdjQuadruple : Type

• weakPos : Semantics.Lexical.Adjective.GradableAdjEntry
• weakNeg : Semantics.Lexical.Adjective.GradableAdjEntry
• strongPos : Semantics.Lexical.Adjective.GradableAdjEntry
• strongNeg : Semantics.Lexical.Adjective.GradableAdjEntry
• isRelative : Bool

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprAdjQuadruple.repr : AdjQuadruple → ℕ → Std.Format

Equations

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

instance Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprAdjQuadruple : Repr AdjQuadruple

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprAdjQuadruple = { reprPrec := Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.instReprAdjQuadruple.repr }

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.sizeQuad : AdjQuadruple

Equations

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

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.cleanlinessQuad : AdjQuadruple

Equations

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

@[reducible, inline]

abbrev Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.Deg5 : Type

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.Deg5 = Core.Scale.Degree 4

@[reducible, inline]

abbrev Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.Thr5 : Type

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.Thr5 = Core.Scale.Threshold 4

structure Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.RelativeScale : Type

• θ_pos : Thr5
• θ_neg : Thr5
• gap : self.θ_neg ≤ self.θ_pos

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.defaultRelativeScale : RelativeScale

Equations

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

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.notPositiveRel (d : Deg5) (s : RelativeScale) : Bool

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.notPositiveRel d s = decide (d ≤ { value := s.θ_pos.value.castSucc })

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.notNegativeRel (d : Deg5) (s : RelativeScale) : Bool

Equations

• Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.notNegativeRel d s = decide ({ value := s.θ_neg.value.castSucc } ≤ d)

The two-threshold model (Theory.lean) and single-threshold model (Core.lean) define comparison operators independently. These rfl proofs verify that the definitions agree — changing either module's definition body breaks them. This is the structural backbone connecting the study to shared infrastructure that @cite{tessler-franke-2019} also uses.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.positive'_eq_positiveMeaning {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Lexical.Adjective.ThresholdPair max) : Semantics.Lexical.Adjective.positiveMeaning' d tp = Semantics.Degree.positiveMeaning d tp.pos

Two-threshold positive IS single-threshold positive at θ_pos. Both compute (θ : Degree max) < d.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.contraryNeg_eq_negativeMeaning {max : ℕ} (d : Core.Scale.Degree max) (tp : Semantics.Lexical.Adjective.ThresholdPair max) : Semantics.Lexical.Adjective.contraryNegMeaning d tp = Semantics.Degree.negativeMeaning d tp.neg

Two-threshold contrary negative IS single-threshold negative at θ_neg. Both compute d < (θ : Degree max).

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.notPositiveRel_eq_antonymMeaning (d : Deg5) (s : RelativeScale) : notPositiveRel d s = Semantics.Degree.antonymMeaning d s.θ_pos

A&G's "not large" IS Core.lean's antonymMeaning at θ_pos. Both compute d ≤ (θ : Degree max).

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.contraryNeg_eq_negativeMeaning' {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Semantics.Lexical.Adjective.contraryNeg d θ = Semantics.Degree.negativeMeaning d θ

Theory.lean's contraryNeg IS Core.lean's negativeMeaning. Both compute d < (θ : Degree max).

For contrary antonyms (ThresholdPair), the scale partitions into three regions: positive, gap, and negative. The gap is WHERE "not positive" diverges from "negative" — the structural basis for polarity asymmetry.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.three_region_exhaustive {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) (d : Core.Scale.Degree max) : Semantics.Lexical.Adjective.positiveMeaning' d tp = true ∨ Semantics.Lexical.Adjective.inGapRegion d tp = true ∨ Semantics.Lexical.Adjective.contraryNegMeaning d tp = true

Every degree falls in at least one of {positive, gap, negative}.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.gap_not_positive {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) (d : Core.Scale.Degree max) (h : Semantics.Lexical.Adjective.inGapRegion d tp = true) : Semantics.Lexical.Adjective.positiveMeaning' d tp = false

Gap region excludes the positive region.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.gap_not_negative {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) (d : Core.Scale.Degree max) (h : Semantics.Lexical.Adjective.inGapRegion d tp = true) : Semantics.Lexical.Adjective.contraryNegMeaning d tp = false

Gap region excludes the negative region.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.gap_iff_neither {max : ℕ} (tp : Semantics.Lexical.Adjective.ThresholdPair max) (d : Core.Scale.Degree max) : Semantics.Lexical.Adjective.inGapRegion d tp = true ↔ Semantics.Lexical.Adjective.positiveMeaning' d tp = false ∧ Semantics.Lexical.Adjective.contraryNegMeaning d tp = false

Gap = "not positive" ∧ "not negative" (biconditional). Connects inGapRegion (Theory.lean) to positiveMeaning' and contraryNegMeaning (also Theory.lean, but equivalent to Core.lean by §3 equivalences).

For contradictory antonyms (single θ), positive and antonym are complements: every degree satisfies exactly one. No gap is possible. This is WHY absolute adjectives show symmetric negation (Exp 2).

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.contradictory_complement {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Semantics.Degree.positiveMeaning d θ = true ∨ Semantics.Degree.antonymMeaning d θ = true

Contradictory antonyms partition the scale with no gap. Now derived from Antonymy.contradictory_exhaustive.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.contradictory_is_complement {max : ℕ} (d : Core.Scale.Degree max) (θ : Core.Scale.Threshold max) : Semantics.Degree.antonymMeaning d θ = !Semantics.Degree.positiveMeaning d θ

antonymMeaning IS the Boolean complement of positiveMeaning. Now derived from Antonymy.contradictory_is_complement.

positiveMeaning_monotone (Core.lean): higher threshold → informationally stronger. This single theorem grounds BOTH: 1. Strong adjectives entail weak (gigantic → large) 2. Precision upshift entails standard (pristine-reading → clean-reading)

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.strong_entails_weak (θ_weak θ_strong : Thr5) (h_ord : θ_weak ≤ θ_strong) (d : Deg5) (h_strong : Semantics.Degree.positiveMeaning d θ_strong = true) : Semantics.Degree.positiveMeaning d θ_weak = true

Strong adjectives entail weak: anything above θ_strong is above θ_weak. Directly applies positiveMeaning_monotone from Core.lean.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.gigantic_entails_large : Semantics.Degree.positiveMeaning (Core.Scale.deg 4 ⋯) (Core.Scale.thr 2 ⋯) = true

Concrete: degree 4 is positive under the weak threshold (thr 2) BECAUSE it's positive under the strong threshold (thr 3) and monotonicity applies. This is a genuinely load-bearing proof: it chains Core.lean's monotonicity theorem through concrete threshold values.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.precision_entails_standard (d : Deg5) (h : Semantics.Degree.positiveMeaning d (Core.Scale.thr 3 ⋯) = true) : Semantics.Degree.positiveMeaning d (Core.Scale.thr 1 ⋯) = true

Precision upshift entails standard reading, by monotonicity. If d satisfies "clean" at pristine precision (θ = 3), it satisfies "clean" at standard precision (θ = 1). Same theorem, different reading.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.negative_strengthening : have s := defaultRelativeScale; have tp := { pos := s.θ_pos, neg := s.θ_neg, gap_exists := ⋯ }; notPositiveRel (Core.Scale.deg 0 ⋯) s = true ∧ Semantics.Lexical.Adjective.contraryNegMeaning (Core.Scale.deg 0 ⋯) tp = true

Exp 1: "not large" at degree 0 overlaps with "small" → negative strengthening.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.middling_reading : have s := defaultRelativeScale; have tp := { pos := s.θ_pos, neg := s.θ_neg, gap_exists := ⋯ }; notNegativeRel (Core.Scale.deg 2 ⋯) s = true ∧ Semantics.Lexical.Adjective.positiveMeaning' (Core.Scale.deg 2 ⋯) tp = false ∧ Semantics.Lexical.Adjective.contraryNegMeaning (Core.Scale.deg 2 ⋯) tp = false

Exp 1: "not small" at degree 2 is in the gap → middling reading.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.polarity_asymmetry : have s := defaultRelativeScale; have tp := { pos := s.θ_pos, neg := s.θ_neg, gap_exists := ⋯ }; (∃ (d : Deg5), notPositiveRel d s = true ∧ Semantics.Lexical.Adjective.contraryNegMeaning d tp = true) ∧ ∃ (d : Deg5), notNegativeRel d s = true ∧ Semantics.Lexical.Adjective.positiveMeaning' d tp = false ∧ Semantics.Lexical.Adjective.contraryNegMeaning d tp = false

Exp 1: Polarity asymmetry — strengthening witness AND middling witness.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.contrary_nonentailment : have s := defaultRelativeScale; have tp := { pos := s.θ_pos, neg := s.θ_neg, gap_exists := ⋯ }; (∃ (d : Deg5), notPositiveRel d s = true ∧ Semantics.Lexical.Adjective.contraryNegMeaning d tp = false) ∧ ∃ (d : Deg5), notNegativeRel d s = true ∧ Semantics.Lexical.Adjective.positiveMeaning' d tp = false

Exp 1: Gap witnesses contrary non-entailment (eqs. 6a-b).

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.strength_invariance : classifyAdj Fragments.English.Predicates.Adjectival.large = classifyAdj Fragments.English.Predicates.Adjectival.gigantic ∧ classifyAdj Fragments.English.Predicates.Adjectival.small = classifyAdj Fragments.English.Predicates.Adjectival.tiny

Exp 1: Strength invariance — gap depends on antonym type, not threshold.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.absolute_symmetric (d : Deg5) : Semantics.Degree.positiveMeaning d (Core.Scale.thr 2 ⋯) = true ∨ Semantics.Degree.antonymMeaning d (Core.Scale.thr 2 ⋯) = true

Exp 2: Absolute adjectives symmetric — contradictory_complement on Deg5.

"clean" in competition with "not clean" takes high-precision reading ≈ "pristine" (θ raised from 1 to 3). This creates a gap, explaining Table 7's relative-like behavior for absolutes. The entailment pristine-clean → standard-clean follows from positiveMeaning_monotone (§6).

def Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.precisionTP : Semantics.Lexical.Adjective.ThresholdPair 4

ThresholdPair for the precision-upshifted "clean" scale: θ_pos = 3 (pristine precision), θ_neg = 1 (filthy threshold).

Equations

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

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.precision_gap : Semantics.Lexical.Adjective.inGapRegion (Core.Scale.deg 2 ⋯) precisionTP = true

Precision upshift creates a gap at degree 2.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.precision_gap_is_neither : Semantics.Lexical.Adjective.positiveMeaning' (Core.Scale.deg 2 ⋯) precisionTP = false ∧ Semantics.Lexical.Adjective.contraryNegMeaning (Core.Scale.deg 2 ⋯) precisionTP = false

The precision gap is genuine: degree 2 satisfies neither positive (at pristine precision) nor negative. Uses gap_iff_neither from §4.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.precision_requires_shared_dimension : Fragments.English.Predicates.Adjectival.pristine.dimension = Fragments.English.Predicates.Adjectival.clean.dimension

Precision requires shared dimension: "clean" can take "pristine" precision because they measure the same thing.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.relative_adjs_contrary : Fragments.English.Predicates.Adjectival.large.antonymRelation = some Core.NegationType.contrary ∧ Fragments.English.Predicates.Adjectival.small.antonymRelation = some Core.NegationType.contrary ∧ Fragments.English.Predicates.Adjectival.gigantic.antonymRelation = some Core.NegationType.contrary ∧ Fragments.English.Predicates.Adjectival.tiny.antonymRelation = some Core.NegationType.contrary

Fragment entries determine gap/no-gap classification.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.absolute_weak_contradictory : Fragments.English.Predicates.Adjectival.clean.antonymRelation = some Core.NegationType.contradictory ∧ Fragments.English.Predicates.Adjectival.dirty.antonymRelation = some Core.NegationType.contradictory

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.absolute_strong_contrary : Fragments.English.Predicates.Adjectival.pristine.antonymRelation = some Core.NegationType.contrary ∧ Fragments.English.Predicates.Adjectival.filthy.antonymRelation = some Core.NegationType.contrary

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.classify_agrees_with_fragment : classifyAdj Fragments.English.Predicates.Adjectival.large = true ∧ classifyAdj Fragments.English.Predicates.Adjectival.small = true ∧ classifyAdj Fragments.English.Predicates.Adjectival.clean = false ∧ classifyAdj Fragments.English.Predicates.Adjectival.dirty = false ∧ classifyAdj Fragments.English.Predicates.Adjectival.pristine = true ∧ classifyAdj Fragments.English.Predicates.Adjectival.filthy = true

Gap classification agrees with fragment for ALL study entries.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.size_same_dimension : Fragments.English.Predicates.Adjectival.large.dimension = Fragments.English.Predicates.Adjectival.small.dimension ∧ Fragments.English.Predicates.Adjectival.large.dimension = Fragments.English.Predicates.Adjectival.gigantic.dimension ∧ Fragments.English.Predicates.Adjectival.large.dimension = Fragments.English.Predicates.Adjectival.tiny.dimension

Size quadruple shares a dimension.

theorem Phenomena.Gradability.Studies.AlexandropoulouGotzner2024.cleanliness_same_dimension : Fragments.English.Predicates.Adjectival.clean.dimension = Fragments.English.Predicates.Adjectival.dirty.dimension ∧ Fragments.English.Predicates.Adjectival.clean.dimension = Fragments.English.Predicates.Adjectival.pristine.dimension ∧ Fragments.English.Predicates.Adjectival.clean.dimension = Fragments.English.Predicates.Adjectival.filthy.dimension

Cleanliness quadruple shares a dimension.