inductive Semantics.Lexical.Verb.EventStructure.Template : Type

Canonical event structure templates. The first four are from @cite{rappaport-hovav-levin-1998}. motionContact is from @cite{rappaport-hovav-levin-2024} for the sweep/rub/scrape class: [x MOVE y] WHILE [x CONTACT y].

• state : Template
• activity : Template
• achievement : Template
• accomplishment : Template
• motionContact : Template

instance Semantics.Lexical.Verb.EventStructure.instDecidableEqTemplate : DecidableEq Template

Equations

• Semantics.Lexical.Verb.EventStructure.instDecidableEqTemplate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.EventStructure.instReprTemplate.repr : Template → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.EventStructure.instReprTemplate : Repr Template

Equations

• Semantics.Lexical.Verb.EventStructure.instReprTemplate = { reprPrec := Semantics.Lexical.Verb.EventStructure.instReprTemplate.repr }

instance Semantics.Lexical.Verb.EventStructure.instBEqTemplate : BEq Template

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqTemplate = { beq := Semantics.Lexical.Verb.EventStructure.instBEqTemplate.beq }

def Semantics.Lexical.Verb.EventStructure.instBEqTemplate.beq : Template → Template → Bool

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqTemplate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Verb.EventStructure.Template.hasCause : Template → Bool

Does the template involve CAUSE?

Equations

• Semantics.Lexical.Verb.EventStructure.Template.accomplishment.hasCause = true
• x✝.hasCause = false

def Semantics.Lexical.Verb.EventStructure.Template.hasExternalCauser : Template → Bool

Does the template have an external causer position?

Equations

• Semantics.Lexical.Verb.EventStructure.Template.accomplishment.hasExternalCauser = true
• x✝.hasExternalCauser = false

def Semantics.Lexical.Verb.EventStructure.Template.predicateCount : Template → ℕ

How many grammatically relevant predicates?

Equations

• Semantics.Lexical.Verb.EventStructure.Template.state.predicateCount = 1
• Semantics.Lexical.Verb.EventStructure.Template.activity.predicateCount = 1
• Semantics.Lexical.Verb.EventStructure.Template.achievement.predicateCount = 1
• Semantics.Lexical.Verb.EventStructure.Template.accomplishment.predicateCount = 2
• Semantics.Lexical.Verb.EventStructure.Template.motionContact.predicateCount = 2

def Semantics.Lexical.Verb.EventStructure.Template.toAspectualProfile : Template → Tense.Aspect.LexicalAspect.AspectualProfile

Predicted aspectual profile for each template.

Equations

• Semantics.Lexical.Verb.EventStructure.Template.state.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.stateProfile
• Semantics.Lexical.Verb.EventStructure.Template.activity.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.activityProfile
• Semantics.Lexical.Verb.EventStructure.Template.achievement.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.achievementProfile
• Semantics.Lexical.Verb.EventStructure.Template.accomplishment.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.accomplishmentProfile
• Semantics.Lexical.Verb.EventStructure.Template.motionContact.toAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.activityProfile

def Semantics.Lexical.Verb.EventStructure.Template.vendlerClass (t : Template) : Tense.Aspect.LexicalAspect.VendlerClass

Predicted Vendler class for each template (derived from profile).

Equations

• t.vendlerClass = t.toAspectualProfile.toVendlerClass

Templates with complex internal structure — multiple sub-events connected by CAUSE or embedding BECOME — license scopal ambiguities that mono-eventive templates do not.

At the template level, three diagnostics from @cite{dowty-1979} reduce
to two structural properties already defined above:

1. ***again*/*re-* ambiguity** tracks `hasResultState`: templates
   embedding [BECOME [STATE]] allow restitutive readings where a
   scopal modifier targets just the result sub-event.
2. **Negation over CAUSE** (@cite{koontz-garboden-2009}) tracks
   `hasCause`: negation can scope narrowly over CAUSE, denying
   the causal link while maintaining the result.
3. **"By itself" licensing** (@cite{koontz-garboden-2009}) also tracks
   `hasCause`: "without outside help" requires CAUSE in the meaning.

@cite{krejci-2012}'s insight is that some verbs assigned simpler templates
(eat, wash, dress, learn) nonetheless pass all three diagnostics — evidence
that they have bieventive, causative event structures in their simple forms.
This verb-level property is captured in `RootTypology` and `ArgDerivation`,
not at the template level here. 

def Semantics.Lexical.Verb.EventStructure.Template.hasResultState : Template → Bool

Does the template embed a result state under BECOME? Templates with [BECOME [STATE]] have a sub-event boundary that scopal modifiers (again, re-, almost) can target independently.

Equations

• Semantics.Lexical.Verb.EventStructure.Template.achievement.hasResultState = true
• Semantics.Lexical.Verb.EventStructure.Template.accomplishment.hasResultState = true
• x✝.hasResultState = false

theorem Semantics.Lexical.Verb.EventStructure.cause_implies_resultState (t : Template) : t.hasCause = true → t.hasResultState = true

CAUSE implies a result state (accomplishment embeds BECOME).

Causative/Inchoative Alternation

The accomplishment template [[x ACT] CAUSE [BECOME [y STATE]]]
has an intransitive variant: the achievement [BECOME [x STATE]],
obtained by stripping the external cause. This is the
event-structural core of the causative/inchoative alternation
(@cite{krejci-2012}; @cite{rappaport-hovav-levin-1998}).

Whether the intransitive variant is *monoeventive* (true
anticausative) or *bieventive* (reflexive, with coidentification
of causer and causee) is a language- and verb-specific property
formalized in `MorphologicalCausation.IntransitivizationType`. 

def Semantics.Lexical.Verb.EventStructure.Template.intransitiveVariant : Template → Option Template

The intransitive variant of a template, stripping the external cause. Only accomplishments have an alternation partner.

Equations

• Semantics.Lexical.Verb.EventStructure.Template.accomplishment.intransitiveVariant = some Semantics.Lexical.Verb.EventStructure.Template.achievement
• x✝.intransitiveVariant = none

theorem Semantics.Lexical.Verb.EventStructure.intransitive_has_resultState (t t' : Template) : t.intransitiveVariant = some t' → t'.hasResultState = true

The intransitive variant retains the result state (BECOME STATE survives stripping of ACT CAUSE).

theorem Semantics.Lexical.Verb.EventStructure.intransitive_no_cause (t t' : Template) : t.intransitiveVariant = some t' → t'.hasCause = false

The intransitive variant loses CAUSE.

theorem Semantics.Lexical.Verb.EventStructure.only_accomplishment_alternates (t : Template) : t.intransitiveVariant.isSome = true → t = Template.accomplishment

Only accomplishments have an intransitive variant (only templates with CAUSE can undergo the alternation).

def Semantics.Lexical.Verb.EventStructure.Template.subjectProfile : Template → EntailmentProfile.EntailmentProfile

Predicted subject entailment profile for each template.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Verb.EventStructure.Template.motionContact.subjectProfile = Semantics.Lexical.Verb.EntailmentProfile.sweepBasicSubjectProfile

def Semantics.Lexical.Verb.EventStructure.Template.objectProfile : Template → Option EntailmentProfile.EntailmentProfile

Predicted object entailment profile (if any).

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Lexical.Verb.EventStructure.Template.state.objectProfile = none
• Semantics.Lexical.Verb.EventStructure.Template.activity.objectProfile = none
• Semantics.Lexical.Verb.EventStructure.Template.achievement.objectProfile = none

theorem Semantics.Lexical.Verb.EventStructure.accomplishment_subject_is_agent : Template.accomplishment.subjectProfile.pAgentScore = 5

Accomplishment subject is a full agent (5 P-Agent entailments).

theorem Semantics.Lexical.Verb.EventStructure.motionContact_variable_agentivity : Template.motionContact.subjectProfile = EntailmentProfile.sweepBasicSubjectProfile

motionContact subject has the same profile as basic sweep (movement + IE, underspecified for agentivity).

inductive Semantics.Lexical.Verb.EventStructure.DeterminingPredicate : Type

For motionContact verbs, which sub-predicate determines argument realization (@cite{rappaport-hovav-levin-2024} §3.3–3.4).

• motion : DeterminingPredicate
• contact : DeterminingPredicate

instance Semantics.Lexical.Verb.EventStructure.instDecidableEqDeterminingPredicate : DecidableEq DeterminingPredicate

Equations

• Semantics.Lexical.Verb.EventStructure.instDecidableEqDeterminingPredicate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.EventStructure.instReprDeterminingPredicate.repr : DeterminingPredicate → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Verb.EventStructure.instReprDeterminingPredicate : Repr DeterminingPredicate

Equations

• Semantics.Lexical.Verb.EventStructure.instReprDeterminingPredicate = { reprPrec := Semantics.Lexical.Verb.EventStructure.instReprDeterminingPredicate.repr }

def Semantics.Lexical.Verb.EventStructure.instBEqDeterminingPredicate.beq : DeterminingPredicate → DeterminingPredicate → Bool

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqDeterminingPredicate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.EventStructure.instBEqDeterminingPredicate : BEq DeterminingPredicate

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqDeterminingPredicate = { beq := Semantics.Lexical.Verb.EventStructure.instBEqDeterminingPredicate.beq }

theorem Semantics.Lexical.Verb.EventStructure.contact_determines_implies_effector_subject : EntailmentProfile.isEffector Template.motionContact.subjectProfile = true

When CONTACT determines argument realization, the subject is an effector (movement + IE → external argument). This yields the simple transitive frame: "The wind swept the deck".

theorem Semantics.Lexical.Verb.EventStructure.motionContact_object_is_forceRecipient : ∃ (p : EntailmentProfile.EntailmentProfile), Template.motionContact.objectProfile = some p ∧ EntailmentProfile.isForceRecipient p = true

The motionContact object profile exists and is a force recipient.

def Semantics.Lexical.Verb.EventStructure.Template.lexicalizeInstrument : Template → EntailmentProfile.EntailmentProfile

Instrument lexicalization adds agentivity to a template by restricting the moving entity to a specific instrument, forcing volition + sentience

• causation. The result is the broom-sweep subject profile.

Equations

• Semantics.Lexical.Verb.EventStructure.Template.motionContact.lexicalizeInstrument = Semantics.Lexical.Verb.EntailmentProfile.sweepBroomSubjectProfile
• x✝.lexicalizeInstrument = x✝.subjectProfile

theorem Semantics.Lexical.Verb.EventStructure.lexicalize_increases_agentivity : Template.motionContact.lexicalizeInstrument.pAgentScore > Template.motionContact.subjectProfile.pAgentScore

Instrument lexicalization strictly increases agentivity for motionContact templates (@cite{rappaport-hovav-levin-2024} §3.5: broom-sweep is more agentive than basic sweep).

theorem Semantics.Lexical.Verb.EventStructure.lexicalized_is_full_agent : Template.motionContact.lexicalizeInstrument.pAgentScore = 5

Lexicalized motionContact has full proto-agent profile (5 entailments).

Levin classes map to event structure templates via meaning components. The core correspondence (@cite{rappaport-hovav-levin-1998} §3; @cite{rappaport-hovav-levin-2010} §2):

| Meaning component pattern | Template | Example class |
|---|---|---|
| CoS + causation | accomplishment | break (45.1), destroy (44) |
| CoS, no causation | achievement | appear (48.1), calve (28) |
| No CoS, no motion | state | exist (47.1), admire (31.2) |
| Otherwise | activity | hit (18.1), run (51.3) |

The `motionContact` template is specific to the sweep/rub/scrape
class and requires a class-specific override. 

inductive Semantics.Lexical.Verb.EventStructure.EventType : Type

The fundamental binary distinction in event types: whether a predicate encodes a process (PROC only) or a state change (involves CHANGE).

This crosscuts Vendler's four-way classification: degree achievements are Vendler activities or accomplishments depending on scale boundedness but are event-structurally state-change predicates (@cite{bohnemeyer-2004} §5).

@cite{bohnemeyer-2004} argues this is the primary semantic distinction governing verb classification in Yukatek Maya — more fundamental than Vendler classes for predicting argument linking and transitivization.

• process : EventType
• stateChange : EventType

instance Semantics.Lexical.Verb.EventStructure.instDecidableEqEventType : DecidableEq EventType

Equations

• Semantics.Lexical.Verb.EventStructure.instDecidableEqEventType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Verb.EventStructure.instBEqEventType : BEq EventType

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqEventType = { beq := Semantics.Lexical.Verb.EventStructure.instBEqEventType.beq }

def Semantics.Lexical.Verb.EventStructure.instBEqEventType.beq : EventType → EventType → Bool

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqEventType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.EventStructure.instReprEventType : Repr EventType

Equations

• Semantics.Lexical.Verb.EventStructure.instReprEventType = { reprPrec := Semantics.Lexical.Verb.EventStructure.instReprEventType.repr }

def Semantics.Lexical.Verb.EventStructure.instReprEventType.repr : EventType → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Verb.EventStructure.Template.eventType : Template → EventType

Derive event type from template. Activities and motionContact are processes; states, achievements, and accomplishments involve state change.

Equations

• Semantics.Lexical.Verb.EventStructure.Template.activity.eventType = Semantics.Lexical.Verb.EventStructure.EventType.process
• Semantics.Lexical.Verb.EventStructure.Template.motionContact.eventType = Semantics.Lexical.Verb.EventStructure.EventType.process
• x✝.eventType = Semantics.Lexical.Verb.EventStructure.EventType.stateChange

inductive Semantics.Lexical.Verb.EventStructure.CausationType : Type

Whether a process is internally caused — the event is instigated by a participant — or externally caused — occurring "spontaneously" without an instigator.

This is a per-verb property of the ROOT, not of the template. Two activity verbs can differ: sing (internal) vs roll (external).

@cite{levin-hovav-1995} §4; @cite{bohnemeyer-2004} §2,6.

• internal : CausationType
• external : CausationType

instance Semantics.Lexical.Verb.EventStructure.instDecidableEqCausationType : DecidableEq CausationType

Equations

• Semantics.Lexical.Verb.EventStructure.instDecidableEqCausationType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Lexical.Verb.EventStructure.instBEqCausationType.beq : CausationType → CausationType → Bool

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqCausationType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Verb.EventStructure.instBEqCausationType : BEq CausationType

Equations

• Semantics.Lexical.Verb.EventStructure.instBEqCausationType = { beq := Semantics.Lexical.Verb.EventStructure.instBEqCausationType.beq }

instance Semantics.Lexical.Verb.EventStructure.instReprCausationType : Repr CausationType

Equations

• Semantics.Lexical.Verb.EventStructure.instReprCausationType = { reprPrec := Semantics.Lexical.Verb.EventStructure.instReprCausationType.repr }

def Semantics.Lexical.Verb.EventStructure.instReprCausationType.repr : CausationType → ℕ → Std.Format

Equations

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

def MeaningComponents.predictedTemplate : MeaningComponents → Semantics.Lexical.Verb.EventStructure.Template

Predicted event structure template from meaning components.

Equations

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

def LevinClass.eventTemplate : LevinClass → Semantics.Lexical.Verb.EventStructure.Template

Predicted template for a Levin class, with class-specific overrides.

Equations

• LevinClass.wipe.eventTemplate = Semantics.Lexical.Verb.EventStructure.Template.motionContact
• x✝.eventTemplate = x✝.meaningComponents.predictedTemplate

Verification: canonical quadruple

theorem Semantics.Lexical.Verb.EventStructure.break_is_accomplishment : LevinClass.break_.eventTemplate = Template.accomplishment

Break → accomplishment (CoS + causation → [ACT CAUSE BECOME]).

theorem Semantics.Lexical.Verb.EventStructure.hit_is_activity : LevinClass.hit.eventTemplate = Template.activity

Hit → activity (contact + motion, no CoS → [ACT]).

theorem Semantics.Lexical.Verb.EventStructure.touch_is_activity : LevinClass.touch.eventTemplate = Template.activity

Touch → activity (contact only, no CoS).

theorem Semantics.Lexical.Verb.EventStructure.cut_is_accomplishment : LevinClass.cut.eventTemplate = Template.accomplishment

Cut → accomplishment (CoS + causation).

Change-of-state classes → accomplishment

theorem Semantics.Lexical.Verb.EventStructure.cos_classes_accomplishment : LevinClass.break_.eventTemplate = Template.accomplishment ∧ LevinClass.bend.eventTemplate = Template.accomplishment ∧ LevinClass.cooking.eventTemplate = Template.accomplishment ∧ LevinClass.otherCoS.eventTemplate = Template.accomplishment ∧ LevinClass.destroy.eventTemplate = Template.accomplishment

All §45 CoS classes map to accomplishment.

Motion classes → activity

theorem Semantics.Lexical.Verb.EventStructure.motion_is_activity : LevinClass.mannerOfMotion.eventTemplate = Template.activity ∧ LevinClass.inherentlyDirectedMotion.eventTemplate = Template.activity

Motion verbs are activities (no CoS, have motion).

Stative classes → state

theorem Semantics.Lexical.Verb.EventStructure.stative_classes_state : LevinClass.exist.eventTemplate = Template.state ∧ LevinClass.admire.eventTemplate = Template.state ∧ LevinClass.want.eventTemplate = Template.state

Perception/psych statives map to state template.

Achievement classes

theorem Semantics.Lexical.Verb.EventStructure.appear_is_achievement : LevinClass.appear.eventTemplate = Template.achievement

Appear (CoS without causation) → achievement.

theorem Semantics.Lexical.Verb.EventStructure.calve_is_achievement : LevinClass.calve.eventTemplate = Template.achievement

Calve (CoS without causation) → achievement.

Special: motionContact

theorem Semantics.Lexical.Verb.EventStructure.wipe_is_motionContact : LevinClass.wipe.eventTemplate = Template.motionContact

Wipe class → motionContact (class-specific override).

Template → aspectual class consistency

theorem Semantics.Lexical.Verb.EventStructure.break_telic : LevinClass.break_.eventTemplate.vendlerClass = Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Accomplishment classes (break, cut) are predicted telic.

theorem Semantics.Lexical.Verb.EventStructure.hit_atelic : LevinClass.hit.eventTemplate.vendlerClass = Tense.Aspect.LexicalAspect.VendlerClass.activity

Activity classes (hit, run) are predicted atelic.

theorem Semantics.Lexical.Verb.EventStructure.exist_stative : LevinClass.exist.eventTemplate.vendlerClass = Tense.Aspect.LexicalAspect.VendlerClass.state

State classes (exist, admire) are predicted stative.