Quality Dimensions for Verb Root Content

@cite{dowty-1991} @cite{fillmore-atkins-2000} @cite{hale-keyser-1987} @cite{levin-1993} @cite{talmy-1988} @cite{talmy-2000}

Empirically attested feature dimensions for characterizing the idiosyncratic ("root") content of verb meanings. Verbs within a single class (e.g., Levin's 45.1 Break Verbs) share event structure but may differ along these dimensions in ways that affect selectional restrictions, figurative extensions, and cross-linguistic translation equivalence (Spalek & McNally, forthcoming).

Three-level architecture

Level 1 — Levin meaning components (§ 1). Binary features that define verb classes, diagnosed by diathesis alternation behavior. From @cite{levin-1993}: the four verbs break, cut, hit, and touch are distinguished by the presence or absence of change of state, contact, motion, and causation.

Level 2 — Root structural entailments (§ 3b). Binary features capturing what the verb root itself entails about event structure: state, manner, result, and cause. From @cite{beavers-koontz-garboden-2020}. These sit between template-level event structure and surface meaning components, explaining why surface verbs have the components they do.

Level 3 — Root-specific features (§ 3). Range-valued dimensions capturing within-class variation in root content. A root's "position" along each dimension is not a point but a range of acceptable values (§ 2), reflecting the fact that verbs are compatible with a range of event types.

Levin class taxonomy

The full verb class taxonomy from @cite{levin-1993} Part II is encoded in § 4. This provides a standardized reference for verb classification; individual verb entries in Fragments/ are tagged with their Levin class.

Extensibility

Adding a new dimension: define a value type, add a Range field to RootProfile (defaulting to none). All existing entries compile unchanged. Adding a value to an existing dimension: breaking change — forces reviewing all entries that constrain that dimension. This is by design.

structure MeaningComponents : Type

Binary meaning components that define @cite{levin-1993} verb classes.

These describe surface verb behavior, not root-level entailments. @cite{beavers-koontz-garboden-2020} argue that surface CoS and causation can come from either the template or the root; see RootEntailments (§ 3b) for the root-level decomposition.

Diagnosed by participation in diathesis alternations (pp. 5–10):

• changeOfState: middle alternation, causative/inchoative alternation
• contact: body-part possessor ascension alternation
• motion: conative alternation (with contact)
• causation: causative/inchoative alternation (with changeOfState)

The four canonical classes from Levin's Introduction:

• break = [+CoS, −contact, −motion, +causation]
• cut = [+CoS, +contact, +motion, +causation]
• hit = [−CoS, +contact, +motion, −causation]
• touch = [−CoS, +contact, −motion, −causation]

Additional binary features (from class descriptions in Part II):

• instrumentSpec: verb specifies instrument/means (cut vs. break; p. 157)
• mannerSpec: verb specifies manner of action (cooking subclasses; p. 244)

• changeOfState : Bool

  Does the verb denote causing a change of state? Diagnostic: participation in the middle alternation (p. 5).

• contact : Bool

  Does the verb's meaning inherently involve contact? Diagnostic: body-part possessor ascension (p. 7).

• motion : Bool

  Does the verb's meaning inherently involve motion? Diagnostic: conative alternation requires both motion and contact (p. 8).

• causation : Bool

  Does the verb's meaning include a notion of causation? Diagnostic: participation in causative/inchoative alternation (p. 9).

• instrumentSpec : Bool

  Does the verb specify the instrument or means? Cut includes instrument specification; break does not (p. 157).

• mannerSpec : Bool

  Does the verb specify the manner of action? Cooking verbs "describe different ways of cooking food" (p. 244).

instance instDecidableEqMeaningComponents : DecidableEq MeaningComponents

Equations

• instDecidableEqMeaningComponents = instDecidableEqMeaningComponents.decEq

def instDecidableEqMeaningComponents.decEq (x✝ x✝¹ : MeaningComponents) : Decidable (x✝ = x✝¹)

Equations

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

instance instBEqMeaningComponents : BEq MeaningComponents

Equations

• instBEqMeaningComponents = { beq := instBEqMeaningComponents.beq }

def instBEqMeaningComponents.beq : MeaningComponents → MeaningComponents → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqMeaningComponents.beq x✝¹ x✝ = false

instance instReprMeaningComponents : Repr MeaningComponents

Equations

• instReprMeaningComponents = { reprPrec := instReprMeaningComponents.repr }

def instReprMeaningComponents.repr : MeaningComponents → Nat → Std.Format

Equations

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

def MeaningComponents.break_ : MeaningComponents

break verbs (45.1): pure change of state, no manner/instrument.

Equations

• MeaningComponents.break_ = { changeOfState := true, contact := false, motion := false, causation := true }

def MeaningComponents.cut : MeaningComponents

cut verbs (21.1): change of state via contact through motion.

Equations

• MeaningComponents.cut = { changeOfState := true, contact := true, motion := true, causation := true, instrumentSpec := true }

def MeaningComponents.hit : MeaningComponents

hit verbs (18.1): contact by impact, no change of state.

Equations

• MeaningComponents.hit = { changeOfState := false, contact := true, motion := true, causation := false }

def MeaningComponents.touch : MeaningComponents

touch verbs (20): pure contact, no motion or change of state.

Equations

• MeaningComponents.touch = { changeOfState := false, contact := true, motion := false, causation := false }

def MeaningComponents.destroy : MeaningComponents

destroy verbs (44): total destruction, no specific physical result.

Equations

• MeaningComponents.destroy = { changeOfState := true, contact := false, motion := false, causation := true }

def MeaningComponents.bend : MeaningComponents

bend verbs (45.2): shape change without disruption of integrity.

Equations

• MeaningComponents.bend = { changeOfState := true, contact := false, motion := false, causation := true }

@[reducible, inline]

abbrev Range (α : Type) : Type

Acceptable values along a quality dimension.

• none: the root is unconstrained on this dimension (says nothing)
• some [v₁, v₂, …]: the root is compatible with exactly these values

Roots are regions, not points: a verb like tear is compatible with a range of force levels, not a single one.

Equations

• Range α = Option (List α)

def Range.unconstrained {α : Type} : Range α

Equations

• Range.unconstrained = none

def Range.only {α : Type} (vs : List α) : Range α

Equations

• Range.only vs = some vs

def Range.isCompatible {α : Type} [BEq α] : Range α → α → Bool

Equations

• Range.isCompatible none x✝ = true
• Range.isCompatible (some vs) x✝ = vs.contains x✝

def Range.isConstrained {α : Type} : Range α → Bool

Equations

• Range.isConstrained none = false
• Range.isConstrained (some val) = true

def Range.overlaps {α : Type} [BEq α] : Range α → Range α → Bool

Two ranges overlap if they share at least one value.

Equations

• Range.overlaps none x✝ = true
• x✝.overlaps none = true
• Range.overlaps (some vs₁) (some vs₂) = vs₁.any fun (x : α) => vs₂.contains x

inductive ForceLevel : Type

Magnitude of force involved in the event.

@cite{talmy-1988} identifies force magnitude as a core parameter of force-dynamic schemas. Spalek & McNally: tear implies considerable force; rasgar implies less (enough to damage something flimsy).

• none : ForceLevel
• low : ForceLevel
• moderate : ForceLevel
• high : ForceLevel

instance instDecidableEqForceLevel : DecidableEq ForceLevel

Equations

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

def instBEqForceLevel.beq : ForceLevel → ForceLevel → Bool

Equations

• instBEqForceLevel.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqForceLevel : BEq ForceLevel

Equations

• instBEqForceLevel = { beq := instBEqForceLevel.beq }

def instReprForceLevel.repr : ForceLevel → Nat → Std.Format

Equations

• instReprForceLevel.repr ForceLevel.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ForceLevel.none")).group prec✝
• instReprForceLevel.repr ForceLevel.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ForceLevel.low")).group prec✝
• instReprForceLevel.repr ForceLevel.moderate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ForceLevel.moderate")).group prec✝
• instReprForceLevel.repr ForceLevel.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ForceLevel.high")).group prec✝

instance instReprForceLevel : Repr ForceLevel

Equations

• instReprForceLevel = { reprPrec := instReprForceLevel.repr }

inductive ForceDirection : Type

Spatial pattern of force application.

@cite{talmy-2000}: force vectors have directional parameters. Spalek & McNally: tear implies contrary-direction force (pulling apart); rasgar implies unidirectional force (gash-like).

• none : ForceDirection
• unidirectional : ForceDirection
• bidirectional : ForceDirection
• omnidirectional : ForceDirection

instance instDecidableEqForceDirection : DecidableEq ForceDirection

Equations

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

instance instBEqForceDirection : BEq ForceDirection

Equations

• instBEqForceDirection = { beq := instBEqForceDirection.beq }

def instBEqForceDirection.beq : ForceDirection → ForceDirection → Bool

Equations

• instBEqForceDirection.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def instReprForceDirection.repr : ForceDirection → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprForceDirection.repr ForceDirection.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ForceDirection.none")).group prec✝
• instReprForceDirection.repr ForceDirection.bidirectional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ForceDirection.bidirectional")).group prec✝

instance instReprForceDirection : Repr ForceDirection

Equations

• instReprForceDirection = { reprPrec := instReprForceDirection.repr }

inductive Robustness : Type

Material substantiality of the affected entity (patient).

Spalek & McNally (forthcoming): the primary dimension distinguishing tear (unrestricted) from rasgar (flimsy patients only).

• insubstantial : Robustness
• flimsy : Robustness
• moderate : Robustness
• robust : Robustness

instance instDecidableEqRobustness : DecidableEq Robustness

Equations

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

instance instBEqRobustness : BEq Robustness

Equations

• instBEqRobustness = { beq := instBEqRobustness.beq }

def instBEqRobustness.beq : Robustness → Robustness → Bool

Equations

• instBEqRobustness.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instReprRobustness : Repr Robustness

Equations

• instReprRobustness = { reprPrec := instReprRobustness.repr }

def instReprRobustness.repr : Robustness → Nat → Std.Format

Equations

• instReprRobustness.repr Robustness.insubstantial prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Robustness.insubstantial")).group prec✝
• instReprRobustness.repr Robustness.flimsy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Robustness.flimsy")).group prec✝
• instReprRobustness.repr Robustness.moderate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Robustness.moderate")).group prec✝
• instReprRobustness.repr Robustness.robust prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Robustness.robust")).group prec✝

inductive ResultType : Type

Nature of the physical change produced by the event.

Grounded in @cite{levin-1993}'s class descriptions and @cite{hale-keyser-1987} notion of "separation in material integrity":

• 45.1 Break: loss of material integrity (break, crack, shatter, tear)
• 45.2 Bend: change in shape without loss of integrity
• 44 Destroy: total destruction (no specific resulting state)
• 21 Cut: separation via instrument contact Refined by @cite{beavers-koontz-garboden-2020} on CoS root types.

• separation : ResultType
• surfaceBreach : ResultType
• fracture : ResultType
• fragmentation : ResultType
• deformation : ResultType
• totalDestruction : ResultType

instance instDecidableEqResultType : DecidableEq ResultType

Equations

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

def instBEqResultType.beq : ResultType → ResultType → Bool

Equations

• instBEqResultType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqResultType : BEq ResultType

Equations

• instBEqResultType = { beq := instBEqResultType.beq }

instance instReprResultType : Repr ResultType

Equations

• instReprResultType = { reprPrec := instReprResultType.repr }

def instReprResultType.repr : ResultType → Nat → Std.Format

Equations

• instReprResultType.repr ResultType.separation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultType.separation")).group prec✝
• instReprResultType.repr ResultType.surfaceBreach prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultType.surfaceBreach")).group prec✝
• instReprResultType.repr ResultType.fracture prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultType.fracture")).group prec✝
• instReprResultType.repr ResultType.fragmentation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultType.fragmentation")).group prec✝
• instReprResultType.repr ResultType.deformation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultType.deformation")).group prec✝
• instReprResultType.repr ResultType.totalDestruction prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultType.totalDestruction")).group prec✝

inductive Volitionality : Type

Whether the agent acts with volitional intent.

@cite{dowty-1991}: Proto-Agent entailment P1 = "volitional involvement in the event or state." @cite{ausensi-yu-smith-2021}: killing verb roots impose specific intentionality requirements on the agent (murder requires intentional agent; kill does not). @cite{levin-1993}: some break verbs "allow unintentional, action interpretations with body-part objects."

• nonvolitional : Volitionality
• neutral : Volitionality
• volitional : Volitionality

instance instDecidableEqVolitionality : DecidableEq Volitionality

Equations

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

def instBEqVolitionality.beq : Volitionality → Volitionality → Bool

Equations

• instBEqVolitionality.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqVolitionality : BEq Volitionality

Equations

• instBEqVolitionality = { beq := instBEqVolitionality.beq }

instance instReprVolitionality : Repr Volitionality

Equations

• instReprVolitionality = { reprPrec := instReprVolitionality.repr }

def instReprVolitionality.repr : Volitionality → Nat → Std.Format

Equations

• instReprVolitionality.repr Volitionality.nonvolitional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Volitionality.nonvolitional")).group prec✝
• instReprVolitionality.repr Volitionality.neutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Volitionality.neutral")).group prec✝
• instReprVolitionality.repr Volitionality.volitional prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Volitionality.volitional")).group prec✝

inductive AgentControl : Type

Whether the action can be performed with care and control.

@cite{dowty-1991}: Proto-Agent entailment P2 = "sentience (and/or perception)," enabling controlled action. Spalek & McNally: tear is compatible with careful action ("carefully tore the tin foil"); rasgar is not ("??rasgaron con cuidado el papel").

• incompatible : AgentControl
• neutral : AgentControl
• compatible : AgentControl

instance instDecidableEqAgentControl : DecidableEq AgentControl

Equations

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

instance instBEqAgentControl : BEq AgentControl

Equations

• instBEqAgentControl = { beq := instBEqAgentControl.beq }

def instBEqAgentControl.beq : AgentControl → AgentControl → Bool

Equations

• instBEqAgentControl.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instReprAgentControl : Repr AgentControl

Equations

• instReprAgentControl = { reprPrec := instReprAgentControl.repr }

def instReprAgentControl.repr : AgentControl → Nat → Std.Format

Equations

• instReprAgentControl.repr AgentControl.incompatible prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgentControl.incompatible")).group prec✝
• instReprAgentControl.repr AgentControl.neutral prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgentControl.neutral")).group prec✝
• instReprAgentControl.repr AgentControl.compatible prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgentControl.compatible")).group prec✝

structure RootProfile : Type

Within-class root content profile.

Captures quality dimensions of root content — force, robustness, agent properties — as opposed to RootEntailments (§ 3b), which captures structural entailments (state, manner, result, cause).

Each dimension is a Range of acceptable values; none means the root says nothing about that dimension (unconstrained).

Together with MeaningComponents (which defines the class), LevinClass (which identifies the class), and RootEntailments (which captures structural entailments), this gives a four-level characterization of a verb's semantic content:

1. Class-defining meaning components (binary, from alternations)
2. Class membership (Levin taxonomy)
3. Root structural entailments (B&@cite{beavers-koontz-garboden-2020})
4. Root-specific quality features (ranges, from detailed lexical analysis)

• forceMag : Range ForceLevel

  Force magnitude: @cite{talmy-1988}.

• forceDir : Range ForceDirection

  Force directionality: @cite{talmy-2000}, Spalek & McNally.

• patientRob : Range Robustness

  Patient material robustness: Spalek & McNally.

• resultType : Range ResultType

  Type of physical change: @cite{levin-1993}, @cite{beavers-koontz-garboden-2020}.

• agentVolition : Range Volitionality

  Agent volitionality: @cite{dowty-1991} P1, @cite{ausensi-yu-smith-2021}.

• agentControl : Range AgentControl

  Agent control: @cite{dowty-1991} P2, Spalek & McNally.

instance instBEqRootProfile : BEq RootProfile

Equations

• instBEqRootProfile = { beq := instBEqRootProfile.beq }

def instBEqRootProfile.beq : RootProfile → RootProfile → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqRootProfile.beq x✝¹ x✝ = false

instance instReprRootProfile : Repr RootProfile

Equations

• instReprRootProfile = { reprPrec := instReprRootProfile.repr }

def instReprRootProfile.repr : RootProfile → Nat → Std.Format

Equations

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

def instInhabitedRootProfile.default : RootProfile

Equations

• instInhabitedRootProfile.default = { forceMag := default, forceDir := default, patientRob := default, resultType := default, agentVolition := default, agentControl := default }

instance instInhabitedRootProfile : Inhabited RootProfile

Equations

• instInhabitedRootProfile = { default := instInhabitedRootProfile.default }

structure RootEntailments : Type

Root-level structural entailments from @cite{beavers-koontz-garboden-2020}.

B&KG argue against Bifurcation (roots only contribute idiosyncratic content) and Manner/Result Complementarity (no root encodes both). Roots CAN entail states, change, and causation — notions traditionally reserved for templates (CAUSE, BECOME).

The four features define a root typology (Table 12, p. 228):

• state: root describes a state (√FLAT, √CRACK, √DRY)
• manner: root describes an action/manner (√JOG, √RUN, √HIT)
• result: root entails change — passes restitutive again test
• cause: root entails causation

Constraints: result → state and cause → result (see wellFormed).

@cite{beavers-koontz-garboden-2020}

• state : Bool
• manner : Bool
• result : Bool
• cause : Bool

def instDecidableEqRootEntailments.decEq (x✝ x✝¹ : RootEntailments) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqRootEntailments : DecidableEq RootEntailments

Equations

• instDecidableEqRootEntailments = instDecidableEqRootEntailments.decEq

instance instBEqRootEntailments : BEq RootEntailments

Equations

• instBEqRootEntailments = { beq := instBEqRootEntailments.beq }

def instBEqRootEntailments.beq : RootEntailments → RootEntailments → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqRootEntailments.beq x✝¹ x✝ = false

def instReprRootEntailments.repr : RootEntailments → Nat → Std.Format

Equations

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

instance instReprRootEntailments : Repr RootEntailments

Equations

• instReprRootEntailments = { reprPrec := instReprRootEntailments.repr }

def RootEntailments.resultImpliesState (r : RootEntailments) : Bool

If a root entails change (result), it entails a state that changes. B&@cite{beavers-koontz-garboden-2020}: result entailments presuppose state entailments.

Equations

• r.resultImpliesState = (!r.result || r.state)

def RootEntailments.causeImpliesResult (r : RootEntailments) : Bool

If a root entails causation, it entails what is caused (a result). B&@cite{beavers-koontz-garboden-2020}: cause entailments presuppose result entailments.

Equations

• r.causeImpliesResult = (!r.cause || r.result)

def RootEntailments.wellFormed (r : RootEntailments) : Bool

Well-formedness: both collocational constraints hold.

Equations

• r.wellFormed = (r.resultImpliesState && r.causeImpliesResult)

Canonical root types (B&KG Table 12)

def RootEntailments.propertyConcept : RootEntailments

+S −M −R −C: property concept roots (√FLAT, √DRY). Deadjectival COS verbs — the root names the result state. Table 12, row 1, complement position.

Equations

• RootEntailments.propertyConcept = { state := true, manner := false, result := false, cause := false }

def RootEntailments.pureResult : RootEntailments

+S −M +R −C: internally caused result roots (√BLOSSOM, √RUST). Root entails both a state and a change to that state, but not external causation. Table 12, row 2, complement position.

Equations

• RootEntailments.pureResult = { state := true, manner := false, result := true, cause := false }

def RootEntailments.causativeResult : RootEntailments

+S −M +R +C: externally caused result roots (√CRACK, √BREAK). Root entails a state, change, AND causation — the root inherently implies an external cause. Table 12, row 3, complement position. B&KG (p. 228): these "lexicalize crosslinguistically as basic causatives" unlike √BLOSSOM-type roots.

Equations

• RootEntailments.causativeResult = { state := true, manner := false, result := true, cause := true }

def RootEntailments.pureManner : RootEntailments

−S +M −R −C: pure manner roots (√JOG, √RUN, √SWIM). Root specifies action manner without entailing any state. Table 12, row 4, adjoined position.

Equations

• RootEntailments.pureManner = { state := false, manner := true, result := false, cause := false }

def RootEntailments.mannerResult : RootEntailments

+S +M +R −C: manner + result without cause. Well-formed per the constraints but UNATTESTED in B&KG's Table 12 (row 6 is empty in both positions). B&KG (p. 229): such roots "would essentially derive syntactically unergative verbs with pure change-of-state meanings." Defined for completeness.

Equations

• RootEntailments.mannerResult = { state := true, manner := true, result := true, cause := false }

def RootEntailments.fullSpec : RootEntailments

+S +M +R +C: fully specified roots (√HAND, √DROWN, √CUT). B&KG Ch. 3–4: manner + caused change. These are the attested MRC violators. Table 12, row 7. √HAND sits in adjoined position, √DROWN in complement position; this structural difference is not captured here.

Equations

• RootEntailments.fullSpec = { state := true, manner := true, result := true, cause := true }

def RootEntailments.minimal : RootEntailments

−S −M −R −C: minimal roots — no structural entailments. Conservative default for classes not yet studied under B&KG's framework. Not a row in Table 12 (which only lists roots with at least one positive feature).

Equations

• RootEntailments.minimal = { state := false, manner := false, result := false, cause := false }

Canonical type well-formedness

theorem RootEntailments.propertyConcept_wf : propertyConcept.wellFormed = true

theorem RootEntailments.pureResult_wf : pureResult.wellFormed = true

theorem RootEntailments.causativeResult_wf : causativeResult.wellFormed = true

theorem RootEntailments.pureManner_wf : pureManner.wellFormed = true

theorem RootEntailments.mannerResult_wf : mannerResult.wellFormed = true

theorem RootEntailments.fullSpec_wf : fullSpec.wellFormed = true

theorem RootEntailments.minimal_wf : minimal.wellFormed = true

MRC violation detection

def RootEntailments.violatesMRC (r : RootEntailments) : Bool

Does this root violate Manner/Result Complementarity? B&KG Ch. 4: some roots encode both manner and result.

Equations

• r.violatesMRC = (r.manner && r.result)

theorem RootEntailments.fullSpec_violates_MRC : fullSpec.violatesMRC = true

theorem RootEntailments.mannerResult_violates_MRC : mannerResult.violatesMRC = true

theorem RootEntailments.pureResult_respects_MRC : pureResult.violatesMRC = false

theorem RootEntailments.pureManner_respects_MRC : pureManner.violatesMRC = false

theorem RootEntailments.causativeResult_respects_MRC : causativeResult.violatesMRC = false

inductive LevinClass : Type

Verb class taxonomy from @cite{levin-1993} Part II.

Section numbers follow the book. Class names are Levin's labels. This provides a standardized, widely-cited reference for verb classification; 49 top-level classes covering the English verb lexicon.

Not all subclasses are listed here — the taxonomy is intentionally at the top-level class grain, with subclass distinctions handled by MeaningComponents and RootProfile.

• put : LevinClass
• funnel : LevinClass
• pour : LevinClass
• coil : LevinClass
• sprayLoad : LevinClass
• remove : LevinClass
• clear : LevinClass
• wipe : LevinClass
• steal : LevinClass
• send : LevinClass
• carry : LevinClass
• drive : LevinClass
• pushPull : LevinClass
• give : LevinClass
• contribute : LevinClass
• getObtain : LevinClass
• exchange : LevinClass
• learn : LevinClass
• hold : LevinClass
• conceal : LevinClass
• throw : LevinClass
• hit : LevinClass
• swat : LevinClass
• poke : LevinClass
• touch : LevinClass
• cut : LevinClass
• carve : LevinClass
• mix : LevinClass
• amalgamate : LevinClass
• separate : LevinClass
• split : LevinClass
• color : LevinClass
• imageCreation : LevinClass
• build : LevinClass
• grow : LevinClass
• create : LevinClass
• knead : LevinClass
• turn : LevinClass
• performance : LevinClass
• engender : LevinClass
• calve : LevinClass
• appoint : LevinClass
• characterize : LevinClass
• declare : LevinClass
• see : LevinClass
• sight : LevinClass
• amuse : LevinClass
• admire : LevinClass
• marvel : LevinClass
• want : LevinClass
• judgment : LevinClass
• assessment : LevinClass
• search : LevinClass
• socialInteraction : LevinClass
• say : LevinClass
• tell : LevinClass
• mannerOfSpeaking : LevinClass
• animalSound : LevinClass
• eat : LevinClass
• devour : LevinClass
• dine : LevinClass
• bodyProcess : LevinClass
• flinch : LevinClass
• dress : LevinClass
• murder : LevinClass
• poison : LevinClass
• lightEmission : LevinClass
• soundEmission : LevinClass
• substanceEmission : LevinClass
• destroy : LevinClass
• break_ : LevinClass
• bend : LevinClass
• cooking : LevinClass
• otherCoS : LevinClass
• entitySpecificCoS : LevinClass
• calibratableCoS : LevinClass
• lodge : LevinClass
• exist : LevinClass
• appear : LevinClass
• bodyInternalMotion : LevinClass
• assumePosition : LevinClass
• inherentlyDirectedMotion : LevinClass
• leave : LevinClass
• mannerOfMotion : LevinClass
• vehicleMotion : LevinClass
• chase : LevinClass
• avoid : LevinClass
• linger : LevinClass
• rush : LevinClass
• measure : LevinClass
• aspectual : LevinClass
• weather : LevinClass

instance instDecidableEqLevinClass : DecidableEq LevinClass

Equations

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

def instBEqLevinClass.beq : LevinClass → LevinClass → Bool

Equations

• instBEqLevinClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqLevinClass : BEq LevinClass

Equations

• instBEqLevinClass = { beq := instBEqLevinClass.beq }

def instReprLevinClass.repr : LevinClass → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprLevinClass.repr LevinClass.put prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.put")).group prec✝
• instReprLevinClass.repr LevinClass.funnel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.funnel")).group prec✝
• instReprLevinClass.repr LevinClass.pour prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.pour")).group prec✝
• instReprLevinClass.repr LevinClass.coil prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.coil")).group prec✝
• instReprLevinClass.repr LevinClass.sprayLoad prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.sprayLoad")).group prec✝
• instReprLevinClass.repr LevinClass.remove prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.remove")).group prec✝
• instReprLevinClass.repr LevinClass.clear prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.clear")).group prec✝
• instReprLevinClass.repr LevinClass.wipe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.wipe")).group prec✝
• instReprLevinClass.repr LevinClass.steal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.steal")).group prec✝
• instReprLevinClass.repr LevinClass.send prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.send")).group prec✝
• instReprLevinClass.repr LevinClass.carry prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.carry")).group prec✝
• instReprLevinClass.repr LevinClass.drive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.drive")).group prec✝
• instReprLevinClass.repr LevinClass.pushPull prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.pushPull")).group prec✝
• instReprLevinClass.repr LevinClass.give prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.give")).group prec✝
• instReprLevinClass.repr LevinClass.contribute prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.contribute")).group prec✝
• instReprLevinClass.repr LevinClass.getObtain prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.getObtain")).group prec✝
• instReprLevinClass.repr LevinClass.exchange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.exchange")).group prec✝
• instReprLevinClass.repr LevinClass.learn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.learn")).group prec✝
• instReprLevinClass.repr LevinClass.hold prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.hold")).group prec✝
• instReprLevinClass.repr LevinClass.conceal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.conceal")).group prec✝
• instReprLevinClass.repr LevinClass.throw prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.throw")).group prec✝
• instReprLevinClass.repr LevinClass.hit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.hit")).group prec✝
• instReprLevinClass.repr LevinClass.swat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.swat")).group prec✝
• instReprLevinClass.repr LevinClass.poke prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.poke")).group prec✝
• instReprLevinClass.repr LevinClass.touch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.touch")).group prec✝
• instReprLevinClass.repr LevinClass.cut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.cut")).group prec✝
• instReprLevinClass.repr LevinClass.carve prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.carve")).group prec✝
• instReprLevinClass.repr LevinClass.mix prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.mix")).group prec✝
• instReprLevinClass.repr LevinClass.amalgamate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.amalgamate")).group prec✝
• instReprLevinClass.repr LevinClass.separate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.separate")).group prec✝
• instReprLevinClass.repr LevinClass.split prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.split")).group prec✝
• instReprLevinClass.repr LevinClass.color prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.color")).group prec✝
• instReprLevinClass.repr LevinClass.imageCreation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.imageCreation")).group prec✝
• instReprLevinClass.repr LevinClass.build prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.build")).group prec✝
• instReprLevinClass.repr LevinClass.grow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.grow")).group prec✝
• instReprLevinClass.repr LevinClass.create prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.create")).group prec✝
• instReprLevinClass.repr LevinClass.knead prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.knead")).group prec✝
• instReprLevinClass.repr LevinClass.turn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.turn")).group prec✝
• instReprLevinClass.repr LevinClass.performance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.performance")).group prec✝
• instReprLevinClass.repr LevinClass.engender prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.engender")).group prec✝
• instReprLevinClass.repr LevinClass.calve prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.calve")).group prec✝
• instReprLevinClass.repr LevinClass.appoint prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.appoint")).group prec✝
• instReprLevinClass.repr LevinClass.characterize prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.characterize")).group prec✝
• instReprLevinClass.repr LevinClass.declare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.declare")).group prec✝
• instReprLevinClass.repr LevinClass.see prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.see")).group prec✝
• instReprLevinClass.repr LevinClass.sight prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.sight")).group prec✝
• instReprLevinClass.repr LevinClass.amuse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.amuse")).group prec✝
• instReprLevinClass.repr LevinClass.admire prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.admire")).group prec✝
• instReprLevinClass.repr LevinClass.marvel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.marvel")).group prec✝
• instReprLevinClass.repr LevinClass.want prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.want")).group prec✝
• instReprLevinClass.repr LevinClass.judgment prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.judgment")).group prec✝
• instReprLevinClass.repr LevinClass.assessment prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.assessment")).group prec✝
• instReprLevinClass.repr LevinClass.search prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.search")).group prec✝
• instReprLevinClass.repr LevinClass.socialInteraction prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.socialInteraction")).group prec✝
• instReprLevinClass.repr LevinClass.say prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.say")).group prec✝
• instReprLevinClass.repr LevinClass.tell prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.tell")).group prec✝
• instReprLevinClass.repr LevinClass.mannerOfSpeaking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.mannerOfSpeaking")).group prec✝
• instReprLevinClass.repr LevinClass.animalSound prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.animalSound")).group prec✝
• instReprLevinClass.repr LevinClass.eat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.eat")).group prec✝
• instReprLevinClass.repr LevinClass.devour prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.devour")).group prec✝
• instReprLevinClass.repr LevinClass.dine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.dine")).group prec✝
• instReprLevinClass.repr LevinClass.bodyProcess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.bodyProcess")).group prec✝
• instReprLevinClass.repr LevinClass.flinch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.flinch")).group prec✝
• instReprLevinClass.repr LevinClass.dress prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.dress")).group prec✝
• instReprLevinClass.repr LevinClass.murder prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.murder")).group prec✝
• instReprLevinClass.repr LevinClass.poison prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.poison")).group prec✝
• instReprLevinClass.repr LevinClass.lightEmission prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.lightEmission")).group prec✝
• instReprLevinClass.repr LevinClass.soundEmission prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.soundEmission")).group prec✝
• instReprLevinClass.repr LevinClass.substanceEmission prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.substanceEmission")).group prec✝
• instReprLevinClass.repr LevinClass.destroy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.destroy")).group prec✝
• instReprLevinClass.repr LevinClass.break_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.break_")).group prec✝
• instReprLevinClass.repr LevinClass.bend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.bend")).group prec✝
• instReprLevinClass.repr LevinClass.cooking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.cooking")).group prec✝
• instReprLevinClass.repr LevinClass.otherCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.otherCoS")).group prec✝
• instReprLevinClass.repr LevinClass.entitySpecificCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.entitySpecificCoS")).group prec✝
• instReprLevinClass.repr LevinClass.calibratableCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.calibratableCoS")).group prec✝
• instReprLevinClass.repr LevinClass.lodge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.lodge")).group prec✝
• instReprLevinClass.repr LevinClass.exist prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.exist")).group prec✝
• instReprLevinClass.repr LevinClass.appear prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.appear")).group prec✝
• instReprLevinClass.repr LevinClass.bodyInternalMotion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.bodyInternalMotion")).group prec✝
• instReprLevinClass.repr LevinClass.assumePosition prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.assumePosition")).group prec✝
• instReprLevinClass.repr LevinClass.leave prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.leave")).group prec✝
• instReprLevinClass.repr LevinClass.mannerOfMotion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.mannerOfMotion")).group prec✝
• instReprLevinClass.repr LevinClass.vehicleMotion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.vehicleMotion")).group prec✝
• instReprLevinClass.repr LevinClass.chase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.chase")).group prec✝
• instReprLevinClass.repr LevinClass.avoid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.avoid")).group prec✝
• instReprLevinClass.repr LevinClass.linger prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.linger")).group prec✝
• instReprLevinClass.repr LevinClass.rush prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.rush")).group prec✝
• instReprLevinClass.repr LevinClass.measure prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.measure")).group prec✝
• instReprLevinClass.repr LevinClass.aspectual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.aspectual")).group prec✝
• instReprLevinClass.repr LevinClass.weather prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.weather")).group prec✝

instance instReprLevinClass : Repr LevinClass

Equations

• instReprLevinClass = { reprPrec := instReprLevinClass.repr }

def LevinClass.section : LevinClass → String

Section number in @cite{levin-1993} for each class.

Equations

• LevinClass.put.section = "9.1"
• LevinClass.funnel.section = "9.3"
• LevinClass.pour.section = "9.5"
• LevinClass.coil.section = "9.6"
• LevinClass.sprayLoad.section = "9.7"
• LevinClass.remove.section = "10.1"
• LevinClass.clear.section = "10.3"
• LevinClass.wipe.section = "10.4"
• LevinClass.steal.section = "10.5"
• LevinClass.send.section = "11.1"
• LevinClass.carry.section = "11.4"
• LevinClass.drive.section = "11.5"
• LevinClass.pushPull.section = "12"
• LevinClass.give.section = "13.1"
• LevinClass.contribute.section = "13.2"
• LevinClass.getObtain.section = "13.5"
• LevinClass.exchange.section = "13.6"
• LevinClass.learn.section = "14"
• LevinClass.hold.section = "15.1"
• LevinClass.conceal.section = "16"
• LevinClass.throw.section = "17.1"
• LevinClass.hit.section = "18.1"
• LevinClass.swat.section = "18.2"
• LevinClass.poke.section = "19"
• LevinClass.touch.section = "20"
• LevinClass.cut.section = "21.1"
• LevinClass.carve.section = "21.2"
• LevinClass.mix.section = "22.1"
• LevinClass.amalgamate.section = "22.2"
• LevinClass.separate.section = "23.1"
• LevinClass.split.section = "23.2"
• LevinClass.color.section = "24"
• LevinClass.imageCreation.section = "25"
• LevinClass.build.section = "26.1"
• LevinClass.grow.section = "26.2"
• LevinClass.create.section = "26.4"
• LevinClass.knead.section = "26.5"
• LevinClass.turn.section = "26.6"
• LevinClass.performance.section = "26.7"
• LevinClass.engender.section = "27"
• LevinClass.calve.section = "28"
• LevinClass.appoint.section = "29.1"
• LevinClass.characterize.section = "29.2"
• LevinClass.declare.section = "29.4"
• LevinClass.see.section = "30.1"
• LevinClass.sight.section = "30.2"
• LevinClass.amuse.section = "31.1"
• LevinClass.admire.section = "31.2"
• LevinClass.marvel.section = "31.3"
• LevinClass.want.section = "32.1"
• LevinClass.judgment.section = "33"
• LevinClass.assessment.section = "34"
• LevinClass.search.section = "35"
• LevinClass.socialInteraction.section = "36"
• LevinClass.say.section = "37.7"
• LevinClass.tell.section = "37.2"
• LevinClass.mannerOfSpeaking.section = "37.3"
• LevinClass.animalSound.section = "38"
• LevinClass.eat.section = "39.1"
• LevinClass.devour.section = "39.4"
• LevinClass.dine.section = "39.5"
• LevinClass.bodyProcess.section = "40.1"
• LevinClass.flinch.section = "40.5"
• LevinClass.dress.section = "41.1"
• LevinClass.murder.section = "42.1"
• LevinClass.poison.section = "42.2"
• LevinClass.lightEmission.section = "43.1"
• LevinClass.soundEmission.section = "43.2"
• LevinClass.substanceEmission.section = "43.4"
• LevinClass.destroy.section = "44"
• LevinClass.break_.section = "45.1"
• LevinClass.bend.section = "45.2"
• LevinClass.cooking.section = "45.3"
• LevinClass.otherCoS.section = "45.4"
• LevinClass.entitySpecificCoS.section = "45.5"
• LevinClass.calibratableCoS.section = "45.6"
• LevinClass.lodge.section = "46"
• LevinClass.exist.section = "47.1"
• LevinClass.appear.section = "48.1"
• LevinClass.bodyInternalMotion.section = "49"
• LevinClass.assumePosition.section = "50"
• LevinClass.inherentlyDirectedMotion.section = "51.1"
• LevinClass.leave.section = "51.2"
• LevinClass.mannerOfMotion.section = "51.3"
• LevinClass.vehicleMotion.section = "51.4"
• LevinClass.chase.section = "51.6"
• LevinClass.avoid.section = "52"
• LevinClass.linger.section = "53.1"
• LevinClass.rush.section = "53.2"
• LevinClass.measure.section = "54"
• LevinClass.aspectual.section = "55"
• LevinClass.weather.section = "57"

def LevinClass.meaningComponents : LevinClass → MeaningComponents

Meaning components associated with each Levin class.

Profiles are assigned using the diagnostic criteria from @cite{levin-1993}:

• changeOfState: middle alternation (the glass broke / this bread cuts easily)
• contact: body-part possessor ascension (I hit him on the arm / I hit his arm)
• motion: conative alternation requires motion + contact (I cut at the bread)
• causation: causative/inchoative alternation (she broke the vase / the vase broke)
• instrumentSpec: verb specifies instrument/means (cut vs. break; p. 157)
• mannerSpec: verb specifies manner of action (cooking, manner of motion; p. 244)

For classes not discussed in the canonical quadruple analysis, profiles are inferred from Part II class descriptions and alternation participation patterns.

Equations

• LevinClass.put.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
• LevinClass.funnel.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
• LevinClass.pour.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
• LevinClass.coil.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
• LevinClass.sprayLoad.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
• LevinClass.remove.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
• LevinClass.clear.meaningComponents = { changeOfState := true, contact := false, motion := true, causation := true }
• LevinClass.wipe.meaningComponents = { changeOfState := true, contact := true, motion := true, causation := true, mannerSpec := true }
• LevinClass.steal.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := true }
• LevinClass.send.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
• LevinClass.carry.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := true, mannerSpec := true }
• LevinClass.drive.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
• LevinClass.pushPull.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := false }
• LevinClass.give.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := true }
• LevinClass.contribute.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := true }
• LevinClass.getObtain.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.exchange.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.learn.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.hold.meaningComponents = { changeOfState := false, contact := true, motion := false, causation := false }
• LevinClass.conceal.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.throw.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := true }
• LevinClass.hit.meaningComponents = MeaningComponents.hit
• LevinClass.swat.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := false }
• LevinClass.poke.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := false, instrumentSpec := true }
• LevinClass.touch.meaningComponents = MeaningComponents.touch
• LevinClass.cut.meaningComponents = MeaningComponents.cut
• LevinClass.carve.meaningComponents = { changeOfState := true, contact := true, motion := true, causation := true, instrumentSpec := true }
• LevinClass.mix.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.amalgamate.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.separate.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.split.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true, instrumentSpec := true }
• LevinClass.color.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true }
• LevinClass.imageCreation.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true, instrumentSpec := true }
• LevinClass.build.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.grow.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.create.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.knead.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true, mannerSpec := true }
• LevinClass.turn.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.performance.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
• LevinClass.engender.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.calve.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := false }
• LevinClass.appoint.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.characterize.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.declare.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.see.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.sight.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.amuse.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.admire.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.marvel.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.want.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.judgment.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.assessment.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.search.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.socialInteraction.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.say.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.tell.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.mannerOfSpeaking.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
• LevinClass.animalSound.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
• LevinClass.eat.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := false }
• LevinClass.devour.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := false, mannerSpec := true }
• LevinClass.dine.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
• LevinClass.bodyProcess.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.flinch.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.dress.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true }
• LevinClass.murder.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.poison.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true, instrumentSpec := true }
• LevinClass.lightEmission.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.soundEmission.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.substanceEmission.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.destroy.meaningComponents = MeaningComponents.destroy
• LevinClass.break_.meaningComponents = MeaningComponents.break_
• LevinClass.bend.meaningComponents = MeaningComponents.bend
• LevinClass.cooking.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true, mannerSpec := true }
• LevinClass.otherCoS.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.entitySpecificCoS.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.calibratableCoS.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.lodge.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.exist.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.appear.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := false }
• LevinClass.bodyInternalMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.assumePosition.meaningComponents = { changeOfState := true, contact := false, motion := true, causation := false }
• LevinClass.inherentlyDirectedMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.leave.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.mannerOfMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false, mannerSpec := true }
• LevinClass.vehicleMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false, mannerSpec := true }
• LevinClass.chase.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
• LevinClass.avoid.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.linger.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
• LevinClass.rush.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false, mannerSpec := true }
• LevinClass.measure.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
• LevinClass.aspectual.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
• LevinClass.weather.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }

inductive DiathesisAlternation : Type

Diathesis alternations from @cite{levin-1993} Part One that serve as diagnostics for verb class membership. The first four are the canonical diagnostics from the Introduction (pp. 5–10); others are class-specific.

• causativeInchoative : DiathesisAlternation

  §1.1.2: she broke the vase / the vase broke. Diagnoses causation + CoS.

• middle : DiathesisAlternation

  §1.2: the bread cuts easily. Diagnoses change of state.

• conative : DiathesisAlternation

  §1.3: I cut at the bread. Diagnoses contact + motion.

• bodyPartPossessorAscension : DiathesisAlternation

  §1.4.1: I hit him on the arm / I hit his arm. Diagnoses contact.

• dative : DiathesisAlternation

  §2.1: give NP NP / give NP to NP. Give/send class.

• locative : DiathesisAlternation

  §2.3: spray paint on wall / spray wall with paint. Spray/load class.

• resultative : DiathesisAlternation

  §8.1: hammer the metal flat. Available to manner verbs.

instance instDecidableEqDiathesisAlternation : DecidableEq DiathesisAlternation

Equations

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

def instBEqDiathesisAlternation.beq : DiathesisAlternation → DiathesisAlternation → Bool

Equations

• instBEqDiathesisAlternation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance instBEqDiathesisAlternation : BEq DiathesisAlternation

Equations

• instBEqDiathesisAlternation = { beq := instBEqDiathesisAlternation.beq }

instance instReprDiathesisAlternation : Repr DiathesisAlternation

Equations

• instReprDiathesisAlternation = { reprPrec := instReprDiathesisAlternation.repr }

def instReprDiathesisAlternation.repr : DiathesisAlternation → Nat → Std.Format

Equations

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

def MeaningComponents.predictedAlternation : MeaningComponents → DiathesisAlternation → Bool

Predicted alternation participation derived from meaning components.

The core claim of @cite{levin-1993}: meaning components — diagnosed by alternation participation — form the bridge between verb semantics and verb syntax. Each diagnostic alternation corresponds to a specific configuration of meaning components:

Alternation	Required components
Causative/inchoative	changeOfState ∧ causation ∧ ¬instrumentSpec
Middle	changeOfState
Conative	contact ∧ motion
Body-part possessor ascension	contact
Resultative	changeOfState ∧ ¬instrumentSpec (manner verbs)

Dative and locative alternations are class-specific rather than component-derived, so they must be checked per class.

Equations

• x✝.predictedAlternation DiathesisAlternation.causativeInchoative = (x✝.changeOfState && x✝.causation && !x✝.instrumentSpec)
• x✝.predictedAlternation DiathesisAlternation.middle = x✝.changeOfState
• x✝.predictedAlternation DiathesisAlternation.conative = (x✝.contact && x✝.motion)
• x✝.predictedAlternation DiathesisAlternation.bodyPartPossessorAscension = x✝.contact
• x✝.predictedAlternation DiathesisAlternation.dative = false
• x✝.predictedAlternation DiathesisAlternation.locative = false
• x✝.predictedAlternation DiathesisAlternation.resultative = (x✝.changeOfState && !x✝.instrumentSpec)

def LevinClass.participatesIn (c : LevinClass) (alt : DiathesisAlternation) : Bool

Full alternation profile for a Levin class, combining component-derived predictions with class-specific overrides for dative and locative.

Equations

• LevinClass.give.participatesIn DiathesisAlternation.dative = (LevinClass.give.meaningComponents.predictedAlternation DiathesisAlternation.dative || true)
• LevinClass.send.participatesIn DiathesisAlternation.dative = (LevinClass.send.meaningComponents.predictedAlternation DiathesisAlternation.dative || true)
• LevinClass.tell.participatesIn DiathesisAlternation.dative = (LevinClass.tell.meaningComponents.predictedAlternation DiathesisAlternation.dative || true)
• LevinClass.sprayLoad.participatesIn DiathesisAlternation.locative = (LevinClass.sprayLoad.meaningComponents.predictedAlternation DiathesisAlternation.locative || true)
• c.participatesIn alt = (c.meaningComponents.predictedAlternation alt || false)

Canonical diagnostic theorems

The four verbs break, cut, hit, touch are distinguished by exactly their pattern of alternation participation (@cite{levin-1993}:5–10).

theorem break_alternations : LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.participatesIn DiathesisAlternation.middle = true ∧ LevinClass.break_.participatesIn DiathesisAlternation.conative = false ∧ LevinClass.break_.participatesIn DiathesisAlternation.bodyPartPossessorAscension = false

Break participates in causative/inchoative and middle (CoS + causation).

theorem cut_alternations : LevinClass.cut.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.cut.participatesIn DiathesisAlternation.middle = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

Cut participates in middle, conative, and BPPA but NOT causative/inchoative. Instrument specification blocks the inchoative: "*The string cut." (Levin p. 9, ex. 23b). Because cut inherently specifies an instrument, it requires an agent (p. 10).

theorem hit_alternations : LevinClass.hit.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.hit.participatesIn DiathesisAlternation.middle = false ∧ LevinClass.hit.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.hit.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

Hit participates in conative and body-part ascension (contact + motion, no CoS).

theorem touch_alternations : LevinClass.touch.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.middle = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.conative = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

Touch participates only in body-part ascension (contact only).

theorem MeaningComponents.instrumentSpec_blocks_ci (mc : MeaningComponents) (h : mc.instrumentSpec = true) : mc.predictedAlternation DiathesisAlternation.causativeInchoative = false

Instrument specification blocks the causative/inchoative alternation for any verb, regardless of other meaning components. Because the instrument must be wielded by an agent, the agentless inchoative variant is unavailable.

theorem MeaningComponents.instrumentSpec_blocks_resultative (mc : MeaningComponents) (h : mc.instrumentSpec = true) : mc.predictedAlternation DiathesisAlternation.resultative = false

Corollary: instrument specification also blocks the resultative (same reasoning — manner verbs that specify an instrument cannot appear in the resultative construction).

Cross-class predictions

theorem cos_classes_causative : LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.bend.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.cooking.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.otherCoS.participatesIn DiathesisAlternation.causativeInchoative = true

All CoS classes (§45) participate in the causative/inchoative alternation.

theorem sprayLoad_locative : LevinClass.sprayLoad.participatesIn DiathesisAlternation.locative = true

Spray/load participates in the locative alternation.

theorem give_dative : LevinClass.give.participatesIn DiathesisAlternation.dative = true

Give class participates in the dative alternation.

theorem motion_no_causative : LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.inherentlyDirectedMotion.participatesIn DiathesisAlternation.causativeInchoative = false

Motion verbs (§51) don't participate in causative alternation (no causation component).

theorem contact_motion_conative : LevinClass.hit.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.swat.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.poke.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.conative = true

Contact verbs predict conative alternation participation.

theorem touch_no_conative : LevinClass.touch.participatesIn DiathesisAlternation.conative = false

Touch verbs lack motion → no conative despite having contact.

theorem cut_no_resultative_break_resultative : LevinClass.cut.participatesIn DiathesisAlternation.resultative = false ∧ LevinClass.break_.participatesIn DiathesisAlternation.resultative = true

Cut participates in resultative; break does too (no instrumentSpec).

def LevinClass.predictsUnaccusative : LevinClass → Bool

Predicted unaccusativity from Levin class membership.

Based on Levin & Rappaport @cite{levin-hovav-1995}: unaccusativity correlates with internally caused change of state or directed change, while unergativity correlates with agentive activity.

For classes that participate in the causative/inchoative alternation (CoS + causation), this predicts unaccusativity for the intransitive (inchoative) alternant. For inherently intransitive classes (emission, existence, appearance), this predicts unaccusativity outright.

Key omission: manner-of-speaking verbs (§37.3) are predicted unergative here (agentive manner), but @cite{storment-2026} shows they are empirically unaccusative. This is a documented divergence.

Equations

• LevinClass.break_.predictsUnaccusative = true
• LevinClass.bend.predictsUnaccusative = true
• LevinClass.cooking.predictsUnaccusative = true
• LevinClass.otherCoS.predictsUnaccusative = true
• LevinClass.entitySpecificCoS.predictsUnaccusative = true
• LevinClass.calibratableCoS.predictsUnaccusative = true
• LevinClass.destroy.predictsUnaccusative = true
• LevinClass.mix.predictsUnaccusative = true
• LevinClass.amalgamate.predictsUnaccusative = true
• LevinClass.separate.predictsUnaccusative = true
• LevinClass.split.predictsUnaccusative = true
• LevinClass.appear.predictsUnaccusative = true
• LevinClass.exist.predictsUnaccusative = true
• LevinClass.calve.predictsUnaccusative = true
• LevinClass.inherentlyDirectedMotion.predictsUnaccusative = true
• LevinClass.leave.predictsUnaccusative = true
• LevinClass.lightEmission.predictsUnaccusative = true
• LevinClass.soundEmission.predictsUnaccusative = true
• LevinClass.substanceEmission.predictsUnaccusative = true
• LevinClass.weather.predictsUnaccusative = true
• x✝.predictsUnaccusative = false

Unaccusativity prediction theorems

theorem cos_predicts_unaccusative : LevinClass.break_.predictsUnaccusative = true ∧ LevinClass.bend.predictsUnaccusative = true ∧ LevinClass.cooking.predictsUnaccusative = true ∧ LevinClass.otherCoS.predictsUnaccusative = true

CoS classes (§45) predict unaccusative.

theorem mom_predicts_unergative : LevinClass.mannerOfMotion.predictsUnaccusative = false

Manner-of-motion (§51.3) predicts unergative.

theorem idm_predicts_unaccusative : LevinClass.inherentlyDirectedMotion.predictsUnaccusative = true

Inherently directed motion (§51.1) predicts unaccusative.

theorem emission_predicts_unaccusative : LevinClass.lightEmission.predictsUnaccusative = true ∧ LevinClass.soundEmission.predictsUnaccusative = true ∧ LevinClass.substanceEmission.predictsUnaccusative = true

Emission classes (§43) predict unaccusative.

theorem mos_predicts_unergative : LevinClass.mannerOfSpeaking.predictsUnaccusative = false

MoS (§37.3) does NOT predict unaccusative — this is the Storment divergence.

theorem causativeInchoative_implies_unaccusative : LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.predictsUnaccusative = true ∧ LevinClass.otherCoS.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.otherCoS.predictsUnaccusative = true

The causative/inchoative alternation implies the existence of an unaccusative variant: if a class participates in causative/inchoative, it predicts unaccusativity for the inchoative alternant.

def RootProfile.constrainsPatient (rp : RootProfile) : Bool

Does a root profile constrain patient properties?

Equations

• rp.constrainsPatient = rp.patientRob.isConstrained

def RootProfile.overlaps (rp₁ rp₂ : RootProfile) : Bool

Do two root profiles overlap (share at least one compatible event)?

Equations

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

def LevinClass.rootEntailments : LevinClass → RootEntailments

Root structural entailments for each Levin class.

Assignments marked (B&KG) are directly from @cite{beavers-koontz-garboden-2020} Table 12 and Chapters 2–5. Others are inferred from class semantics following B&KG's framework:

• Externally caused CoS → causativeResult (√CRACK pattern)
• Internally caused CoS → pureResult (√BLOSSOM pattern)
• Action/manner verbs → pureManner (√JOG pattern)
• MRC violators → fullSpec (√HAND/√DROWN pattern)
• Stative/psychological → propertyConcept (√FLAT pattern)

Classes marked (default) use minimal as a conservative placeholder pending detailed study under B&KG's framework.

Equations

• LevinClass.put.rootEntailments = RootEntailments.minimal
• LevinClass.funnel.rootEntailments = RootEntailments.pureManner
• LevinClass.pour.rootEntailments = RootEntailments.pureManner
• LevinClass.coil.rootEntailments = RootEntailments.pureManner
• LevinClass.sprayLoad.rootEntailments = RootEntailments.minimal
• LevinClass.remove.rootEntailments = RootEntailments.minimal
• LevinClass.clear.rootEntailments = RootEntailments.causativeResult
• LevinClass.wipe.rootEntailments = RootEntailments.pureManner
• LevinClass.steal.rootEntailments = RootEntailments.minimal
• LevinClass.send.rootEntailments = RootEntailments.minimal
• LevinClass.carry.rootEntailments = RootEntailments.pureManner
• LevinClass.drive.rootEntailments = RootEntailments.pureManner
• LevinClass.pushPull.rootEntailments = RootEntailments.pureManner
• LevinClass.give.rootEntailments = RootEntailments.fullSpec
• LevinClass.contribute.rootEntailments = RootEntailments.minimal
• LevinClass.getObtain.rootEntailments = RootEntailments.minimal
• LevinClass.exchange.rootEntailments = RootEntailments.minimal
• LevinClass.learn.rootEntailments = RootEntailments.minimal
• LevinClass.hold.rootEntailments = RootEntailments.propertyConcept
• LevinClass.conceal.rootEntailments = RootEntailments.causativeResult
• LevinClass.throw.rootEntailments = RootEntailments.fullSpec
• LevinClass.hit.rootEntailments = RootEntailments.pureManner
• LevinClass.swat.rootEntailments = RootEntailments.pureManner
• LevinClass.poke.rootEntailments = RootEntailments.pureManner
• LevinClass.touch.rootEntailments = RootEntailments.minimal
• LevinClass.cut.rootEntailments = RootEntailments.fullSpec
• LevinClass.carve.rootEntailments = RootEntailments.fullSpec
• LevinClass.mix.rootEntailments = RootEntailments.causativeResult
• LevinClass.amalgamate.rootEntailments = RootEntailments.causativeResult
• LevinClass.separate.rootEntailments = RootEntailments.causativeResult
• LevinClass.split.rootEntailments = RootEntailments.fullSpec
• LevinClass.color.rootEntailments = RootEntailments.causativeResult
• LevinClass.imageCreation.rootEntailments = RootEntailments.fullSpec
• LevinClass.build.rootEntailments = RootEntailments.causativeResult
• LevinClass.grow.rootEntailments = RootEntailments.pureResult
• LevinClass.create.rootEntailments = RootEntailments.causativeResult
• LevinClass.knead.rootEntailments = RootEntailments.fullSpec
• LevinClass.turn.rootEntailments = RootEntailments.causativeResult
• LevinClass.performance.rootEntailments = RootEntailments.pureManner
• LevinClass.engender.rootEntailments = RootEntailments.causativeResult
• LevinClass.calve.rootEntailments = RootEntailments.pureResult
• LevinClass.appoint.rootEntailments = RootEntailments.causativeResult
• LevinClass.characterize.rootEntailments = RootEntailments.minimal
• LevinClass.declare.rootEntailments = RootEntailments.causativeResult
• LevinClass.see.rootEntailments = RootEntailments.minimal
• LevinClass.sight.rootEntailments = RootEntailments.minimal
• LevinClass.amuse.rootEntailments = RootEntailments.causativeResult
• LevinClass.admire.rootEntailments = RootEntailments.propertyConcept
• LevinClass.marvel.rootEntailments = RootEntailments.propertyConcept
• LevinClass.want.rootEntailments = RootEntailments.propertyConcept
• LevinClass.judgment.rootEntailments = RootEntailments.minimal
• LevinClass.assessment.rootEntailments = RootEntailments.minimal
• LevinClass.search.rootEntailments = RootEntailments.pureManner
• LevinClass.socialInteraction.rootEntailments = RootEntailments.minimal
• LevinClass.say.rootEntailments = RootEntailments.minimal
• LevinClass.tell.rootEntailments = RootEntailments.minimal
• LevinClass.mannerOfSpeaking.rootEntailments = RootEntailments.pureManner
• LevinClass.animalSound.rootEntailments = RootEntailments.pureManner
• LevinClass.eat.rootEntailments = RootEntailments.causativeResult
• LevinClass.devour.rootEntailments = RootEntailments.fullSpec
• LevinClass.dine.rootEntailments = RootEntailments.pureManner
• LevinClass.bodyProcess.rootEntailments = RootEntailments.minimal
• LevinClass.flinch.rootEntailments = RootEntailments.minimal
• LevinClass.dress.rootEntailments = RootEntailments.causativeResult
• LevinClass.murder.rootEntailments = RootEntailments.causativeResult
• LevinClass.poison.rootEntailments = RootEntailments.fullSpec
• LevinClass.lightEmission.rootEntailments = RootEntailments.propertyConcept
• LevinClass.soundEmission.rootEntailments = RootEntailments.propertyConcept
• LevinClass.substanceEmission.rootEntailments = RootEntailments.propertyConcept
• LevinClass.destroy.rootEntailments = RootEntailments.causativeResult
• LevinClass.break_.rootEntailments = RootEntailments.causativeResult
• LevinClass.bend.rootEntailments = RootEntailments.causativeResult
• LevinClass.cooking.rootEntailments = RootEntailments.fullSpec
• LevinClass.otherCoS.rootEntailments = RootEntailments.causativeResult
• LevinClass.entitySpecificCoS.rootEntailments = RootEntailments.pureResult
• LevinClass.calibratableCoS.rootEntailments = RootEntailments.pureResult
• LevinClass.lodge.rootEntailments = RootEntailments.minimal
• LevinClass.exist.rootEntailments = RootEntailments.minimal
• LevinClass.appear.rootEntailments = RootEntailments.pureResult
• LevinClass.bodyInternalMotion.rootEntailments = RootEntailments.pureManner
• LevinClass.assumePosition.rootEntailments = RootEntailments.pureResult
• LevinClass.inherentlyDirectedMotion.rootEntailments = RootEntailments.pureResult
• LevinClass.leave.rootEntailments = RootEntailments.pureResult
• LevinClass.mannerOfMotion.rootEntailments = RootEntailments.pureManner
• LevinClass.vehicleMotion.rootEntailments = RootEntailments.pureManner
• LevinClass.chase.rootEntailments = RootEntailments.pureManner
• LevinClass.avoid.rootEntailments = RootEntailments.minimal
• LevinClass.linger.rootEntailments = RootEntailments.pureManner
• LevinClass.rush.rootEntailments = RootEntailments.pureManner
• LevinClass.measure.rootEntailments = RootEntailments.propertyConcept
• LevinClass.aspectual.rootEntailments = RootEntailments.minimal
• LevinClass.weather.rootEntailments = RootEntailments.minimal

Well-formedness verification

All canonical types satisfy the constraints, so every branch of rootEntailments is well-formed (each branch returns a canonical type).

theorem break_root_wf : LevinClass.break_.rootEntailments.wellFormed = true

Break roots (√CRACK) are well-formed.

theorem cut_root_wf : LevinClass.cut.rootEntailments.wellFormed = true

Cut roots (MRC violator, fullSpec) are well-formed.

theorem hit_root_wf : LevinClass.hit.rootEntailments.wellFormed = true

Hit roots (pureManner) are well-formed.

theorem touch_root_wf : LevinClass.touch.rootEntailments.wellFormed = true

Touch roots (minimal) are well-formed.

theorem give_root_wf : LevinClass.give.rootEntailments.wellFormed = true

Give roots (√HAND, fullSpec) are well-formed.

theorem destroy_root_wf : LevinClass.destroy.rootEntailments.wellFormed = true

Destroy roots (causativeResult) are well-formed.

theorem murder_root_wf : LevinClass.murder.rootEntailments.wellFormed = true

Murder roots (causativeResult) are well-formed.

theorem poison_root_wf : LevinClass.poison.rootEntailments.wellFormed = true

Poison roots (√DROWN-type fullSpec) are well-formed.

MRC violation verification

theorem cut_violates_MRC : LevinClass.cut.rootEntailments.violatesMRC = true

Cut is an MRC violator (B&KG Ch. 4): manner of cutting + caused separation.

theorem cooking_violates_MRC : LevinClass.cooking.rootEntailments.violatesMRC = true

Cooking is an MRC violator: cooking manner + caused CoS.

theorem poison_violates_MRC : LevinClass.poison.rootEntailments.violatesMRC = true

Poison (√DROWN-type) is an MRC violator: poisoning manner + caused death.

theorem break_respects_MRC : LevinClass.break_.rootEntailments.violatesMRC = false

Break respects MRC — pure result (√CRACK), no manner.

theorem hit_respects_MRC : LevinClass.hit.rootEntailments.violatesMRC = false

Hit respects MRC — pure manner (√JOG-type), no result.

Cross-layer consistency

Template + root entailments predict the event-structural subset of surface meaning components (changeOfState, causation, mannerSpec). Uses mc.changeOfState && mc.causation as a proxy for Template.hasCause (the accomplishment template is selected when both hold; the actual Template type lives in Theories/Semantics/Events/EventStructure.lean and cannot be imported here without creating a circular dependency).

B&KG's "manner" is broader than Levin's mannerSpec: B&KG code hit/cut as +manner (impact/cutting action), but Levin codes this as contact+motion (±instrument), not mannerSpec. The prediction holds for classes where root manner aligns with Levin's mannerSpec (cooking, motion) but diverges for contact-manner classes (hit, cut).

def predictEventStructural (templateHasCause : Bool) (r : RootEntailments) : Bool × Bool × Bool

Predict event-structural meaning components from template causation and root entailments.

Equations

• predictEventStructural templateHasCause r = (templateHasCause || r.result, templateHasCause || r.cause, r.manner)

def MeaningComponents.eventStructural (mc : MeaningComponents) : Bool × Bool × Bool

Event-structural subset of surface meaning components.

Equations

• mc.eventStructural = (mc.changeOfState, mc.causation, mc.mannerSpec)

def LevinClass.predictedEventStructural (c : LevinClass) : Bool × Bool × Bool

Predicted event structure for a Levin class. Uses mc.changeOfState && mc.causation as a proxy for Template.hasCause.

Equations

• c.predictedEventStructural = predictEventStructural (c.meaningComponents.changeOfState && c.meaningComponents.causation) c.rootEntailments

theorem break_eventStructural_consistent : LevinClass.break_.predictedEventStructural = LevinClass.break_.meaningComponents.eventStructural

Break: prediction matches observation (accomplishment + √CRACK).

theorem cooking_eventStructural_consistent : LevinClass.cooking.predictedEventStructural = LevinClass.cooking.meaningComponents.eventStructural

Cooking: prediction matches (accomplishment + fullSpec root).

theorem mannerOfMotion_eventStructural_consistent : LevinClass.mannerOfMotion.predictedEventStructural = LevinClass.mannerOfMotion.meaningComponents.eventStructural

Manner of motion: prediction matches (activity + √JOG).

theorem exist_eventStructural_consistent : LevinClass.exist.predictedEventStructural = LevinClass.exist.meaningComponents.eventStructural

Existence: prediction matches (stative + minimal root).

theorem destroy_eventStructural_consistent : LevinClass.destroy.predictedEventStructural = LevinClass.destroy.meaningComponents.eventStructural

Destroy: prediction matches (accomplishment + causativeResult).

theorem touch_eventStructural_consistent : LevinClass.touch.predictedEventStructural = LevinClass.touch.meaningComponents.eventStructural

Touch: prediction matches (activity + minimal root).

theorem murder_eventStructural_consistent : LevinClass.murder.predictedEventStructural = LevinClass.murder.meaningComponents.eventStructural

Murder: prediction matches (accomplishment + causativeResult).

theorem mannerOfSpeaking_eventStructural_consistent : LevinClass.mannerOfSpeaking.predictedEventStructural = LevinClass.mannerOfSpeaking.meaningComponents.eventStructural

Manner of speaking: prediction matches (activity + pureManner root).