The Parameter of Aspect (2nd ed.)

@cite{smith-1997}

Formalizes Smith's two-component theory of aspect: aspectual meaning = situation type × viewpoint aspect, independently combined.

What this file exercises

• Temporal schemata per situation type (Ch. 2)
• Viewpoint visibility properties (§4.1): what each viewpoint makes visible
• Neutral viewpoint (§4.2.3): default for LVM sentences
• Independence theorem (§4.3): situation type × viewpoint freely combine
• Cross-linguistic viewpoint parameters (§4.2): language-specific inventories
• Compositional rules bridge (§3.3): connects to Composition.lean

What lives elsewhere

• Situation type classification (VendlerClass): Features/Aktionsart.lean
• Viewpoint operators (IMPF, PRFV, INIT_OVERLAP): Core.lean
• VP-level composition rules: Composition.lean
• Aspectual diagnostics: Diagnostics.lean

Smith Ch. 2: each situation type has a characteristic temporal schema defining its internal temporal structure.

- States: (I)——(F)          unbounded, no internal stages
- Activities: I......F_Arb  arbitrary final point, internal stages
- Accomplishments: I.....F_Nat R  natural final point + result
- Semelfactives: E          single instantaneous stage
- Achievements: ...E_R...   instantaneous + result state

We encode the structural properties of each schema. 

def Smith1997.hasNaturalEndpoint (c : Features.VendlerClass) : Bool

Whether the situation type has a natural (non-arbitrary) final point. Telic types have natural endpoints; atelic types don't. This is exactly the telicity feature, named for Smith's terminology.

Note: hasNaturalEndpoint coincides extensionally with hasResultState in our 3-feature system (both reduce to telicity), but the concepts differ in Smith's presentation: a natural endpoint is a property of the temporal schema's boundary structure, while a result state is the post-final-point stage (the built house, the won race). We retain hasNaturalEndpoint as the primary predicate and derive result-state presence from it via resultState_iff_naturalEndpoint.

Equations

• Smith1997.hasNaturalEndpoint c = (c.telicity == Features.Telicity.telic)

def Smith1997.hasInternalStages (c : Features.VendlerClass) : Bool

Whether the situation type has internal stages (intervals of change). Dynamic + durative types have internal stages; states and punctuals don't. Smith Ch. 4: the progressive focuses internal stages, so types without them resist the progressive.

Equations

• Smith1997.hasInternalStages c = (c.dynamicity == Features.Dynamicity.dynamic && c.duration == Features.Duration.durative)

def Smith1997.hasPreliminaryStages (c : Features.VendlerClass) : Bool

Whether the situation type has detachable preliminary stages that the imperfective can focus independently of the event itself.

Smith §4.2.2 (p. 75): achievements have preliminary stages — processes leading to the instantaneous change ("The team was reaching the top" presents preliminary stages, not the reaching itself). Semelfactives, also instantaneous, do NOT have preliminary stages and never appear with imperfectives focusing a preliminary interval.

Accomplishments also have process stages, but these are non-detachable: the process IS the event (building a house). The imperfective focuses internal stages of the event proper, not separate preliminary stages. This detachability distinction is why hasPreliminaryStages is true only for achievements.

Equations

• Smith1997.hasPreliminaryStages c = (c == Features.VendlerClass.achievement)

theorem Smith1997.activity_schema : hasInternalStages Features.VendlerClass.activity = true ∧ hasNaturalEndpoint Features.VendlerClass.activity = false

Activities have internal stages but no natural endpoint.

theorem Smith1997.accomplishment_schema : hasInternalStages Features.VendlerClass.accomplishment = true ∧ hasNaturalEndpoint Features.VendlerClass.accomplishment = true

Accomplishments have internal stages AND a natural endpoint.

theorem Smith1997.semelfactive_schema : hasInternalStages Features.VendlerClass.semelfactive = false ∧ hasNaturalEndpoint Features.VendlerClass.semelfactive = false ∧ hasPreliminaryStages Features.VendlerClass.semelfactive = false

Semelfactives: single stage, no internal structure, no endpoint, no preliminary stages. Contrasts with achievements on all three schema properties despite sharing [−durative].

theorem Smith1997.achievement_schema : hasInternalStages Features.VendlerClass.achievement = false ∧ hasNaturalEndpoint Features.VendlerClass.achievement = true ∧ hasPreliminaryStages Features.VendlerClass.achievement = true

Achievements: instantaneous with natural endpoint, and detachable preliminary stages that the imperfective can focus.

theorem Smith1997.state_schema : hasInternalStages Features.VendlerClass.state = false ∧ hasNaturalEndpoint Features.VendlerClass.state = false

States: no internal stages, no natural endpoint.

theorem Smith1997.resultState_iff_naturalEndpoint (c : Features.VendlerClass) : hasNaturalEndpoint c = (c.telicity == Features.Telicity.telic)

Result states coincide with natural endpoints in the 3-feature system. Both reduce to telicity. Conceptually distinct in Smith's presentation (endpoint = schema boundary, result = post-final stage), but our feature decomposition doesn't distinguish them — both are consequences of [+telic].

Smith §4.1: viewpoints differ in what they make visible.

| Viewpoint     | Initial pt | Internal stages | Final pt |
|---------------|------------|----------------|----------|
| Perfective    | visible    | visible        | visible  |
| Imperfective  | not vis.   | visible        | not vis. |
| Neutral       | visible    | ≥1 stage       | open     |

The neutral viewpoint is informationally between perfective
and imperfective: it always includes I (like perfective) but
F may or may not be visible (unlike either). 

def Smith1997.showsInitialPoint : Semantics.Aspect.Core.ViewpointType → Bool

Whether the viewpoint makes the initial point visible.

Equations

• Smith1997.showsInitialPoint Semantics.Aspect.Core.ViewpointType.perfective = true
• Smith1997.showsInitialPoint Semantics.Aspect.Core.ViewpointType.imperfective = false
• Smith1997.showsInitialPoint Semantics.Aspect.Core.ViewpointType.neutral = true
• Smith1997.showsInitialPoint Semantics.Aspect.Core.ViewpointType.perfect = false
• Smith1997.showsInitialPoint Semantics.Aspect.Core.ViewpointType.prospective = false

def Smith1997.showsFinalPoint : Semantics.Aspect.Core.ViewpointType → Bool

Whether the viewpoint makes the final point visible (asserted).

Equations

• Smith1997.showsFinalPoint Semantics.Aspect.Core.ViewpointType.perfective = true
• Smith1997.showsFinalPoint Semantics.Aspect.Core.ViewpointType.imperfective = false
• Smith1997.showsFinalPoint Semantics.Aspect.Core.ViewpointType.neutral = false
• Smith1997.showsFinalPoint Semantics.Aspect.Core.ViewpointType.perfect = false
• Smith1997.showsFinalPoint Semantics.Aspect.Core.ViewpointType.prospective = false

def Smith1997.isClosed : Semantics.Aspect.Core.ViewpointType → Prop

Whether the viewpoint presents a closed (completed) situation.

Equations

• Smith1997.isClosed Semantics.Aspect.Core.ViewpointType.perfective = True
• Smith1997.isClosed Semantics.Aspect.Core.ViewpointType.imperfective = False
• Smith1997.isClosed Semantics.Aspect.Core.ViewpointType.neutral = False
• Smith1997.isClosed Semantics.Aspect.Core.ViewpointType.perfect = True
• Smith1997.isClosed Semantics.Aspect.Core.ViewpointType.prospective = False

@[implicit_reducible]

instance Smith1997.instDecidablePredViewpointTypeIsClosed : DecidablePred isClosed

Equations

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

theorem Smith1997.perfective_closed : showsInitialPoint Semantics.Aspect.Core.ViewpointType.perfective = true ∧ showsFinalPoint Semantics.Aspect.Core.ViewpointType.perfective = true ∧ isClosed Semantics.Aspect.Core.ViewpointType.perfective

Perfective is informationally closed: both I and F visible.

theorem Smith1997.imperfective_open : showsInitialPoint Semantics.Aspect.Core.ViewpointType.imperfective = false ∧ showsFinalPoint Semantics.Aspect.Core.ViewpointType.imperfective = false ∧ ¬isClosed Semantics.Aspect.Core.ViewpointType.imperfective

Imperfective is informationally open: neither I nor F visible.

theorem Smith1997.neutral_intermediate : showsInitialPoint Semantics.Aspect.Core.ViewpointType.neutral = true ∧ showsFinalPoint Semantics.Aspect.Core.ViewpointType.neutral = false ∧ ¬isClosed Semantics.Aspect.Core.ViewpointType.neutral

Neutral includes I but not necessarily F — intermediate informativity.

def Smith1997.focusesPreliminaryStages : Semantics.Aspect.Core.ViewpointType → Bool

Whether the viewpoint can focus preliminary stages of an event. @cite{smith-1997} §4.2.2 (p. 75): imperfective viewpoints may focus preliminary stages of achievements ("The team was reaching the top"). §4.2.3 (p. 80): neutral viewpoints do NOT focus preliminary stages — this is a key discriminator between neutral and imperfective.

French Futur achievements cannot conjoin with assertions that the event didn't occur (p. 80, ex. 41): # "La guerre éclaira mais elle n'éclaira pas." Unlike imperfectives, which can present preliminary stages without entailing the event occurs.

Perfective viewpoints don't focus preliminary stages either — they present the event as a whole (or closed).

Equations

• Smith1997.focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.imperfective = true
• Smith1997.focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.perfective = false
• Smith1997.focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.neutral = false
• Smith1997.focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.perfect = false
• Smith1997.focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.prospective = false

theorem Smith1997.neutral_no_preliminary_stages : focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.neutral = false ∧ focusesPreliminaryStages Semantics.Aspect.Core.ViewpointType.imperfective = true

Neutral viewpoints do not focus preliminary stages, unlike imperfectives. This is the key discrimination: "La guerre éclaira" (neutral/Futur) does NOT have the preliminary reading available to "La guerre était en train d'éclater" (imperfective).

theorem Smith1997.neutral_between_perf_imperf : showsInitialPoint Semantics.Aspect.Core.ViewpointType.neutral = showsInitialPoint Semantics.Aspect.Core.ViewpointType.perfective ∧ showsFinalPoint Semantics.Aspect.Core.ViewpointType.neutral = showsFinalPoint Semantics.Aspect.Core.ViewpointType.imperfective

The neutral viewpoint is strictly between perfective and imperfective in informativity: it shows I (like perfective, unlike imperfective) but doesn't assert F (like imperfective, unlike perfective).

Smith §4.3: the two components of aspectual meaning are independent. Any situation type can combine with any viewpoint. The 5 × 4 product is freely generated — there are no gaps.

This is the core structural claim of the two-component theory. We
verify it by showing that `ViewpointType` and `VendlerClass` are
independently enumerable and that each combination is distinct. 

structure Smith1997.AspectualInterpretation : Type

An aspectual interpretation: the combination of situation type and viewpoint. This is the "two-component" structure.

• situationType : Features.VendlerClass
• viewpoint : Semantics.Aspect.Core.ViewpointType

@[implicit_reducible]

instance Smith1997.instDecidableEqAspectualInterpretation : DecidableEq AspectualInterpretation

Equations

• Smith1997.instDecidableEqAspectualInterpretation = Smith1997.instDecidableEqAspectualInterpretation.decEq

def Smith1997.instDecidableEqAspectualInterpretation.decEq (x✝ x✝¹ : AspectualInterpretation) : Decidable (x✝ = x✝¹)

Equations

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

def Smith1997.instReprAspectualInterpretation.repr : AspectualInterpretation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Smith1997.instReprAspectualInterpretation : Repr AspectualInterpretation

Equations

• Smith1997.instReprAspectualInterpretation = { reprPrec := Smith1997.instReprAspectualInterpretation.repr }

def Smith1997.allSitTypes : List Features.VendlerClass

All 20 combinations of situation type × viewpoint.

Equations

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

def Smith1997.allViewpoints : List Semantics.Aspect.Core.ViewpointType

Equations

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

def Smith1997.allInterpretations : List AspectualInterpretation

Equations

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

theorem Smith1997.independence_free_generation : allInterpretations.length = 25

The product is freely generated: 25 distinct combinations.

theorem Smith1997.independence_no_duplicates : allInterpretations.Nodup

No duplicates in the product — all combinations are distinct.

Smith §4.2: languages differ in their viewpoint inventories. Three parameters: 1. Which viewpoints are available 2. Which is the default (dominant) viewpoint 3. Whether/how statives participate in the perfective system

These parameters are the "parameter of aspect" — the locus of
cross-linguistic variation within the universal two-component theory. 

inductive Smith1997.PerfStativeParam : Type

How the perfective viewpoint interacts with statives. @cite{smith-1997} pp. 69-70 identifies three cross-linguistic patterns:

• closed: perfective covers statives with a closed interpretation (French: "Marie a vécu à Paris" — asserts the situation is over)
• open: perfective appears with stative verb constellations but allows both open and closed readings (English: "Jennifer knew Turkish" — she may or may not still know it)
• excluded: perfective does not apply to statives at all (Russian, Chinese, Navajo — no perfective stative sentences)

• closed : PerfStativeParam
• open : PerfStativeParam
• excluded : PerfStativeParam

@[implicit_reducible]

instance Smith1997.instDecidableEqPerfStativeParam : DecidableEq PerfStativeParam

Equations

• Smith1997.instDecidableEqPerfStativeParam x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Smith1997.instReprPerfStativeParam : Repr PerfStativeParam

Equations

• Smith1997.instReprPerfStativeParam = { reprPrec := Smith1997.instReprPerfStativeParam.repr }

def Smith1997.instReprPerfStativeParam.repr : PerfStativeParam → ℕ → Std.Format

Equations

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

structure Smith1997.AspectualSystem : Type

A language's aspectual system parameters.

• language : String

  Language name

• viewpoints : List Semantics.Aspect.Core.ViewpointType

  Available viewpoint types

• defaultViewpoint : Semantics.Aspect.Core.ViewpointType

  Default viewpoint for aspectually vague sentences

• perfStativeParam : PerfStativeParam

  How the perfective interacts with statives

def Smith1997.instReprAspectualSystem.repr : AspectualSystem → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Smith1997.instReprAspectualSystem : Repr AspectualSystem

Equations

• Smith1997.instReprAspectualSystem = { reprPrec := Smith1997.instReprAspectualSystem.repr }

def Smith1997.english : AspectualSystem

English: perfective + imperfective (progressive); no neutral; perfective with statives allows open or closed readings (@cite{smith-1997} p. 70: "Jennifer knew Turkish" — she may still know it or may have forgotten).

Equations

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

def Smith1997.french : AspectualSystem

French: perfective + imperfective + neutral (Futur); perfective covers statives with closed reading (@cite{smith-1997} p. 70: "Marie a vécu à Paris" — asserts the situation is over; # "Marie a vécu à Paris et elle y vit encore").

Equations

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

def Smith1997.mandarin : AspectualSystem

Mandarin: perfective (-le) + imperfective (zai, -zhe) + neutral (bare); perfective does NOT apply to statives.

Equations

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

def Smith1997.navajo : AspectualSystem

Navajo: perfective + imperfective + neutral (Usitative/Iterative); perfective does NOT apply to statives.

Equations

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

theorem Smith1997.universal_core : ([english, french, mandarin, navajo].all fun (sys : AspectualSystem) => sys.viewpoints.contains Semantics.Aspect.Core.ViewpointType.perfective && sys.viewpoints.contains Semantics.Aspect.Core.ViewpointType.imperfective) = true

All four languages have at least perfective and imperfective.

theorem Smith1997.neutral_in_lvm_languages : french.viewpoints.contains Semantics.Aspect.Core.ViewpointType.neutral = true ∧ mandarin.viewpoints.contains Semantics.Aspect.Core.ViewpointType.neutral = true ∧ navajo.viewpoints.contains Semantics.Aspect.Core.ViewpointType.neutral = true

The neutral viewpoint appears in languages with LVM sentences.

theorem Smith1997.english_no_neutral : english.viewpoints.contains Semantics.Aspect.Core.ViewpointType.neutral = false

English lacks the neutral viewpoint.

theorem Smith1997.three_perf_stative_patterns : english.perfStativeParam = PerfStativeParam.open ∧ french.perfStativeParam = PerfStativeParam.closed ∧ mandarin.perfStativeParam = PerfStativeParam.excluded ∧ navajo.perfStativeParam = PerfStativeParam.excluded

The three perfective-stative patterns are all distinct.

Smith's viewpoint inventories and the WALS typological profiles (Typology.lean) describe the same languages at different levels: Smith identifies which viewpoints a language has; WALS records whether the perfective/imperfective distinction is grammaticalized.

All four Smith languages grammaticalize this distinction (WALS Ch 65
= `.grammatical`), which is consistent with their viewpoint inventories
containing both `.perfective` and `.imperfective`. 

theorem Smith1997.smith_languages_have_wals_aspect : Fragments.English.tenseAspectProfile.aspect = Typology.AspectMarking.grammatical ∧ Fragments.French.tenseAspectProfile.aspect = Typology.AspectMarking.grammatical ∧ Fragments.Mandarin.tenseAspectProfile.aspect = Typology.AspectMarking.grammatical

Languages in Smith's sample all have grammaticalized aspect in WALS. This is expected: Smith's viewpoint inventory presupposes the perfective/imperfective contrast is grammatically expressed.

theorem Smith1997.french_neutral_has_inflectional_future : french.viewpoints.contains Semantics.Aspect.Core.ViewpointType.neutral = true ∧ Fragments.French.tenseAspectProfile.future = Typology.FutureMarking.inflectional

Smith's French has the neutral viewpoint (Futur); WALS French has inflectional future — consistent, since the Futur is the morphological expression of the neutral viewpoint.

Smith Ch. 4: although the components are independent, their interaction produces predictable interpretive effects.

def Smith1997.imperfectiveParadoxArises (ai : AspectualInterpretation) : Bool

The imperfective paradox arises exactly when the viewpoint is imperfective and the situation type is telic. "Mary was walking to school" does not entail "Mary walked to school". The paradox doesn't arise for atelic types (activities, states) because their subinterval property makes IMPF entail PRFV.

Equations

• Smith1997.imperfectiveParadoxArises ai = (ai.viewpoint == Semantics.Aspect.Core.ViewpointType.imperfective && ai.situationType.telicity == Features.Telicity.telic)

theorem Smith1997.paradox_impf_accomplishment : imperfectiveParadoxArises { situationType := Features.VendlerClass.accomplishment, viewpoint := Semantics.Aspect.Core.ViewpointType.imperfective } = true

The paradox arises for imperfective accomplishments.

theorem Smith1997.no_paradox_impf_activity : imperfectiveParadoxArises { situationType := Features.VendlerClass.activity, viewpoint := Semantics.Aspect.Core.ViewpointType.imperfective } = false

The paradox does not arise for imperfective activities.

theorem Smith1997.no_paradox_perfective (c : Features.VendlerClass) : imperfectiveParadoxArises { situationType := c, viewpoint := Semantics.Aspect.Core.ViewpointType.perfective } = false

The paradox never arises with perfective viewpoint.

inductive Smith1997.PerfectiveEffect : Type

Whether the perfective conveys completion (reaching the natural endpoint) or merely termination (stopping). @cite{smith-1997} pp. 67-68: "The Activity sentence conveys termination (Lily stopped swimming) whereas the Accomplishment conveys completion (Mrs Ramsey finished the letter)."

• Perfective + telic → completion (the endpoint was reached)
• Perfective + atelic → termination (the event stopped)
• Non-perfective viewpoints don't assert either

• completion : PerfectiveEffect
• termination : PerfectiveEffect
• noEffect : PerfectiveEffect

@[implicit_reducible]

instance Smith1997.instDecidableEqPerfectiveEffect : DecidableEq PerfectiveEffect

Equations

• Smith1997.instDecidableEqPerfectiveEffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Smith1997.instReprPerfectiveEffect : Repr PerfectiveEffect

Equations

• Smith1997.instReprPerfectiveEffect = { reprPrec := Smith1997.instReprPerfectiveEffect.repr }

def Smith1997.instReprPerfectiveEffect.repr : PerfectiveEffect → ℕ → Std.Format

Equations

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

def Smith1997.perfectiveEffect (ai : AspectualInterpretation) : PerfectiveEffect

Determine the perfective effect from an aspectual interpretation.

Equations

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

theorem Smith1997.perf_accomplishment_completes : perfectiveEffect { situationType := Features.VendlerClass.accomplishment, viewpoint := Semantics.Aspect.Core.ViewpointType.perfective } = PerfectiveEffect.completion

Perfective accomplishments convey completion. "Mrs Ramsey wrote a letter" → she finished it (# "she didn't finish it").

theorem Smith1997.perf_activity_terminates : perfectiveEffect { situationType := Features.VendlerClass.activity, viewpoint := Semantics.Aspect.Core.ViewpointType.perfective } = PerfectiveEffect.termination

Perfective activities convey termination, not completion. "Lily swam in the pond" → she stopped swimming (not completed swimming).

theorem Smith1997.perf_achievement_completes : perfectiveEffect { situationType := Features.VendlerClass.achievement, viewpoint := Semantics.Aspect.Core.ViewpointType.perfective } = PerfectiveEffect.completion

Perfective achievements convey completion (instantaneous endpoint).

theorem Smith1997.impf_no_completion_termination (c : Features.VendlerClass) : perfectiveEffect { situationType := c, viewpoint := Semantics.Aspect.Core.ViewpointType.imperfective } = PerfectiveEffect.noEffect

Imperfective viewpoints don't assert completion or termination.

theorem Smith1997.completion_iff_telic (c : Features.VendlerClass) : perfectiveEffect { situationType := c, viewpoint := Semantics.Aspect.Core.ViewpointType.perfective } = PerfectiveEffect.completion ↔ c.telicity = Features.Telicity.telic

Completion vs termination tracks telicity exactly: telic situations complete, atelic situations merely terminate.

theorem Smith1997.progressive_requires_stages (c : Features.VendlerClass) : Phenomena.TenseAspect.Diagnostics.progressivePrediction c = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.accept ↔ hasInternalStages c = true

Progressive requires internal stages (durative + dynamic). This is derived from the feature decomposition, not stipulated per class — connecting to progressive_from_features in Diagnostics.lean.

Connect Smith's compositional rules (§3.3) to Composition.lean and verify against Smith's examples.

theorem Smith1997.external_override_is_final (v : Features.AspectualProfile) (np : MassCount) (ext : Features.Telicity) : (Semantics.Aspect.Composition.overrideTelicity (Semantics.Aspect.Composition.composeWithNP v np) ext).telicity = ext

Smith's external override (§3.2.5) is idempotent and absorbs prior composition — the override is the final word.

theorem Smith1997.krifka_smith_agreement : (Semantics.Aspect.Composition.composeWithNP Features.accomplishmentProfile MassCount.count).telicity = Features.Telicity.telic ∧ (Semantics.Aspect.Composition.composeWithNP Features.accomplishmentProfile MassCount.mass).telicity = Features.Telicity.atelic

The count/mass distinction in NPs tracks cumulativity/quantization: count NPs are quantized (QUA), mass NPs are cumulative (CUM). This connects Smith's compositional rules to Krifka's mereological telicity theory via the bridge in Events/CEM.lean.

• V[+Telic] + NP[+Count/QUA] → VCon[+Telic] (telic preserved)
• V[+Telic] + NP[-Count/CUM] → VCon[-Telic] (atelicized)

These are the same predictions as eat_two_apples_telic and eat_apples_atelic in Krifka1998.lean.

theorem Smith1997.semelfactive_coercion_three_ways : Features.semelfactiveProfile.duratize.toVendlerClass = Features.VendlerClass.activity ∧ (Semantics.Aspect.Composition.overrideDuration Features.semelfactiveProfile Features.Duration.durative).toVendlerClass = Features.VendlerClass.activity ∧ Phenomena.TenseAspect.Diagnostics.forXPrediction Features.VendlerClass.semelfactive = Phenomena.TenseAspect.Diagnostics.DiagnosticResult.coerced

Semelfactive coercion under duration is compositionally derived: VCon[+Dyn, -Tel, -Dur] + [+Dur] → DVCon[+Dyn, -Tel, +Dur] = Activity. This matches duratize_semelfactive in Features/Aktionsart.lean and semelfactive_durative_is_activity in Composition.lean.

theorem Smith1997.hasNaturalEndpoint_iff_telic_to_qua (c : Features.VendlerClass) : hasNaturalEndpoint c = true ↔ c.telicity.toMereoTag = Core.Scale.MereoTag.qua

Smith's hasNaturalEndpoint is extensionally equivalent to K89's QUA-via-MereoTag. Both formalisms derive telicity from incomparable primitives — Smith from Vendler-class feature decomposition (telicity ∈ {telic, atelic}), K89 from algebraic mereology (MereoTag.qua/.cum) — but agree on the four-way Vendler partition. This one-line bridge makes the cross-framework agreement visible at the type level (round-2 cross-framework audit found that Phenomena/TenseAspect/Studies/Krifka1989.lean was running on a parallel track without an explicit Smith ↔ K89 connection).