Gradable adjectives

Adjective-specific degree semantics, layered on the syntactic Adjective (Syntax/Category/Adjective): the GradableAdjective lexeme with its derived Kennedy classification, the two-threshold model for contrary antonyms, multidimensional binding ([Sas13]), and the bridge from a concrete Degree scale to the abstract PolarMeasure.

Main definitions

• GradableAdjective — a syntactic Adjective refined with the degree-semantic layer; scaleType, standard, and adjectiveClass are derived views.
• ThresholdPair — the two thresholds of a contrary antonym pair, with a gap.
• InformationalStrength — the weak/strong distinction ([AG24a]).
• DimensionBindingType — how a multidimensional adjective binds its dimensions.
• adjMeasure — a GradableAdjective read as a PolarMeasure over a scale.

Core degree types (Degree, Threshold) live in Core.MeasurementScale; the threshold semantics (positiveMeaning, negativeMeaning) in Semantics/Degree/Basic. The intersective/subsective/privative classification lives in Semantics/Modification/Classification.lean.

Standards and Interpretive Economy ([Ken07])

Absorbed from the retired Standard.lean: the classification of gradable adjectives by scale structure and the derivation of standard type from boundedness. Interpretive Economy ([Ken07] eq. (66)) maximises the contribution of conventional meaning: a scale with an endpoint rules out the contextual standard; a totally closed scale admits both endpoint standards (ieAdmits) with the maximum as the pragmatically preferred default (interpretiveEconomy).

Classification carriers

inductive Degree.PositiveStandard : Type

Positive form standard: how the contextual threshold is determined. For open scales, the standard is the contextual norm ([Ken07]); for closed scales, it is the relevant endpoint fixed by Interpretive Economy.

• contextual : PositiveStandard

  Open-scale: θ = norm relative to comparison class.

• minEndpoint : PositiveStandard

  Lower-bounded: θ = minimum (e.g., "bent", "wet").

• maxEndpoint : PositiveStandard

  Upper-bounded / closed: θ = maximum (e.g., "full", "dry").

• functional : PositiveStandard

  Necessity standard: θ = minimum value for pursuit ([Bel25]).

@[implicit_reducible]

instance Degree.instDecidableEqPositiveStandard : DecidableEq PositiveStandard

Equations

• Degree.instDecidableEqPositiveStandard x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Degree.instReprPositiveStandard : Repr PositiveStandard

Equations

• Degree.instReprPositiveStandard = { reprPrec := Degree.instReprPositiveStandard.repr }

def Degree.instReprPositiveStandard.repr : PositiveStandard → ℕ → Std.Format

Equations

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

def Degree.PositiveStandard.RequiresComparisonClass : PositiveStandard → Prop

Whether the positive standard depends on contextual domain information.

[Ken07] argues the comparison class is not a semantic argument of pos (contra [Kle80]), replacing it with the standard-fixing function s: ⟦pos⟧ = λg.λx. g(x) ≥ s(g). For relative (open-scale) adjectives, s still requires contextual domain information; for absolute (closed-scale) adjectives the standard comes from scale endpoints via Interpretive Economy.

Equations

• Degree.PositiveStandard.contextual.RequiresComparisonClass = True
• Degree.PositiveStandard.minEndpoint.RequiresComparisonClass = False
• Degree.PositiveStandard.maxEndpoint.RequiresComparisonClass = False
• Degree.PositiveStandard.functional.RequiresComparisonClass = True

@[implicit_reducible]

instance Degree.instDecidablePredPositiveStandardRequiresComparisonClass : DecidablePred PositiveStandard.RequiresComparisonClass

Equations

• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.contextual = isTrue Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_1
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.minEndpoint = isFalse Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_2
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.maxEndpoint = isFalse Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_3
• Degree.instDecidablePredPositiveStandardRequiresComparisonClass Degree.PositiveStandard.functional = isTrue Degree.instDecidablePredPositiveStandardRequiresComparisonClass._proof_4

inductive Degree.AdjectiveClass : Type

Kennedy's adjective classification by scale structure and standard type [Ken07] [KMcN05], plus a nonGradable case for adjectives outside the degree-based fragment.

• relativeGradable : AdjectiveClass

  Standard varies with comparison class — tall, expensive, big.

• absoluteMaximum : AdjectiveClass

  Threshold fixed at scale maximum — full, straight, closed, dry.

• absoluteMinimum : AdjectiveClass

  Threshold fixed at scale minimum — wet, bent, open, dirty.

• mildlyPositive : AdjectiveClass

  Necessity-relative threshold — decent, acceptable ([Bel25]).

• nonGradable : AdjectiveClass

  Non-gradable: no degree argument, no scale — atomic, prime, deceased, pregnant. Outside the gradable (PolarMeasure) system; consumers that classify a general adjective should map non-gradables here rather than coercing them into a gradable class.

def Degree.instReprAdjectiveClass.repr : AdjectiveClass → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instReprAdjectiveClass : Repr AdjectiveClass

Equations

• Degree.instReprAdjectiveClass = { reprPrec := Degree.instReprAdjectiveClass.repr }

@[implicit_reducible]

instance Degree.instDecidableEqAdjectiveClass : DecidableEq AdjectiveClass

Equations

• Degree.instDecidableEqAdjectiveClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Degree.AdjectiveClass.IsRelative (c : AdjectiveClass) : Prop

Coarse two-way classification: relative vs absolute. Collapses absoluteMaximum and absoluteMinimum.

Equations

• c.IsRelative = (c = Degree.AdjectiveClass.relativeGradable)

@[implicit_reducible]

instance Degree.instDecidablePredAdjectiveClassIsRelative : DecidablePred AdjectiveClass.IsRelative

Equations

• Degree.instDecidablePredAdjectiveClassIsRelative c = decEq c Degree.AdjectiveClass.relativeGradable

def Degree.ieAdmits : Core.Order.Boundedness → PositiveStandard → Prop

The positive-form standards that Interpretive Economy admits for a scale. IE maximises the contribution of conventional (scalar) meaning, so the contextual/relative standard is admitted only on a totally open scale (which has no endpoint to use). A one-sided closed scale admits its single endpoint; a totally closed scale admits both endpoint standards — IE rules out the relative reading but is silent on the min/max choice ([Ken07] eq. (66), the opaque/transparent and open/exposed cases of eq. (67)–(68)).

Equations

• Degree.ieAdmits Core.Order.Boundedness.open_ x✝ = (x✝ = Degree.PositiveStandard.contextual)
• Degree.ieAdmits Core.Order.Boundedness.lowerBounded x✝ = (x✝ = Degree.PositiveStandard.minEndpoint)
• Degree.ieAdmits Core.Order.Boundedness.upperBounded x✝ = (x✝ = Degree.PositiveStandard.maxEndpoint)
• Degree.ieAdmits Core.Order.Boundedness.closed x✝ = (x✝ = Degree.PositiveStandard.minEndpoint ∨ x✝ = Degree.PositiveStandard.maxEndpoint)

@[implicit_reducible]

instance Degree.instDecidableIeAdmits (b : Core.Order.Boundedness) (s : PositiveStandard) : Decidable (ieAdmits b s)

Equations

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

def Degree.interpretiveEconomy : Core.Order.Boundedness → PositiveStandard

The out-of-context default positive standard. Where Interpretive Economy admits a unique standard (open / one-sided closed scales) this is forced; for a totally closed scale IE admits both endpoints (ieAdmits) and the default is the maximum on pragmatic grounds — a maximum standard entails a minimum one and stronger meanings are preferred ([Ken07] eq. (66) discussion). So this is Interpretive Economy plus a strengthening default for closed scales, not IE alone; the genuine (variable) IE claim is ieAdmits.

Equations

• Degree.interpretiveEconomy Core.Order.Boundedness.open_ = Degree.PositiveStandard.contextual
• Degree.interpretiveEconomy Core.Order.Boundedness.lowerBounded = Degree.PositiveStandard.minEndpoint
• Degree.interpretiveEconomy Core.Order.Boundedness.upperBounded = Degree.PositiveStandard.maxEndpoint
• Degree.interpretiveEconomy Core.Order.Boundedness.closed = Degree.PositiveStandard.maxEndpoint

theorem Degree.interpretiveEconomy_open : interpretiveEconomy Core.Order.Boundedness.open_ = PositiveStandard.contextual

theorem Degree.interpretiveEconomy_lowerBounded : interpretiveEconomy Core.Order.Boundedness.lowerBounded = PositiveStandard.minEndpoint

theorem Degree.interpretiveEconomy_upperBounded : interpretiveEconomy Core.Order.Boundedness.upperBounded = PositiveStandard.maxEndpoint

theorem Degree.interpretiveEconomy_closed : interpretiveEconomy Core.Order.Boundedness.closed = PositiveStandard.maxEndpoint

The default standard for a totally closed scale is the maximum — a pragmatic preference (stronger meaning), not an Interpretive-Economy determination; the minimum is equally admitted (ieAdmits_closed_minEndpoint).

theorem Degree.ieAdmits_interpretiveEconomy (b : Core.Order.Boundedness) : ieAdmits b (interpretiveEconomy b)

The default standard is always among those Interpretive Economy admits.

theorem Degree.ieAdmits_closed_minEndpoint : ieAdmits Core.Order.Boundedness.closed PositiveStandard.minEndpoint

Interpretive variability of totally closed scales: IE admits the minimum standard, so the interpretiveEconomy maximum default is a pragmatic preference, not a semantic determination ([Ken07] eq. (67)–(68): opaque/transparent, open/exposed).

theorem Degree.ieAdmits_closed_maxEndpoint : ieAdmits Core.Order.Boundedness.closed PositiveStandard.maxEndpoint

A totally closed scale also admits the maximum standard.

theorem Degree.not_ieAdmits_contextual_of_isLicensed {b : Core.Order.Boundedness} (h : b.IsLicensed) : ¬ieAdmits b PositiveStandard.contextual

Interpretive Economy rules out the relative (contextual) standard whenever the scale has an endpoint (Boundedness.IsLicensed).

def Degree.IsClassA (b : Core.Order.Boundedness) : Prop

A boundedness is Class A (relative) iff its default standard requires a comparison class — i.e. iff the scale is open. Kennedy's tall, expensive, big.

Equations

• Degree.IsClassA b = (Degree.interpretiveEconomy b).RequiresComparisonClass

@[implicit_reducible]

instance Degree.instDecidablePredBoundednessIsClassA : DecidablePred IsClassA

Equations

• Degree.instDecidablePredBoundednessIsClassA b = Degree.instDecidablePredBoundednessIsClassA._aux_1 b

Two-threshold model for contrary antonyms

structure Degree.ThresholdPair (max : ℕ) : Type

The two thresholds of a contrary antonym pair (happy/unhappy): pos for the positive form (true when degree > pos) and neg for the negative form (true when degree < neg). When neg < pos a gap region [neg, pos] — "neither" — lies between them; that strict inequality is taken as a hypothesis where a gap is needed (contrary_gap_exists, gap_nonempty), not stored as an invariant.

• pos : Threshold max
• neg : Threshold max

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

Equations

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

@[implicit_reducible]

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

Equations

• Degree.instReprThresholdPair = { reprPrec := Degree.instReprThresholdPair.repr }

@[implicit_reducible]

instance Degree.instDecidableEqThresholdPair {max✝ : ℕ} : DecidableEq (ThresholdPair max✝)

Equations

• Degree.instDecidableEqThresholdPair = Degree.instDecidableEqThresholdPair.decEq

def Degree.instDecidableEqThresholdPair.decEq {max✝ : ℕ} (x✝ x✝¹ : ThresholdPair max✝) : Decidable (x✝ = x✝¹)

Equations

• Degree.instDecidableEqThresholdPair.decEq { pos := a, neg := a_1 } { pos := b, neg := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Degree.instBEqThresholdPair.beq {max✝ : ℕ} : ThresholdPair max✝ → ThresholdPair max✝ → Bool

Equations

• Degree.instBEqThresholdPair.beq { pos := a, neg := a_1 } { pos := b, neg := b_1 } = (a == b && a_1 == b_1)
• Degree.instBEqThresholdPair.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Degree.instBEqThresholdPair {max✝ : ℕ} : BEq (ThresholdPair max✝)

Equations

• Degree.instBEqThresholdPair = { beq := Degree.instBEqThresholdPair.beq }

Negation semantics

The two-threshold model for contrary antonyms: the general threshold semantics of Semantics/Degree/Basic (positiveMeaning/negativeMeaning/notPositiveMeaning) read through a ThresholdPair's two poles.

@[reducible, inline]

abbrev Degree.contradictoryNeg {max : ℕ} (d : Bounded max) (θ : Threshold max) : Prop

Contradictory negation not happy — d ≤ θ (Degree.notPositiveMeaning).

Equations

• Degree.contradictoryNeg d θ = Degree.notPositiveMeaning d θ

@[reducible, inline]

abbrev Degree.contraryNeg {max : ℕ} (d : Bounded max) (θ_neg : Threshold max) : Prop

Contrary negation unhappy — d < θ_neg (Degree.negativeMeaning).

Equations

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

@[reducible, inline]

abbrev Degree.inGapRegion {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

The gap region: d is neither positive nor negative (neg ≤ d ≤ pos).

Equations

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

@[reducible, inline]

abbrev Degree.positiveMeaning' {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

Positive form happy at the pair's upper threshold — d > pos.

Equations

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

@[reducible, inline]

abbrev Degree.contraryNegMeaning {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

Negative form unhappy at the pair's lower threshold — d < neg.

Equations

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

@[reducible, inline]

abbrev Degree.notContraryNegMeaning {max : ℕ} (d : Bounded max) (tp : ThresholdPair max) : Prop

not unhappy — the complement of the negative form (neg ≤ d).

Equations

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

Antonym relations

@[reducible, inline]

abbrev Degree.AntonymRelation : Type

The relation between a positive form and its antonym.

Equations

• Degree.AntonymRelation = Features.NegationType

Informational strength

inductive Degree.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: [AG24a], [Hor72]

• weak : InformationalStrength
• strong : InformationalStrength

def Degree.instReprInformationalStrength.repr : InformationalStrength → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instReprInformationalStrength : Repr InformationalStrength

Equations

• Degree.instReprInformationalStrength = { reprPrec := Degree.instReprInformationalStrength.repr }

@[implicit_reducible]

instance Degree.instDecidableEqInformationalStrength : DecidableEq InformationalStrength

Equations

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

The gradable adjective

inductive Degree.SpatialConfigType : Type

Spatial configuration type for adjectives in resultative constructions ([Lev26]). Only adjectives describing spatially instantiated states license intr-push open resultatives.

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

@[implicit_reducible]

instance Degree.instDecidableEqSpatialConfigType : DecidableEq SpatialConfigType

Equations

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

@[implicit_reducible]

instance Degree.instReprSpatialConfigType : Repr SpatialConfigType

Equations

• Degree.instReprSpatialConfigType = { reprPrec := Degree.instReprSpatialConfigType.repr }

def Degree.instReprSpatialConfigType.repr : SpatialConfigType → ℕ → Std.Format

Equations

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

structure Degree.GradableAdjectiveextends Adjective : Type

A gradable adjective: the syntactic Adjective (Syntax/Category/Adjective) refined with the degree-semantic layer that becomes relevant in this module — the Kennedy standardOverride, and the lexical-semantic facets antonymRelation, resultative spatialConfigType ([Lev26]), and evaluativeValence ([Nou24]). The scale shape (scaleType), positive standard, and Kennedy adjectiveClass are derived views below — the fix for the old stored scaleType that conflated scale shape with pole (wet/dry share one closed .wetness scale, differing only in pole).

• form : String
• script : Option String
• dimension : Option Features.ScalarDimension
• isLowerEndpoint : Bool
• comparison : ComparisonFacet
• antonymForm : Option String
• standardOverride : Option PositiveStandard

  Override the Kennedy default standard (the good/MPA residual: an open-shape scale that nonetheless takes a functional/contextual standard, [Bel25]). none = take the derived default.

• antonymRelation : Option AntonymRelation

  Lexical antonym's logical relation (contrary vs contradictory).

• spatialConfigType : Option SpatialConfigType

  Resultative spatial-configuration class ([Lev26]).

• evaluativeValence : Option Features.EvaluativeValence

  Evaluative valence of the adjective, when applicable. Determines intensifier degree class ([Nou24]): negative-evaluative bases yield H-degree intensifiers, positive-evaluative bases yield M-degree intensifiers.

def Degree.instReprGradableAdjective.repr : GradableAdjective → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instReprGradableAdjective : Repr GradableAdjective

Equations

• Degree.instReprGradableAdjective = { reprPrec := Degree.instReprGradableAdjective.repr }

def Degree.GradableAdjective.scaleType (g : GradableAdjective) : Core.Order.Boundedness

The scale's intrinsic shape — read off the dimension key, not stored (.open_ for a non-gradable, which has no scale).

Equations

• g.scaleType = (Option.map Features.ScalarDimension.boundedness g.dimension).getD Core.Order.Boundedness.open_

def Degree.GradableAdjective.standard (g : GradableAdjective) : PositiveStandard

The effective positive standard: the default from (scale shape, pole), overridable by standardOverride. This is the quantity the old scaleType field conflated — it separates wet (closed + lower ⇒ min) from dry (closed + upper ⇒ max), and lets good (open shape) take a contextual standard rather than a bogus bound. ([Ken07]'s Interpretive Economy on the open/singly-bounded cases.)

Equations

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

theorem Degree.GradableAdjective.standard_ieAdmits (g : GradableAdjective) (h : g.standardOverride = none) : ieAdmits g.scaleType g.standard

The entry-level selection implements the type-level theory: an override-free entry's derived standard is always among the standards Interpretive Economy admits for its scale shape. The closed-scale pole dispatch (min for lower-endpoint, max otherwise) picks within IE's admitted pair rather than beyond it.

def Degree.GradableAdjective.adjectiveClass (g : GradableAdjective) : AdjectiveClass

Kennedy's adjective class — derived from standard, not stored; .nonGradable exactly when there is no dimension ([Ken07], [KMcN05]).

Equations

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

def Degree.GradableAdjective.IsRelative (g : GradableAdjective) : Prop

Comparison-class dependence — the relative/absolute distinction, derived.

Equations

• g.IsRelative = g.adjectiveClass.IsRelative

@[implicit_reducible]

instance Degree.GradableAdjective.instDecidableIsRelative (g : GradableAdjective) : Decidable g.IsRelative

Equations

• g.instDecidableIsRelative = id inferInstance

Multidimensional adjectives ([Sas13])

inductive Degree.DimensionBindingType : Type

How a multidimensional adjective binds its dimensions ([Sas13]).

• 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

@[implicit_reducible]

instance Degree.instReprDimensionBindingType : Repr DimensionBindingType

Equations

• Degree.instReprDimensionBindingType = { reprPrec := Degree.instReprDimensionBindingType.repr }

def Degree.instReprDimensionBindingType.repr : DimensionBindingType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Degree.instDecidableEqDimensionBindingType : DecidableEq DimensionBindingType

Equations

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

def Degree.conjunctiveBinding {α : Type u_1} (dims : List (α → Bool)) (x : α) : Bool

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

Equations

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

def Degree.disjunctiveBinding {α : Type u_1} (dims : List (α → Bool)) (x : α) : Bool

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

Equations

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

theorem Degree.deMorgan_conjunctive_disjunctive {α : Type u_1} (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 [Sas13]'s Hypothesis 2 — under a negation theory of antonymy, if the positive form is conjunctive, the negative antonym (its negation) is disjunctive.

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

def Degree.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

• Degree.DimensionBindingType.conjunctive.negate = Degree.DimensionBindingType.disjunctive
• Degree.DimensionBindingType.disjunctive.negate = Degree.DimensionBindingType.conjunctive
• Degree.DimensionBindingType.mixed.negate = Degree.DimensionBindingType.mixed

theorem Degree.negate_involutive (b : DimensionBindingType) : b.negate.negate = b

def Degree.predictedBinding : PositiveStandard → DimensionBindingType

[Sas13] Hypothesis 3: standard type predicts binding type. Total (max standard) → conjunctive, partial (min standard) → disjunctive, relative (contextual) → mixed.

Equations

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

Degree–PolarMeasure bridge

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

def Degree.adjMeasure {max : ℕ} {W : Type u_1} (μ : W → Bounded max) (entry : GradableAdjective) : PolarMeasure (Bounded max) W

Equations

• Degree.adjMeasure μ entry = Degree.PolarMeasure.adjective μ entry.scaleType

theorem Degree.closedAdj_licensed {max : ℕ} {W : Type u_1} (μ : W → Bounded max) (entry : GradableAdjective) (h : entry.scaleType = Core.Order.Boundedness.closed) : (adjMeasure μ entry).IsLicensed

theorem Degree.openAdj_blocked {max : ℕ} {W : Type u_1} (μ : W → Bounded max) (entry : GradableAdjective) (h : entry.scaleType = Core.Order.Boundedness.open_) : ¬(adjMeasure μ entry).IsLicensed

theorem Degree.degree_measure_is_id {max : ℕ} {W : Type u_1} (μ : W → Bounded max) : (PolarMeasure.numeral μ).μ = μ