Root Quality Dimensions and Structural Entailments

@cite{talmy-1988} @cite{talmy-2000} @cite{dowty-1991} @cite{beavers-koontz-garboden-2020} @cite{majid-boster-bowerman-2008}

Framework-agnostic infrastructure for characterizing verb root content. Roots are regions, not points: each dimension is a Range of acceptable values, reflecting that verbs are compatible with a range of event types.

Quality dimensions (§§ 1–2)

Range-valued dimensions capturing within-class variation: force magnitude, force direction, patient robustness, result type, instrument type, object dimensionality, agent volition, agent control.

Root structural entailments (§ 3)

From @cite{beavers-koontz-garboden-2020}: binary features capturing what the root itself entails about event structure (state, manner, result, cause).

Root structural position (§ 4)

From Marantz (2009) and @cite{beavers-koontz-garboden-2020}: whether the root merges as complement or adjunct of v.

@[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. @cite{spalek-mcnally-2026}: 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 ⋯

instance instBEqForceLevel : BEq ForceLevel

Equations

• instBEqForceLevel = { beq := instBEqForceLevel.beq }

def instBEqForceLevel.beq : ForceLevel → ForceLevel → Bool

Equations

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

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. @cite{spalek-mcnally-2026}: 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 ⋯

def instBEqForceDirection.beq : ForceDirection → ForceDirection → Bool

Equations

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

instance instBEqForceDirection : BEq ForceDirection

Equations

• instBEqForceDirection = { beq := instBEqForceDirection.beq }

instance instReprForceDirection : Repr ForceDirection

Equations

• instReprForceDirection = { reprPrec := instReprForceDirection.repr }

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✝

inductive Robustness : Type

Material substantiality of the affected entity (patient).

@cite{spalek-mcnally-2026}: 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 ⋯

def instBEqRobustness.beq : Robustness → Robustness → Bool

Equations

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

instance instBEqRobustness : BEq Robustness

Equations

• instBEqRobustness = { beq := instBEqRobustness.beq }

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 }

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✝

instance instReprResultType : Repr ResultType

Equations

• instReprResultType = { reprPrec := instReprResultType.repr }

inductive InstrumentType : Type

Type of instrument used in the event.

@cite{majid-boster-bowerman-2008}: instrument type interacts with object properties to determine the predictability of separation locus (their Dimension 1). Sharp instruments yield predictable separations; blunt instruments and hands yield unpredictable separations.

@cite{levin-1993}: cut verbs (§21) specify their instrument (instrumentSpec = true); break verbs (§45.1) do not.

• sharpBlade : InstrumentType
• bluntImpact : InstrumentType
• hands : InstrumentType
• none : InstrumentType

instance instDecidableEqInstrumentType : DecidableEq InstrumentType

Equations

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

def instBEqInstrumentType.beq : InstrumentType → InstrumentType → Bool

Equations

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

instance instBEqInstrumentType : BEq InstrumentType

Equations

• instBEqInstrumentType = { beq := instBEqInstrumentType.beq }

instance instReprInstrumentType : Repr InstrumentType

Equations

• instReprInstrumentType = { reprPrec := instReprInstrumentType.repr }

def instReprInstrumentType.repr : InstrumentType → Nat → Std.Format

Equations

• instReprInstrumentType.repr InstrumentType.sharpBlade prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "InstrumentType.sharpBlade")).group prec✝
• instReprInstrumentType.repr InstrumentType.bluntImpact prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "InstrumentType.bluntImpact")).group prec✝
• instReprInstrumentType.repr InstrumentType.hands prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "InstrumentType.hands")).group prec✝
• instReprInstrumentType.repr InstrumentType.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "InstrumentType.none")).group prec✝

inductive ObjectDimensionality : Type

Dimensionality of the affected object (patient).

@cite{majid-boster-bowerman-2008}: object dimensionality interacts with instrument type and manner of action to determine event categorization cross-linguistically. 1D objects (rope, stick) can be snapped; 2D objects (cloth, paper) can be torn; 3D objects (melon, pot) can be smashed.

• oneD : ObjectDimensionality
• twoD : ObjectDimensionality
• threeD : ObjectDimensionality

instance instDecidableEqObjectDimensionality : DecidableEq ObjectDimensionality

Equations

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

def instBEqObjectDimensionality.beq : ObjectDimensionality → ObjectDimensionality → Bool

Equations

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

instance instBEqObjectDimensionality : BEq ObjectDimensionality

Equations

• instBEqObjectDimensionality = { beq := instBEqObjectDimensionality.beq }

def instReprObjectDimensionality.repr : ObjectDimensionality → Nat → Std.Format

Equations

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

instance instReprObjectDimensionality : Repr ObjectDimensionality

Equations

• instReprObjectDimensionality = { reprPrec := instReprObjectDimensionality.repr }

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 ⋯

instance instBEqVolitionality : BEq Volitionality

Equations

• instBEqVolitionality = { beq := instBEqVolitionality.beq }

def instBEqVolitionality.beq : Volitionality → Volitionality → Bool

Equations

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

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✝

instance instReprVolitionality : Repr Volitionality

Equations

• instReprVolitionality = { reprPrec := instReprVolitionality.repr }

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. @cite{spalek-mcnally-2026}: 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)

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✝

instance instReprAgentControl : Repr AgentControl

Equations

• instReprAgentControl = { reprPrec := instReprAgentControl.repr }

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}, @cite{spalek-mcnally-2026}.

• patientRob : Range Robustness

  Patient material robustness: @cite{spalek-mcnally-2026}.

• 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, @cite{spalek-mcnally-2026}.

• instrumentType : Range InstrumentType

  Instrument type the root selects for: @cite{majid-boster-bowerman-2008}. cut selects for sharp blades; break is unspecified.

• patientDim : Range ObjectDimensionality

  Patient dimensionality: @cite{majid-boster-bowerman-2008}. tear selects for 2D objects (cloth, paper); snap for 1D (stick, twig).

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 instBEqRootProfile : BEq RootProfile

Equations

• instBEqRootProfile = { beq := instBEqRootProfile.beq }

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.

instance instInhabitedRootProfile : Inhabited RootProfile

Equations

• instInhabitedRootProfile = { default := instInhabitedRootProfile.default }

def instInhabitedRootProfile.default : RootProfile

Equations

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

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

instance instDecidableEqRootEntailments : DecidableEq RootEntailments

Equations

• instDecidableEqRootEntailments = instDecidableEqRootEntailments.decEq

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

Equations

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

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 RootPosition : Type

Structural attachment position of a verb root, following Marantz (2009a;b, 2013) as systematized by @cite{beavers-koontz-garboden-2020} Table 12.

• Complement: root merges as complement of v (inside VP). Fills the result-state slot. Change-of-state roots: √FLAT, √CRACK, √BLOSSOM, √DROWN.
• Adjoined: root merges as adjunct to v (outside VP). Modifies the causing event. Manner/activity roots: √JOG, √TOSS, √HAND.

This distinction is structurally significant beyond root typology: it determines vVPE eligibility (@cite{kalyakin-2026}), scope of result-state modifiers, and the restitutive/repetitive again ambiguity (@cite{beavers-koontz-garboden-2020}, @cite{merchant-2013}).

• complement : RootPosition
• adjoined : RootPosition

instance instDecidableEqRootPosition : DecidableEq RootPosition

Equations

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

instance instBEqRootPosition : BEq RootPosition

Equations

• instBEqRootPosition = { beq := instBEqRootPosition.beq }

def instBEqRootPosition.beq : RootPosition → RootPosition → Bool

Equations

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

instance instReprRootPosition : Repr RootPosition

Equations

• instReprRootPosition = { reprPrec := instReprRootPosition.repr }

def instReprRootPosition.repr : RootPosition → Nat → Std.Format

Equations

• instReprRootPosition.repr RootPosition.complement prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootPosition.complement")).group prec✝
• instReprRootPosition.repr RootPosition.adjoined prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootPosition.adjoined")).group prec✝

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.