Degree Achievements

[KL08]

[KL08] show that degree achievements (rust, cool, widen, increase) have variable telicity determined by the boundedness of the underlying adjectival scale:

• Closed-scale adjectives (clean, full, straight) → telic degree achievements
• Open-scale adjectives (long, wide, cool) → atelic degree achievements

A degree achievement V derived from adjective A has a measure of change function mΔ(e) = d(result(e)) - d(init(e)) on A's scale. Telicity = whether mΔ is bounded: if A's scale has a maximum, mΔ is bounded → telic (accomplishment); if A's scale is open, mΔ is unbounded → atelic (activity).

This module derives VendlerClass from Boundedness, connecting to the existing LicensingPipeline infrastructure in Core/Scales/Scale.lean.

structure Features.DegreeAchievement.DegreeAchievementScale : Type

A degree achievement's base scale structure.

The key claim: the telicity of a degree achievement verb is determined by the boundedness of the scale inherited from the base adjective. Scales with a maximum (closed, upper-bounded) yield telic VPs; scales without a maximum (open, lower-bounded) yield atelic VPs.

• dimension : Semantics.Gradability.Dimension

  The scalar dimension the base adjective measures. Its boundedness is the order-mixin profile of the dimension's degree type, recovered by the derived scaleBoundedness below — not stored.

• baseAdjective : Option String

  Citation form of the base adjective (if deadjectival).

def Features.DegreeAchievement.instReprDegreeAchievementScale.repr : DegreeAchievementScale → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Features.DegreeAchievement.instReprDegreeAchievementScale : Repr DegreeAchievementScale

Equations

• Features.DegreeAchievement.instReprDegreeAchievementScale = { reprPrec := Features.DegreeAchievement.instReprDegreeAchievementScale.repr }

def Features.DegreeAchievement.instBEqDegreeAchievementScale.beq : DegreeAchievementScale → DegreeAchievementScale → Bool

Equations

• Features.DegreeAchievement.instBEqDegreeAchievementScale.beq { dimension := a, baseAdjective := a_1 } { dimension := b, baseAdjective := b_1 } = (a == b && a_1 == b_1)
• Features.DegreeAchievement.instBEqDegreeAchievementScale.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Features.DegreeAchievement.instBEqDegreeAchievementScale : BEq DegreeAchievementScale

Equations

• Features.DegreeAchievement.instBEqDegreeAchievementScale = { beq := Features.DegreeAchievement.instBEqDegreeAchievementScale.beq }

def Features.DegreeAchievement.DegreeAchievementScale.scaleBoundedness (s : DegreeAchievementScale) : Core.Order.Boundedness

The base scale's boundedness, as a derived view of the dimension (the scale's shape is read off the dimension's order structure, not stored per verb).

Equations

• s.scaleBoundedness = s.dimension.boundedness

@[implicit_reducible]

instance Features.DegreeAchievement.instInhabitedDegreeAchievementScale : Inhabited DegreeAchievementScale

Equations

• Features.DegreeAchievement.instInhabitedDegreeAchievementScale = { default := { dimension := Semantics.Gradability.Dimension.unspecified } }

def Features.DegreeAchievement.DegreeAchievementScale.defaultTelicity (s : DegreeAchievementScale) : Telicity

Derive default telicity from scale boundedness — the central claim of [KL08]. Scales with a maximum → telic; scales without → atelic.

Delegates to Dimension.defaultTelicity — a scale with a maximal degree gives a telic verb — grounded to the order mixin by Semantics.Gradability.Dimension.defaultTelicity_telic_iff_hasGreatest.

Equations

• s.defaultTelicity = s.dimension.defaultTelicity

def Features.DegreeAchievement.DegreeAchievementScale.defaultVendlerClass (s : DegreeAchievementScale) : VendlerClass

Default Vendler class, delegating to Dimension.defaultVendlerClass: closed scale → accomplishment, open → activity.

Equations

• s.defaultVendlerClass = s.dimension.defaultVendlerClass

theorem Features.DegreeAchievement.closed_dimension_telic (a : Option String) : { dimension := Semantics.Gradability.Dimension.straightness, baseAdjective := a }.defaultTelicity = Telicity.telic

A closed dimension (e.g. straightness) → telic.

theorem Features.DegreeAchievement.open_dimension_atelic (a : Option String) : { dimension := Semantics.Gradability.Dimension.width, baseAdjective := a }.defaultTelicity = Telicity.atelic

An open dimension (e.g. width) → atelic.

theorem Features.DegreeAchievement.closed_dimension_accomplishment (a : Option String) : { dimension := Semantics.Gradability.Dimension.straightness, baseAdjective := a }.defaultVendlerClass = VendlerClass.accomplishment

A closed dimension → accomplishment.

theorem Features.DegreeAchievement.open_dimension_activity (a : Option String) : { dimension := Semantics.Gradability.Dimension.width, baseAdjective := a }.defaultVendlerClass = VendlerClass.activity

An open dimension → activity.

theorem Features.DegreeAchievement.default_vendler_is_dynamic (s : DegreeAchievementScale) : s.defaultVendlerClass = VendlerClass.accomplishment ∨ s.defaultVendlerClass = VendlerClass.activity

defaultVendlerClass always returns.accomplishment or.activity — degree achievements are always dynamic and durative.

theorem Features.DegreeAchievement.telicity_vendler_agree (s : DegreeAchievementScale) : s.defaultVendlerClass.telicity = s.defaultTelicity

defaultTelicity agrees with the telicity of defaultVendlerClass.

@[implicit_reducible]

instance Features.DegreeAchievement.instLicensingPipelineDegreeAchievementScale : Core.Order.LicensingPipeline DegreeAchievementScale

LicensingPipeline instance: a degree-achievement scale's boundedness is its dimension's (a derived view, no stored flag).

Equations

• Features.DegreeAchievement.instLicensingPipelineDegreeAchievementScale = { toBoundedness := fun (s : Features.DegreeAchievement.DegreeAchievementScale) => s.scaleBoundedness }