Root Typology: States and Changes of State (@cite{beavers-etal-2021}, B&@cite{beavers-koontz-garboden-2020}) @cite{beavers-etal-2021} @cite{beavers-koontz-garboden-2020} @cite{coon-2019}

@cite{arad-2005} @cite{dixon-1982} @cite{embick-2004} @cite{dowty-1991} @cite{embick-2009} @cite{rose-nichols-2021} @cite{levin-1993}

Beavers, Everdell, Jerro, Kauhanen, @cite{beavers-etal-2021} "States and changes of state: A crosslinguistic study of the roots of verbal meaning." Language 97(3), 439–484.

Core contribution

Change-of-state verb roots split into two types:

• Property concept (PC) roots: flat, red, long — underlie deadjectival CoS verbs
• Result roots: crack, break, shatter — underlie non-deadjectival CoS verbs

The key semantic distinction: result roots lexically entail change, while PC roots do not. This refutes the Bifurcation Thesis: contra bifurcation, some roots introduce templatic meaning (change = BECOME).

The deepest theorem

A root's entailment of change determines ALL of its morphosyntactic behavior in a single four-way biconditional (§§3–8):

entailsChange R ↔ ¬hasSimpleStative R ∧ ¬verbalFormIsMarked R ∧ ¬allowsRestitutiveAgain R

This holds crosslinguistically (88-language typological study), ruling out bifurcation as an explanation. The deeper explanation is the Markedness Generalization (eq. 44): morphological markedness reflects semantic mismatch between functional head and root.

Bridges

• EntailmentProfile.changeOfState = result root entailment (ProtoRoles §8)
• TemplateHead.vBecome = the templatic operator that result roots lexicalize
• CoSType.inception = BECOME as ¬P→P transition (ChangeOfState/Theory)
• Template.achievement/.accomplishment = templates containing BECOME (EventStructure)
• Crosslinguistic data validates the correlations (Phenomena)

Unified Root (§§15–17)

Extends the file with the Root structure (§16) bundling @cite{coon-2019}'s arity dimension (does the root select an internal argument?) with Beavers et al.'s change-entailment dimension. The two axes cross-classify orthogonally (arity_changeType_orthogonal): knowing whether a root selects a theme tells you nothing about whether it entails change, and vice versa.

• Coon, J. (2019). Building verbs in Chuj: Consequences for the nature of roots. Journal of Linguistics 55(1): 35–81.
• Hale, K. & Keyser, S.J. (2002). Prolegomenon to a Theory of Argument Structure. MIT Press.
• Harley, H. (2014). On the identity of roots. Theoretical Linguistics 40, 225–276.

inductive RootType : Type

Two types of change-of-state verb roots (@cite{beavers-etal-2021} §3.1).

Property concept (PC) roots: underlie deadjectival CoS verbs. The root describes a gradable property (dimension, color, value, etc.). Examples: flat, red, long, warm.

Result roots: underlie non-deadjectival CoS verbs. The root describes a specific result state that arises from a particular kind of event (breaking, cooking, killing, etc.). Examples: crack, break, shatter.

• propertyConcept : RootType
• result : RootType

instance instDecidableEqRootType : DecidableEq RootType

Equations

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

instance instReprRootType : Repr RootType

Equations

• instReprRootType = { reprPrec := instReprRootType.repr }

def instReprRootType.repr : RootType → ℕ → Std.Format

Equations

• instReprRootType.repr RootType.propertyConcept prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootType.propertyConcept")).group prec✝
• instReprRootType.repr RootType.result prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootType.result")).group prec✝

def instBEqRootType.beq : RootType → RootType → Bool

Equations

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

instance instBEqRootType : BEq RootType

Equations

• instBEqRootType = { beq := instBEqRootType.beq }

def RootType.entailsChange : RootType → Bool

Whether a root lexically entails prior change (@cite{beavers-etal-2021} §3.6).

PC roots denote simple states that can hold without any prior change event. Result roots denote states that entail a prior change event.

Equations

• RootType.propertyConcept.entailsChange = false
• RootType.result.entailsChange = true

inductive RootArity : Type

Whether a root selects an internal (theme) argument.

@cite{coon-2019}: the central division of labor is that roots determine internal arguments while functional heads (v/Voice⁰) determine external arguments. This is orthogonal to change entailment.

• selectsTheme : RootArity
• noTheme : RootArity

instance instDecidableEqRootArity : DecidableEq RootArity

Equations

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

def instReprRootArity.repr : RootArity → ℕ → Std.Format

Equations

• instReprRootArity.repr RootArity.selectsTheme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootArity.selectsTheme")).group prec✝
• instReprRootArity.repr RootArity.noTheme prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "RootArity.noTheme")).group prec✝

instance instReprRootArity : Repr RootArity

Equations

• instReprRootArity = { reprPrec := instReprRootArity.repr }

instance instBEqRootArity : BEq RootArity

Equations

• instBEqRootArity = { beq := instBEqRootArity.beq }

def instBEqRootArity.beq : RootArity → RootArity → Bool

Equations

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

def RootArity.hasInternalArg : RootArity → Bool

Does this root arity entail an obligatory internal argument?

Equations

• RootArity.selectsTheme.hasInternalArg = true
• RootArity.noTheme.hasInternalArg = false

inductive RootDenotationType : Type

The semantic denotation domain of a root (@cite{coon-2019}, (3)).

• eventPred ⟨e, ⟨s,t⟩⟩: entity → event → truth-value (√TV, √ITV)
• measureFn ⟨e, ⟨s,d⟩⟩: entity → event → degree (√POS; @cite{henderson-2019})
• entityPred ⟨e,t⟩: entity → truth-value, no event (√NOM)

• eventPred : RootDenotationType
• measureFn : RootDenotationType
• entityPred : RootDenotationType

instance instDecidableEqRootDenotationType : DecidableEq RootDenotationType

Equations

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

instance instBEqRootDenotationType : BEq RootDenotationType

Equations

• instBEqRootDenotationType = { beq := instBEqRootDenotationType.beq }

def instBEqRootDenotationType.beq : RootDenotationType → RootDenotationType → Bool

Equations

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

def instReprRootDenotationType.repr : RootDenotationType → ℕ → Std.Format

Equations

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

instance instReprRootDenotationType : Repr RootDenotationType

Equations

• instReprRootDenotationType = { reprPrec := instReprRootDenotationType.repr }

structure Root : Type

Unified root characterization bundling all classification dimensions.

A root is characterized along five independent axes:

1. Arity: does it select an internal argument?
2. Change entailment: does it lexically entail a prior change event?
3. Denotation type (@cite{coon-2019}, (3)): event predicate, measure function, or entity predicate.
4. Quality dimensions (@cite{spalek-mcnally-2026}): within-class root content
5. Class membership: verb class taxonomy

Axes 1, 2, and 3 cross-classify: Coon's four Chuj root classes are recovered as (arity × denotationType) pairs: √TV = selectsTheme + eventPred, √ITV = noTheme + eventPred, √POS = noTheme + measureFn, √NOM = noTheme + entityPred.

• arity : RootArity

  Does this root select an internal argument?

• changeType : RootType

  Does this root lexically entail prior change?

• denotationType : Option RootDenotationType

  Semantic denotation domain (@cite{coon-2019}, (3)). Optional — not all roots have been annotated.

• profile : RootProfile

  Within-class quality dimensions (@cite{spalek-mcnally-2026})

• levinClass : Option LevinClass

  Verb class membership

def instBEqRoot.beq : Root → Root → Bool

Equations

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

instance instBEqRoot : BEq Root

Equations

• instBEqRoot = { beq := instBEqRoot.beq }

instance instReprRoot : Repr Root

Equations

• instReprRoot = { reprPrec := instReprRoot.repr }

def instReprRoot.repr : Root → ℕ → Std.Format

Equations

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

def Root.entailsChange (r : Root) : Bool

Does this root lexically entail prior change?

Equations

• r.entailsChange = r.changeType.entailsChange

inductive PCClass : Type

Property concept root subclasses (@cite{dixon-1982}; @cite{beavers-etal-2021} ex. 5).

• dimension : PCClass
• age : PCClass
• value : PCClass
• color : PCClass
• physicalProperty : PCClass
• speed : PCClass

instance instDecidableEqPCClass : DecidableEq PCClass

Equations

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

instance instReprPCClass : Repr PCClass

Equations

• instReprPCClass = { reprPrec := instReprPCClass.repr }

def instReprPCClass.repr : PCClass → ℕ → Std.Format

Equations

• instReprPCClass.repr PCClass.dimension prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.dimension")).group prec✝
• instReprPCClass.repr PCClass.age prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.age")).group prec✝
• instReprPCClass.repr PCClass.value prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.value")).group prec✝
• instReprPCClass.repr PCClass.color prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.color")).group prec✝
• instReprPCClass.repr PCClass.physicalProperty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.physicalProperty")).group prec✝
• instReprPCClass.repr PCClass.speed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PCClass.speed")).group prec✝

def instBEqPCClass.beq : PCClass → PCClass → Bool

Equations

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

instance instBEqPCClass : BEq PCClass

Equations

• instBEqPCClass = { beq := instBEqPCClass.beq }

inductive ResultClass : Type

Result root subclasses (@cite{levin-1993}; @cite{beavers-etal-2021} ex. 6).

• entitySpecificCoS : ResultClass
• cooking : ResultClass
• breaking : ResultClass
• bending : ResultClass
• killing : ResultClass
• destroying : ResultClass
• calibratableCoS : ResultClass
• inherentlyDirectedMotion : ResultClass

instance instDecidableEqResultClass : DecidableEq ResultClass

Equations

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

instance instReprResultClass : Repr ResultClass

Equations

• instReprResultClass = { reprPrec := instReprResultClass.repr }

def instReprResultClass.repr : ResultClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprResultClass.repr ResultClass.entitySpecificCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.entitySpecificCoS")).group prec✝
• instReprResultClass.repr ResultClass.cooking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.cooking")).group prec✝
• instReprResultClass.repr ResultClass.breaking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.breaking")).group prec✝
• instReprResultClass.repr ResultClass.bending prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.bending")).group prec✝
• instReprResultClass.repr ResultClass.killing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.killing")).group prec✝
• instReprResultClass.repr ResultClass.destroying prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.destroying")).group prec✝
• instReprResultClass.repr ResultClass.calibratableCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultClass.calibratableCoS")).group prec✝

def instBEqResultClass.beq : ResultClass → ResultClass → Bool

Equations

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

instance instBEqResultClass : BEq ResultClass

Equations

• instBEqResultClass = { beq := instBEqResultClass.beq }

inductive ChangeRestriction : Type

How a result root's change entailment is restricted (B&@cite{beavers-koontz-garboden-2020} §2.4).

Break-type result roots (√CRACK, √SHATTER) entail change of ANY kind — spatial or temporal. A crack can "run from the tree to the house" without a temporal becoming event; the state itself extends spatially.

Cook/kill-type result roots (√COOK, √KILL) entail only TEMPORAL change. Cooking, killing, and melting are necessarily temporal processes. "✱The meat cooked from the oven to the table" is ruled out.

This three-way refinement (PC / break-type / cook-type) is invisible to the binary entailsChange flag but has consequences for spatial predication and the interpretation of directional PPs (B&@cite{beavers-koontz-garboden-2020} §2.4).

• anyChange : ChangeRestriction
• temporalOnly : ChangeRestriction

instance instDecidableEqChangeRestriction : DecidableEq ChangeRestriction

Equations

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

def instReprChangeRestriction.repr : ChangeRestriction → ℕ → Std.Format

Equations

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

instance instReprChangeRestriction : Repr ChangeRestriction

Equations

• instReprChangeRestriction = { reprPrec := instReprChangeRestriction.repr }

instance instBEqChangeRestriction : BEq ChangeRestriction

Equations

• instBEqChangeRestriction = { beq := instBEqChangeRestriction.beq }

def instBEqChangeRestriction.beq : ChangeRestriction → ChangeRestriction → Bool

Equations

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

def ResultClass.changeRestriction : ResultClass → ChangeRestriction

Change restriction for each result root subclass. Breaking/bending roots and directed motion allow spatial change descriptions; cooking/killing/destroying/scalar-change roots are temporally restricted.

Equations

• ResultClass.breaking.changeRestriction = ChangeRestriction.anyChange
• ResultClass.bending.changeRestriction = ChangeRestriction.anyChange
• ResultClass.inherentlyDirectedMotion.changeRestriction = ChangeRestriction.anyChange
• ResultClass.entitySpecificCoS.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.cooking.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.killing.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.destroying.changeRestriction = ChangeRestriction.temporalOnly
• ResultClass.calibratableCoS.changeRestriction = ChangeRestriction.temporalOnly

theorem breaking_allows_spatial : ResultClass.breaking.changeRestriction = ChangeRestriction.anyChange

Breaking roots allow spatial change: "The road cracked from the tree to the house."

theorem cooking_temporal_only : ResultClass.cooking.changeRestriction = ChangeRestriction.temporalOnly

Cooking roots restrict to temporal change: "✱The meat cooked from A to B."

def RootType.hasSimpleStative : RootType → Bool

PC roots have simple (unmarked) stative forms; result roots lack them.

Crosslinguistic evidence (§6, Fig. 1): PC median = 95.67% of languages have simple statives; result median = 1.59% (Mann-Whitney U = 1266.5, p < 0.001, n₁ = n₂ = 36).

English: "bright" (PC, simple adj) vs *"shattered" requires prior change.

Equations

• RootType.propertyConcept.hasSimpleStative = true
• RootType.result.hasSimpleStative = false

def RootType.verbalFormIsMarked : RootType → Bool

PC root verbs are morphologically marked (deadjectival: wid-en, flat-ten); result root verbs are unmarked (basic verbs: break, crack, shatter).

Crosslinguistic evidence (§7, Fig. 5): PC median = 56.01% marked; result median = 15.20% (U = 1291, p < 0.001).

Equations

• RootType.propertyConcept.verbalFormIsMarked = true
• RootType.result.verbalFormIsMarked = false

def RootType.allowsRestitutiveAgain : RootType → Bool

PC roots allow restitutive 'again' (scope over root only); result roots allow only repetitive 'again' (scope over BECOME).

§3.4: "John sharpened the knife again" allows restitutive reading (could be just one sharpening), but "#Chris thawed the meat again" in a restitutive context is unacceptable (necessarily two defrostings).

Under the analysis in §3.6: 'again' can target √ROOT. For PC roots, this yields a restitutive reading (return to prior state without prior change). For result roots, since the root itself entails change, 'again' over the root still entails a prior change event.

Equations

• RootType.propertyConcept.allowsRestitutiveAgain = true
• RootType.result.allowsRestitutiveAgain = false

theorem semantic_determines_morphosyntax (rt : RootType) : rt.entailsChange = true ↔ rt.hasSimpleStative = false ∧ rt.verbalFormIsMarked = false ∧ rt.allowsRestitutiveAgain = false

The main theorem of @cite{beavers-etal-2021}.

A root's entailment of change determines ALL of its morphosyntactic behavior in a single four-way biconditional. This is the paper's deepest result: four independently testable properties form a perfect correlation package.

For result roots (entailsChange = true):

• No simple stative forms (§6)
• Unmarked verbal forms (§7)
• No restitutive 'again' — only repetitive (§3.4)

For PC roots (entailsChange = false):

• Simple stative forms exist (§6)
• Marked verbal forms (§7)
• Restitutive 'again' available (§3.4)

This correlation holds crosslinguistically (88 languages, §§4–7) and refutes the Bifurcation Thesis: if roots couldn't introduce templatic meaning (change), there would be NO semantic basis for the morphological and syntactic correlations.

theorem pc_determines_morphosyntax (rt : RootType) : rt.entailsChange = false ↔ rt.hasSimpleStative = true ∧ rt.verbalFormIsMarked = true ∧ rt.allowsRestitutiveAgain = true

The converse: NOT entailing change determines the opposite package.

def bifurcationThesis (rootEntailsChange : RootType → Bool) : Prop

The Bifurcation Thesis for Roots (@cite{embick-2009}:1, @cite{arad-2005}:79; @cite{beavers-etal-2021} eq. 2):

"If a component of meaning is introduced by a semantic rule that applies to elements in combination [i.e. by templatic operators], then that component of meaning cannot be part of the meaning of a [lexical semantic] root."

Under bifurcation, change (= BECOME) is introduced only by templates, never by roots. Therefore NO root should entail change.

Equations

• bifurcationThesis rootEntailsChange = ∀ (rt : RootType), rootEntailsChange rt = false

theorem bifurcation_fails : ¬bifurcationThesis RootType.entailsChange

@cite{beavers-etal-2021} main result: bifurcation does not hold. Result roots entail change, violating the thesis (§§3.3, 3.6, 9).

theorem result_roots_witness_against_bifurcation : RootType.result.entailsChange = true

Corollary: result roots are a witness to bifurcation failure.

theorem pc_roots_consistent_with_bifurcation : RootType.propertyConcept.entailsChange = false

PC roots are consistent with bifurcation (they don't entail change).

theorem bkg_bifurcation_fails_all_dimensions : RootEntailments.fullSpec.result = true ∧ RootEntailments.fullSpec.cause = true ∧ RootEntailments.fullSpec.manner = true ∧ RootEntailments.fullSpec.state = true

B&@cite{beavers-koontz-garboden-2020} strengthened bifurcation failure via RootEntailments.

@cite{beavers-etal-2021} show roots can entail CHANGE (one templatic notion). B&@cite{beavers-koontz-garboden-2020} show roots can entail CHANGE, CAUSATION, and MANNER — ALL notions traditionally reserved for templates. This is a strictly stronger refutation: even if one accepted that change is "special", roots encoding manner+cause (√GUILLOTINE, √HAND) violate bifurcation on three separate dimensions simultaneously.

Witness: RootEntailments.fullSpec has all four features true.

theorem bkg_bifurcation_multiple_witnesses : LevinClass.cut.rootEntailments.result = true ∧ LevinClass.cut.rootEntailments.manner = true ∧ LevinClass.give.rootEntailments.cause = true ∧ LevinClass.give.rootEntailments.manner = true

Multiple Levin classes witness the stronger bifurcation failure.

inductive Markedness : Type

Whether a form is morphologically marked (=derived/complex) or unmarked (=basic/simple).

• unmarked : Markedness
• marked : Markedness

instance instDecidableEqMarkedness : DecidableEq Markedness

Equations

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

instance instReprMarkedness : Repr Markedness

Equations

• instReprMarkedness = { reprPrec := instReprMarkedness.repr }

def instReprMarkedness.repr : Markedness → ℕ → Std.Format

Equations

• instReprMarkedness.repr Markedness.unmarked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Markedness.unmarked")).group prec✝
• instReprMarkedness.repr Markedness.marked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Markedness.marked")).group prec✝

def instBEqMarkedness.beq : Markedness → Markedness → Bool

Equations

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

instance instBEqMarkedness : BEq Markedness

Equations

• instBEqMarkedness = { beq := instBEqMarkedness.beq }

def verbalMarkedness (rt : RootType) : Markedness

The Markedness Generalization (@cite{beavers-etal-2021} eq. 44).

Morphological markedness reflects semantic mismatch between a functional head and its root complement. A form is unmarked when the head's semantic contribution is REDUNDANT with the root's meaning:

(a) Default realization of v_become with complement √ROOT: - If √ROOT entails change → v_become is redundant → UNMARKED verb - If √ROOT does not entail change → v_become adds content → MARKED verb

(b) Default realization of Asp_{S/R} with complement X: - If X does not entail change → already stative → UNMARKED stative - If X entails change → change must be stripped → MARKED stative

This explains three attested language types:

1. English-type: markedness asymmetry realized overtly (-en, -ed)
2. Equipollent: both marked (high-marking languages like Hebrew)
3. Labile: neither marked (low-marking languages like Kinyarwanda)

And rules out the unattested fourth type (where the markedness pattern is the inverse of what the generalization predicts).

Equations

• verbalMarkedness rt = if rt.entailsChange = true then Markedness.unmarked else Markedness.marked

def stativeMarkedness (rt : RootType) : Markedness

Stative markedness is the mirror image of verbal markedness.

Equations

• stativeMarkedness rt = if rt.entailsChange = true then Markedness.marked else Markedness.unmarked

theorem markedness_complementarity (rt : RootType) : verbalMarkedness rt ≠ stativeMarkedness rt

Verbal and stative markedness are always complementary.

theorem result_root_unmarked_verb : verbalMarkedness RootType.result = Markedness.unmarked

Result roots produce unmarked verbs.

theorem pc_root_marked_verb : verbalMarkedness RootType.propertyConcept = Markedness.marked

PC roots produce marked verbs.

theorem result_root_marked_stative : stativeMarkedness RootType.result = Markedness.marked

Result roots produce marked statives.

theorem pc_root_unmarked_stative : stativeMarkedness RootType.propertyConcept = Markedness.unmarked

PC roots produce unmarked statives.

theorem markedness_from_semantics (rt : RootType) : verbalMarkedness rt = Markedness.unmarked ↔ rt.entailsChange = true

The markedness generalization is equivalent to the semantic distinction.

@[reducible, inline]

abbrev RootDenotation (Entity State : Type) : Type

A root's denotation: a state predicate over entities and states. @cite{beavers-etal-2021} eq. 20a: ⟦√FLAT⟧ = λx.λs[flat'(x, s)].

Equations

• RootDenotation Entity State = (Entity → State → Prop)

def MeaningPostulateEntailsChange {Entity State Event : Type} (rootPred : RootDenotation Entity State) (become : Event → State → Prop) : Prop

A meaning postulate: the root's state predicate entails a prior change event. @cite{beavers-etal-2021} eq. 21a: ∀x.∀s[cracked'(x, s) → ∃e'[become'(e', s)]].

Equations

• MeaningPostulateEntailsChange rootPred become = ∀ (x : Entity) (s : State), rootPred x s → ∃ (e : Event), become e s

inductive RootDen (Entity State Event : Type) : Type

Root denotation architecture (B&@cite{beavers-koontz-garboden-2020} §2.5, eqs. 37a–b), where change is CONSTITUTIVE of the result root's meaning rather than an external meaning postulate (cf. @cite{beavers-etal-2021} eq. 21).

The formal contrast:

• √FLAT = λxλs[flat'(x,s)] — pure state, no change in truth conditions
• √CRACK = λxλs[cracked'(x,s) ∧ ∃e'[become'(s,e')]] — change IN the root

The earlier @cite{beavers-etal-2021} analysis used a separate structure with an external meaning postulate constraining result roots. B&KG argue the change IS what the root means, not an external constraint.

The empirical payoff: the again diagnostic's reading collapse for result roots (§12b below) follows logically from this architecture. If change is in the root, scoping again over root vs. over vP yields the same presupposition — explaining the collapse without stipulation.

• pc {Entity State Event : Type} (statePred : Entity → State → Prop) : RootDen Entity State Event

  PC root: pure state predicate. The state can hold without prior change. √FLAT = λxλs[flat'(x,s)] — "the table is flat" doesn't presuppose any prior flattening event.

• result {Entity State Event : Type} (statePred : Entity → State → Prop) (become : Event → State → Prop) (entailsChange : ∀ (x : Entity) (s : State), statePred x s → ∃ (e : Event), become e s) : RootDen Entity State Event

  Result root: state predicate constitutively entailing change. √CRACK = λxλs[cracked'(x,s) ∧ ∃e'[become'(s,e')]] The existential over becoming events is PART OF the root's truth conditions, not a separate meaning postulate.

• mannerResult {Entity State Event : Type} (statePred : Entity → State → Prop) (become : Event → State → Prop) (manner : Event → Prop) (entailsChange : ∀ (x : Entity) (s : State), statePred x s → ∃ (e : Event), become e s) (entailsManner : ∀ (x : Entity) (s : State), statePred x s → ∃ (v : Event), manner v) : RootDen Entity State Event

  Manner+result root: state predicate entailing change AND manner restriction on the causing event (B&@cite{beavers-koontz-garboden-2020} §4.5.3, eq. 74). √GUILLOTINE = λxλs[dead'(x,s) ∧ ∃e'∃v[cause'(v,e') ∧ become'(s,e') ∧ ∀v'[cause'(v',e') → guillotining'(v')]]] The root packages both the result state AND a restriction on how that result is brought about. This violates Manner/Result Complementarity — manner and result coexist in one root.

def RootDen.rootType {Entity State Event : Type} : RootDen Entity State Event → RootType

Extract the RootType from a BKG denotation. Manner+result roots map to .result at the Boolean level — they entail change, which is all the Chapter 2 typology cares about. The manner dimension is only visible at the denotation level.

Equations

• (RootDen.pc statePred).rootType = RootType.propertyConcept
• (RootDen.result statePred become entailsChange).rootType = RootType.result
• (RootDen.mannerResult statePred become manner entailsChange entailsManner).rootType = RootType.result

def RootDen.statePred {Entity State Event : Type} : RootDen Entity State Event → Entity → State → Prop

Extract the underlying state predicate from any root type.

Equations

• (RootDen.pc statePred).statePred = statePred
• (RootDen.result statePred become entailsChange).statePred = statePred
• (RootDen.mannerResult statePred become manner entailsChange entailsManner).statePred = statePred

def RootDen.carriesBECOME {Entity State Event : Type} : RootDen Entity State Event → Bool

Whether the root carries its own BECOME relation (built into the denotation).

Equations

• (RootDen.pc statePred).carriesBECOME = false
• (RootDen.result statePred become entailsChange).carriesBECOME = true
• (RootDen.mannerResult statePred become manner entailsChange entailsManner).carriesBECOME = true

theorem RootDen.carriesBECOME_iff_entailsChange {Entity State Event : Type} (rd : RootDen Entity State Event) : rd.carriesBECOME = rd.rootType.entailsChange

Carrying BECOME built-in is the same as entailing change. This connects the denotation architecture to the Boolean flag.

theorem RootDen.meaning_postulate_derived {Entity State Event : Type} (pred : Entity → State → Prop) (become : Event → State → Prop) (h : ∀ (x : Entity) (s : State), pred x s → ∃ (e : Event), become e s) : MeaningPostulateEntailsChange pred become

For result roots, the meaning postulate is DERIVED from the denotation — not a separate axiom. This is the formal content of B&KG's argument: change isn't externally constrained — it's what the root means.

def RootDen.carriesMANNER {Entity State Event : Type} : RootDen Entity State Event → Bool

Whether the root carries a manner restriction on causation (B&@cite{beavers-koontz-garboden-2020} §4.5.3). Only manner+result roots have this — PC and pure result roots do not restrict how causation proceeds.

Equations

• (RootDen.pc statePred).carriesMANNER = false
• (RootDen.result statePred become entailsChange).carriesMANNER = false
• (RootDen.mannerResult statePred become manner entailsChange entailsManner).carriesMANNER = true

def RootDen.denotationViolatesMRC {Entity State Event : Type} (rd : RootDen Entity State Event) : Bool

A root denotation violates MRC iff it carries both BECOME and a manner restriction — i.e., it encodes both result and manner in one root. Derived from the two independent predicates, not pattern-matched separately.

Equations

• rd.denotationViolatesMRC = (rd.carriesBECOME && rd.carriesMANNER)

theorem RootDen.mannerResult_violates {Entity State Event : Type} (sp : Entity → State → Prop) (become : Event → State → Prop) (manner : Event → Prop) (hc : ∀ (x : Entity) (s : State), sp x s → ∃ (e : Event), become e s) (hm : ∀ (x : Entity) (s : State), sp x s → ∃ (v : Event), manner v) : (mannerResult sp become manner hc hm).denotationViolatesMRC = true

Manner+result denotations violate MRC.

theorem RootDen.result_respects {Entity State Event : Type} (sp : Entity → State → Prop) (become : Event → State → Prop) (hc : ∀ (x : Entity) (s : State), sp x s → ∃ (e : Event), become e s) : (result sp become hc).denotationViolatesMRC = false

Result-only denotations respect MRC.

theorem RootDen.pc_respects {Entity State Event : Type} (sp : Entity → State → Prop) : (pc sp).denotationViolatesMRC = false

PC denotations respect MRC.

theorem RootDen.mrc_requires_both {Entity State Event : Type} (rd : RootDen Entity State Event) (h : rd.denotationViolatesMRC = true) : rd.carriesBECOME = true ∧ rd.carriesMANNER = true

Bridge: denotation-level MRC → Boolean RootEntailments MRC. MRC violation requires BOTH conditions — having manner alone (if such a constructor existed) would not be a violation.

inductive PossessionEntailment : Type

What a ditransitive root entails about possession (B&@cite{beavers-koontz-garboden-2020} §3.3). Templates always introduce PROSPECTIVE possession (via ◇ modality). Whether the ROOT adds actual or prospective possession on top determines cancellability: "gave X the ball, #but X never had it" vs. "sent X the ball, but it never arrived" (OK).

• none : PossessionEntailment
• prospective : PossessionEntailment
• actual : PossessionEntailment

instance instDecidableEqPossessionEntailment : DecidableEq PossessionEntailment

Equations

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

instance instReprPossessionEntailment : Repr PossessionEntailment

Equations

• instReprPossessionEntailment = { reprPrec := instReprPossessionEntailment.repr }

def instReprPossessionEntailment.repr : PossessionEntailment → ℕ → Std.Format

Equations

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

def instBEqPossessionEntailment.beq : PossessionEntailment → PossessionEntailment → Bool

Equations

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

instance instBEqPossessionEntailment : BEq PossessionEntailment

Equations

• instBEqPossessionEntailment = { beq := instBEqPossessionEntailment.beq }

inductive DitransitiveRootClass : Type

Six classes of ditransitive verb roots (B&@cite{beavers-koontz-garboden-2020} §3.6). The ditransitive parallel to the PC/result distinction for CoS roots: templates contribute only PROSPECTIVE states; roots can contribute ACTUAL states.

• causedPossession : DitransitiveRootClass
• futureHaving : DitransitiveRootClass
• ballisticMotion : DitransitiveRootClass
• sending : DitransitiveRootClass
• accompaniedMotion : DitransitiveRootClass
• carrying : DitransitiveRootClass

instance instDecidableEqDitransitiveRootClass : DecidableEq DitransitiveRootClass

Equations

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

instance instReprDitransitiveRootClass : Repr DitransitiveRootClass

Equations

• instReprDitransitiveRootClass = { reprPrec := instReprDitransitiveRootClass.repr }

def instReprDitransitiveRootClass.repr : DitransitiveRootClass → ℕ → Std.Format

Equations

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

def instBEqDitransitiveRootClass.beq : DitransitiveRootClass → DitransitiveRootClass → Bool

Equations

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

instance instBEqDitransitiveRootClass : BEq DitransitiveRootClass

Equations

• instBEqDitransitiveRootClass = { beq := instBEqDitransitiveRootClass.beq }

structure DitransitiveEntailments : Type

What a ditransitive root entails about the transfer event. Each field is a distinct semantic entailment from the ROOT, independent of what the template provides.

• possession : PossessionEntailment
• causedMotion : Bool
• manner : Bool
• accompaniment : Bool

instance instDecidableEqDitransitiveEntailments : DecidableEq DitransitiveEntailments

Equations

• instDecidableEqDitransitiveEntailments = instDecidableEqDitransitiveEntailments.decEq

def instDecidableEqDitransitiveEntailments.decEq (x✝ x✝¹ : DitransitiveEntailments) : Decidable (x✝ = x✝¹)

Equations

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

def instBEqDitransitiveEntailments.beq : DitransitiveEntailments → DitransitiveEntailments → Bool

Equations

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

instance instBEqDitransitiveEntailments : BEq DitransitiveEntailments

Equations

• instBEqDitransitiveEntailments = { beq := instBEqDitransitiveEntailments.beq }

instance instReprDitransitiveEntailments : Repr DitransitiveEntailments

Equations

• instReprDitransitiveEntailments = { reprPrec := instReprDitransitiveEntailments.repr }

def instReprDitransitiveEntailments.repr : DitransitiveEntailments → ℕ → Std.Format

Equations

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

def DitransitiveRootClass.entailments : DitransitiveRootClass → DitransitiveEntailments

Entailment profile for each ditransitive root class (B&@cite{beavers-koontz-garboden-2020} §3.6).

Equations

• DitransitiveRootClass.causedPossession.entailments = { possession := PossessionEntailment.actual, causedMotion := false, manner := false, accompaniment := false }
• DitransitiveRootClass.futureHaving.entailments = { possession := PossessionEntailment.prospective, causedMotion := false, manner := false, accompaniment := false }
• DitransitiveRootClass.ballisticMotion.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := true, accompaniment := false }
• DitransitiveRootClass.sending.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := false, accompaniment := false }
• DitransitiveRootClass.accompaniedMotion.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := false, accompaniment := true }
• DitransitiveRootClass.carrying.entailments = { possession := PossessionEntailment.none, causedMotion := true, manner := true, accompaniment := true }

theorem give_entails_actual_possession : DitransitiveRootClass.causedPossession.entailments.possession = PossessionEntailment.actual

√GIVE entails actual possession — "Kim gave Sandy the ball, #but Sandy never had it" is contradictory (§3.3, ex. 17).

theorem send_no_possession : DitransitiveRootClass.sending.entailments.possession = PossessionEntailment.none

√SEND does NOT entail possession — "Kim sent Sandy the ball, but it never arrived" is felicitous (§3.3, ex. 18).

theorem promise_prospective : DitransitiveRootClass.futureHaving.entailments.possession = PossessionEntailment.prospective

√PROMISE entails only prospective possession.

theorem throw_manner_motion : have e := DitransitiveRootClass.ballisticMotion.entailments; e.possession = PossessionEntailment.none ∧ e.causedMotion = true ∧ e.manner = true

√THROW entails manner + caused motion but not possession.

theorem bring_accompaniment : DitransitiveRootClass.accompaniedMotion.entailments.accompaniment = true

√BRING entails accompaniment — agent travels with theme.

theorem carry_manner_accompaniment : have e := DitransitiveRootClass.carrying.entailments; e.manner = true ∧ e.accompaniment = true ∧ e.possession = PossessionEntailment.none

√CARRY entails manner + accompaniment but not possession.

def LevinClass.ditransitiveRootClass : LevinClass → Option DitransitiveRootClass

Bridge to LevinClass: ditransitive Levin classes → root classes.

Equations

• LevinClass.give.ditransitiveRootClass = some DitransitiveRootClass.causedPossession
• LevinClass.contribute.ditransitiveRootClass = some DitransitiveRootClass.causedPossession
• LevinClass.exchange.ditransitiveRootClass = some DitransitiveRootClass.causedPossession
• LevinClass.throw.ditransitiveRootClass = some DitransitiveRootClass.ballisticMotion
• LevinClass.send.ditransitiveRootClass = some DitransitiveRootClass.sending
• LevinClass.carry.ditransitiveRootClass = some DitransitiveRootClass.carrying
• x✝.ditransitiveRootClass = none

theorem give_class_causedPossession : LevinClass.give.ditransitiveRootClass = some DitransitiveRootClass.causedPossession

theorem throw_class_ballisticMotion : LevinClass.throw.ditransitiveRootClass = some DitransitiveRootClass.ballisticMotion

theorem send_class_sending : LevinClass.send.ditransitiveRootClass = some DitransitiveRootClass.sending

theorem carry_class_carrying : LevinClass.carry.ditransitiveRootClass = some DitransitiveRootClass.carrying

inductive DitransitiveDen (Entity Event : Type) : Type

A ditransitive root's denotation (B&@cite{beavers-koontz-garboden-2020} §3.5, eqs. 46–55). Parallel to RootDen for CoS roots (§7b).

The formal contrast:

• √SEND = λyλzλe[send'(y,z,e)] — event predicate only
• √GIVE = λyλzλe[give'(y,z,e) ∧ have'(z,y)] — possession IN the root

Templates always add prospective possession (via ◇). Whether the root ALSO adds actual possession determines cancellation behavior, telicity, and again readings — the same architecture as CoS roots with BECOME.

• simple {Entity Event : Type} (eventPred : Entity → Entity → Event → Prop) : DitransitiveDen Entity Event

  Root WITHOUT possession entailment. Like PC roots for CoS: the template provides the (prospective) possession.

• withPossession {Entity Event : Type} (eventPred : Entity → Entity → Event → Prop) (possess : Entity → Entity → Prop) (entailsPoss : ∀ (y z : Entity) (e : Event), eventPred y z e → possess z y) : DitransitiveDen Entity Event

  Root WITH actual possession entailment. Like result roots for CoS: possession is IN the root's truth conditions. The entailsPoss proof is constitutive — not a meaning postulate.

def DitransitiveDen.possessionCancelable {Entity Event : Type} : DitransitiveDen Entity Event → Bool

Whether possession is cancelable for a verb with this root. Root-entailed actual possession is NOT cancelable; template-only prospective possession IS cancelable.

Structural parallel to RootDen.carriesBECOME: root-constitutive content cannot be canceled in either domain.

Equations

• (DitransitiveDen.simple eventPred).possessionCancelable = true
• (DitransitiveDen.withPossession eventPred possess entailsPoss).possessionCancelable = false

theorem simple_possession_cancelable {Entity Event : Type} (ep : Entity → Entity → Event → Prop) : (DitransitiveDen.simple ep).possessionCancelable = true

A send-type denotation (simple) has cancelable possession.

theorem withPossession_not_cancelable {Entity Event : Type} (ep : Entity → Entity → Event → Prop) (poss : Entity → Entity → Prop) (h : ∀ (y z : Entity) (e : Event), ep y z e → poss z y) : (DitransitiveDen.withPossession ep poss h).possessionCancelable = false

A give-type denotation (withPossession) has uncancelable possession.

inductive MRCDiagnostic : Type

The six MRC diagnostics developed in B&KG (2020 §§4.2–4.3). Three test for result entailment in the root; three test for manner. An MRC violation is a verb that passes diagnostics from BOTH sets.

Result diagnostics (§4.2):

• denialOfResult: "X cut Y, #but Y wasn't separated" — contradictory
• objectDeletion: result verbs resist unspecified object deletion
• restrictedResultatives: result verbs block adding new result XPs

Manner diagnostics (§4.3):

• selectionalRestriction: subject restricted to agents capable of the manner
• denialOfAction: "X cut Y, #but X didn't do anything" — contradictory
• actorParaphrase: paraphrasable as "X did manner to Y" (§4.3)

• denialOfResult : MRCDiagnostic
• objectDeletion : MRCDiagnostic
• restrictedResultatives : MRCDiagnostic
• selectionalRestriction : MRCDiagnostic
• denialOfAction : MRCDiagnostic
• actorParaphrase : MRCDiagnostic

instance instDecidableEqMRCDiagnostic : DecidableEq MRCDiagnostic

Equations

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

def instReprMRCDiagnostic.repr : MRCDiagnostic → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprMRCDiagnostic.repr MRCDiagnostic.denialOfResult prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.denialOfResult")).group prec✝
• instReprMRCDiagnostic.repr MRCDiagnostic.objectDeletion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.objectDeletion")).group prec✝
• instReprMRCDiagnostic.repr MRCDiagnostic.denialOfAction prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.denialOfAction")).group prec✝
• instReprMRCDiagnostic.repr MRCDiagnostic.actorParaphrase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MRCDiagnostic.actorParaphrase")).group prec✝

instance instReprMRCDiagnostic : Repr MRCDiagnostic

Equations

• instReprMRCDiagnostic = { reprPrec := instReprMRCDiagnostic.repr }

instance instBEqMRCDiagnostic : BEq MRCDiagnostic

Equations

• instBEqMRCDiagnostic = { beq := instBEqMRCDiagnostic.beq }

def instBEqMRCDiagnostic.beq : MRCDiagnostic → MRCDiagnostic → Bool

Equations

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

def MRCDiagnostic.testsResult : MRCDiagnostic → Bool

Whether a diagnostic tests for result entailment.

Equations

• MRCDiagnostic.denialOfResult.testsResult = true
• MRCDiagnostic.objectDeletion.testsResult = true
• MRCDiagnostic.restrictedResultatives.testsResult = true
• x✝.testsResult = false

def MRCDiagnostic.testsManner : MRCDiagnostic → Bool

Whether a diagnostic tests for manner entailment.

Equations

• MRCDiagnostic.selectionalRestriction.testsManner = true
• MRCDiagnostic.denialOfAction.testsManner = true
• MRCDiagnostic.actorParaphrase.testsManner = true
• x✝.testsManner = false

theorem diagnostic_exclusive (d : MRCDiagnostic) : d.testsResult = !d.testsManner

Each diagnostic tests for exactly one of manner or result.

structure MRCDiagnosticProfile : Type

A verb's diagnostic profile: which of the six diagnostics it passes. B&KG (2020 §§4.2–4.3) survey these for each verb class.

• denialOfResult : Bool
• objectDeletion : Bool
• restrictedResultatives : Bool
• selectionalRestriction : Bool
• denialOfAction : Bool
• actorParaphrase : Bool

def instDecidableEqMRCDiagnosticProfile.decEq (x✝ x✝¹ : MRCDiagnosticProfile) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqMRCDiagnosticProfile : DecidableEq MRCDiagnosticProfile

Equations

• instDecidableEqMRCDiagnosticProfile = instDecidableEqMRCDiagnosticProfile.decEq

instance instBEqMRCDiagnosticProfile : BEq MRCDiagnosticProfile

Equations

• instBEqMRCDiagnosticProfile = { beq := instBEqMRCDiagnosticProfile.beq }

def instBEqMRCDiagnosticProfile.beq : MRCDiagnosticProfile → MRCDiagnosticProfile → Bool

Equations

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

instance instReprMRCDiagnosticProfile : Repr MRCDiagnosticProfile

Equations

• instReprMRCDiagnosticProfile = { reprPrec := instReprMRCDiagnosticProfile.repr }

def instReprMRCDiagnosticProfile.repr : MRCDiagnosticProfile → ℕ → Std.Format

Equations

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

def MRCDiagnosticProfile.showsResult (p : MRCDiagnosticProfile) : Bool

Whether the profile shows result entailment (passes ≥1 result diagnostic).

Equations

• p.showsResult = (p.denialOfResult || p.objectDeletion || p.restrictedResultatives)

def MRCDiagnosticProfile.showsManner (p : MRCDiagnosticProfile) : Bool

Whether the profile shows manner entailment (passes ≥1 manner diagnostic).

Equations

• p.showsManner = (p.selectionalRestriction || p.denialOfAction || p.actorParaphrase)

def MRCDiagnosticProfile.showsMRCViolation (p : MRCDiagnosticProfile) : Bool

An MRC violation is a verb whose diagnostics show BOTH manner and result.

Equations

• p.showsMRCViolation = (p.showsManner && p.showsResult)

def cutDiagnostics : MRCDiagnosticProfile

Cut passes all 6 diagnostics (B&KG §4.4): manner of cutting + separation. "Kim cut the bread, #but the bread wasn't separated" (result) "Kim cut the bread, #but Kim didn't do anything" (manner)

Equations

• cutDiagnostics = { denialOfResult := true, objectDeletion := true, restrictedResultatives := true, selectionalRestriction := true, denialOfAction := true, actorParaphrase := true }

def breakDiagnostics : MRCDiagnosticProfile

Break passes result diagnostics only: pure result (√CRACK), no manner.

Equations

• breakDiagnostics = { denialOfResult := true, objectDeletion := true, restrictedResultatives := true, selectionalRestriction := false, denialOfAction := false, actorParaphrase := false }

def hitDiagnostics : MRCDiagnosticProfile

Hit passes manner diagnostics only: pure manner (impact), no result.

Equations

• hitDiagnostics = { denialOfResult := false, objectDeletion := false, restrictedResultatives := false, selectionalRestriction := true, denialOfAction := true, actorParaphrase := true }

def drownDiagnostics : MRCDiagnosticProfile

Drown passes all 6 (B&KG §4.5): manner of drowning + death result.

Equations

• drownDiagnostics = { denialOfResult := true, objectDeletion := true, restrictedResultatives := true, selectionalRestriction := true, denialOfAction := true, actorParaphrase := true }

theorem cut_MRC_violation : cutDiagnostics.showsMRCViolation = true

theorem break_no_MRC_violation : breakDiagnostics.showsMRCViolation = false

theorem hit_no_MRC_violation : hitDiagnostics.showsMRCViolation = false

theorem drown_MRC_violation : drownDiagnostics.showsMRCViolation = true

theorem cut_diagnostics_match_entailments : cutDiagnostics.showsMRCViolation = LevinClass.cut.rootEntailments.violatesMRC

Cut is MRC-violating by BOTH diagnostics AND RootEntailments.

theorem break_diagnostics_match_entailments : breakDiagnostics.showsMRCViolation = LevinClass.break_.rootEntailments.violatesMRC

Break is MRC-respecting by BOTH diagnostics AND RootEntailments.

theorem hit_diagnostics_match_entailments : hitDiagnostics.showsMRCViolation = LevinClass.hit.rootEntailments.violatesMRC

Hit is MRC-respecting by BOTH diagnostics AND RootEntailments.

def rootTypeFromChangeEntailment (p : Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile) : RootType

Dowty's P-Patient entailment (a) "undergoes change of state" is precisely the result root entailment. An object bearing a result root's state predicate has changeOfState = true.

This bridges the root typology to the entailment profile via the shared property.

Equations

• rootTypeFromChangeEntailment p = if p.changeOfState = true then RootType.result else RootType.propertyConcept

theorem result_object_has_changeOfState : rootTypeFromChangeEntailment Semantics.Lexical.Verb.EntailmentProfile.kickObjectProfile = RootType.result

A result root's object has changeOfState = true.

theorem die_result_pattern : rootTypeFromChangeEntailment Semantics.Lexical.Verb.EntailmentProfile.dieSubjectProfile = RootType.result

Die subject undergoes change → result-type pattern.

def RootType.requiresBECOME : RootType → Bool

Result roots MUST combine with a template containing BECOME (achievement or accomplishment), because the root's change entailment is semantically redundant with BECOME.

PC roots CAN combine with any template — with BECOME (achievement/ accomplishment) they get change compositionally; without it (state) they denote simple states.

Equations

• RootType.result.requiresBECOME = true
• RootType.propertyConcept.requiresBECOME = false

theorem result_root_gets_become_template : RootType.result.requiresBECOME = true

Result roots always get templates with BECOME.

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

Achievement and accomplishment templates contain BECOME.

Equations

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

theorem result_templates_have_become : Template.hasBECOME Semantics.Lexical.Verb.EventStructure.Template.achievement = true ∧ Template.hasBECOME Semantics.Lexical.Verb.EventStructure.Template.accomplishment = true

The templates result roots combine with always have BECOME.

theorem state_template_no_become : Template.hasBECOME Semantics.Lexical.Verb.EventStructure.Template.state = false

State template lacks BECOME — only available to PC roots.

theorem become_templates_telic : Semantics.Lexical.Verb.EventStructure.Template.achievement.vendlerClass = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement ∧ Semantics.Lexical.Verb.EventStructure.Template.accomplishment.vendlerClass = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.accomplishment

Bridge: templates with BECOME map to achievement/accomplishment Vendler classes, both of which are telic (bounded by the result state). This connects the template operator to the existing aspectual profile.

def RootType.stativeAspectualProfile : RootType → Semantics.Tense.Aspect.LexicalAspect.AspectualProfile

Aspectual profile for root types in their stative use.

Equations

• RootType.propertyConcept.stativeAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.stateProfile
• RootType.result.stativeAspectualProfile = Semantics.Tense.Aspect.LexicalAspect.achievementProfile

def RootType.stativeVendlerClass (rt : RootType) : Semantics.Tense.Aspect.LexicalAspect.VendlerClass

Result root verbs are typically achievements or accomplishments (they have BECOME in their template). PC root verbs in their inchoative (change-of-state) use are also achievements/accomplishments, but their stative use is a state (derived from profile).

Equations

• rt.stativeVendlerClass = rt.stativeAspectualProfile.toVendlerClass

theorem root_stative_vendler : RootType.propertyConcept.stativeVendlerClass = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.state ∧ RootType.result.stativeVendlerClass = Semantics.Tense.Aspect.LexicalAspect.VendlerClass.achievement

PC roots in stative use are states; result roots pattern as achievements even in adjectival use (the state entails prior change).

inductive AdjectivalStructure : Type

@cite{embick-2004} posits two adjectival structures:

(8a) BASIC STATIVES: [AspP AspS √ROOT] Simple adjective directly combining with stativizer. Only available to PC roots.

(8b) RESULT STATIVES: [AspP AspR [vP DP v_become √ROOT]] Deverbal adjective containing v_become. Available to result roots; superficially also to PC roots.

Under the non-bifurcated analysis, result root adjectives are ALWAYS (8b) because the root requires v_become. PC root adjectives are (8a) by default but can also be (8b).

• basicStative : AdjectivalStructure
• resultStative : AdjectivalStructure

instance instDecidableEqAdjectivalStructure : DecidableEq AdjectivalStructure

Equations

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

def instReprAdjectivalStructure.repr : AdjectivalStructure → ℕ → Std.Format

Equations

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

instance instReprAdjectivalStructure : Repr AdjectivalStructure

Equations

• instReprAdjectivalStructure = { reprPrec := instReprAdjectivalStructure.repr }

instance instBEqAdjectivalStructure : BEq AdjectivalStructure

Equations

• instBEqAdjectivalStructure = { beq := instBEqAdjectivalStructure.beq }

def instBEqAdjectivalStructure.beq : AdjectivalStructure → AdjectivalStructure → Bool

Equations

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

def RootType.admitsBasicStative : RootType → Bool

PC roots admit both structures; result roots only admit resultStative.

Equations

• RootType.propertyConcept.admitsBasicStative = true
• RootType.result.admitsBasicStative = false

theorem admitsBasicStative_iff_no_change (rt : RootType) : rt.admitsBasicStative = true ↔ rt.entailsChange = false

This is equivalent to NOT entailing change.

inductive AgainReading : Type

Sublexical modifier 'again' has two readings:

(14a) RESTITUTIVE: again attaches to just the root → restores a prior state (one sharpening event) (14b) REPETITIVE: again attaches to the whole vP (including v_become) → repeats the entire change event (two sharpenings)

Under the non-bifurcated analysis:

• PC roots: again over √ROOT yields a pure state → restitutive OK
• Result roots: again over √ROOT still entails change (root has it) → restitutive reading collapses into repetitive

• restitutive : AgainReading
• repetitive : AgainReading

instance instDecidableEqAgainReading : DecidableEq AgainReading

Equations

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

def instReprAgainReading.repr : AgainReading → ℕ → Std.Format

Equations

• instReprAgainReading.repr AgainReading.restitutive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgainReading.restitutive")).group prec✝
• instReprAgainReading.repr AgainReading.repetitive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "AgainReading.repetitive")).group prec✝

instance instReprAgainReading : Repr AgainReading

Equations

• instReprAgainReading = { reprPrec := instReprAgainReading.repr }

def instBEqAgainReading.beq : AgainReading → AgainReading → Bool

Equations

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

instance instBEqAgainReading : BEq AgainReading

Equations

• instBEqAgainReading = { beq := instBEqAgainReading.beq }

def RootType.againReadings : RootType → List AgainReading

Which readings of 'again' are available for each root type.

Equations

• RootType.propertyConcept.againReadings = [AgainReading.restitutive, AgainReading.repetitive]
• RootType.result.againReadings = [AgainReading.repetitive]

theorem pc_more_again_readings : RootType.propertyConcept.againReadings.length > RootType.result.againReadings.length

PC roots have strictly more 'again' readings than result roots.

theorem result_no_restitutive : AgainReading.restitutive ∉ RootType.result.againReadings

Result roots lack the restitutive reading.

theorem pc_has_restitutive : AgainReading.restitutive ∈ RootType.propertyConcept.againReadings

PC roots have the restitutive reading.

inductive AgainPresupposition : Type

What again presupposes at a given scope position.

again is a presupposition trigger: attaching it to constituent C presupposes that C's denotation held at some prior time. The distinction between priorState and priorChange determines whether restitutive and repetitive readings are distinct or collapse into one.

• priorState : AgainPresupposition
• priorChange : AgainPresupposition

instance instDecidableEqAgainPresupposition : DecidableEq AgainPresupposition

Equations

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

instance instReprAgainPresupposition : Repr AgainPresupposition

Equations

• instReprAgainPresupposition = { reprPrec := instReprAgainPresupposition.repr }

def instReprAgainPresupposition.repr : AgainPresupposition → ℕ → Std.Format

Equations

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

instance instBEqAgainPresupposition : BEq AgainPresupposition

Equations

• instBEqAgainPresupposition = { beq := instBEqAgainPresupposition.beq }

def instBEqAgainPresupposition.beq : AgainPresupposition → AgainPresupposition → Bool

Equations

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

def RootDen.againOverRoot {Entity State Event : Type} : RootDen Entity State Event → AgainPresupposition

What again presupposes when scoping over just the root.

For PC roots (√FLAT): again√FLAT presupposes x was previously flat. This is a pure state presupposition — no change is implied.

For result roots (√CRACK): again√CRACK presupposes x was previously cracked. But √CRACK's denotation INCLUDES ∃e'[become'(s,e')], so this presupposition ENTAILS a prior change event.

For manner+result roots (√GUILLOTINE): again over the root presupposes prior change+manner. The root packages BECOME + manner restriction, so root-scope again entails a prior mannered change event (§4.5.2).

Equations

• (RootDen.pc statePred).againOverRoot = AgainPresupposition.priorState
• (RootDen.result statePred become entailsChange).againOverRoot = AgainPresupposition.priorChange
• (RootDen.mannerResult statePred become manner entailsChange entailsManner).againOverRoot = AgainPresupposition.priorChange

def againOverVP : AgainPresupposition

What again presupposes when scoping over vP (v_become + root). Always presupposes prior change, regardless of root type, because v_become introduces BECOME compositionally.

Equations

• againOverVP = AgainPresupposition.priorChange

theorem pc_again_distinct {Entity State Event : Type} (pred : Entity → State → Prop) : (RootDen.pc pred).againOverRoot ≠ againOverVP

PC roots: root-scope and vP-scope again yield DISTINCT presuppositions. Root-scope → prior state (no change); vP-scope → prior change. Two distinct presuppositions → two available readings.

theorem result_again_collapsed {Entity State Event : Type} (pred : Entity → State → Prop) (become : Event → State → Prop) (h : ∀ (x : Entity) (s : State), pred x s → ∃ (e : Event), become e s) : (RootDen.result pred become h).againOverRoot = againOverVP

Result roots: root-scope and vP-scope again yield THE SAME presupposition. Both presuppose prior change — root-scope because change is in the denotation, vP-scope because v_become introduces it. Same presupposition → readings collapse into one.

def RootDen.predictedAgainReadings {Entity State Event : Type} : RootDen Entity State Event → List AgainReading

Predicted again readings from the BKG denotation architecture. Distinct presuppositions → both readings available. Collapsed presuppositions → only repetitive. Manner+result roots collapse like result roots — the manner restriction adds no new scope point because it's within the root.

Equations

• (RootDen.pc statePred).predictedAgainReadings = [AgainReading.restitutive, AgainReading.repetitive]
• (RootDen.result statePred become entailsChange).predictedAgainReadings = [AgainReading.repetitive]
• (RootDen.mannerResult statePred become manner entailsChange entailsManner).predictedAgainReadings = [AgainReading.repetitive]

theorem bkg_again_matches_boolean {Entity State Event : Type} (rd : RootDen Entity State Event) : rd.predictedAgainReadings = rd.rootType.againReadings

The key bridge: the BKG denotation architecture predicts the SAME again-reading distribution as the Boolean RootType.againReadings.

This validates the compositional explanation: the reading collapse for result roots is not stipulated — it follows from change being constitutive of the root's meaning. The Boolean function encodes the SAME prediction, but the compositional analysis explains WHY.

def DitransitiveRootClass.obligatorilyTelic : DitransitiveRootClass → Bool

Whether a ditransitive verb is obligatorily telic in the IO frame (B&@cite{beavers-koontz-garboden-2020} §3.7).

Telicity correlates with whether the root spells out a state in the template. If the root entails actual possession, the template's prospective possession is discharged → definite endpoint → telic.

"Kim gave Sandy balls for an hour" — # (bounded by possession transfer) "Kim sent Sandy balls for an hour" — OK (endpoint only prospective)

Equations

• DitransitiveRootClass.causedPossession.obligatorilyTelic = true
• x✝.obligatorilyTelic = false

theorem telic_iff_actual_possession (c : DitransitiveRootClass) : c.obligatorilyTelic = true ↔ c.entailments.possession = PossessionEntailment.actual

Telicity aligns exactly with actual possession entailment.

def DitransitiveDen.againOverRoot {Entity Event : Type} : DitransitiveDen Entity Event → AgainPresupposition

What again presupposes over the root of a ditransitive denotation. Parallel to RootDen.againOverRoot (§12b): root-constitutive content makes root-scope and vP-scope again collapse.

-.withPossession: root carries possession → again over root presupposes prior possession (= prior change) → collapse -.simple: root has no possession → again over root presupposes prior event only (= prior state) → distinct readings

Equations

• (DitransitiveDen.simple eventPred).againOverRoot = AgainPresupposition.priorState
• (DitransitiveDen.withPossession eventPred possess entailsPoss).againOverRoot = AgainPresupposition.priorChange

def againOverDitransitiveVP : AgainPresupposition

again over the ditransitive vP always presupposes prior caused possession (from template CAUSE + ◇have').

Equations

• againOverDitransitiveVP = AgainPresupposition.priorChange

theorem give_den_again_collapsed {Entity Event : Type} (ep : Entity → Entity → Event → Prop) (poss : Entity → Entity → Prop) (h : ∀ (y z : Entity) (e : Event), ep y z e → poss z y) : (DitransitiveDen.withPossession ep poss h).againOverRoot = againOverDitransitiveVP

Give-type: root-scope and vP-scope again yield the SAME presupposition. Parallel to result_again_collapsed.

theorem send_den_again_distinct {Entity Event : Type} (ep : Entity → Entity → Event → Prop) : (DitransitiveDen.simple ep).againOverRoot ≠ againOverDitransitiveVP

Send-type: root-scope and vP-scope again yield DISTINCT presuppositions. Parallel to pc_again_distinct.

def DitransitiveRootClass.againReadings : DitransitiveRootClass → List AgainReading

Predicted again readings for each ditransitive root class.

Equations

• DitransitiveRootClass.causedPossession.againReadings = [AgainReading.repetitive]
• x✝.againReadings = [AgainReading.restitutive, AgainReading.repetitive]

theorem give_one_send_two_again : DitransitiveRootClass.causedPossession.againReadings.length = 1 ∧ DitransitiveRootClass.sending.againReadings.length = 2

Give has one reading (collapse); send has two (distinct).

theorem mannerResult_again_collapsed {Entity State Event : Type} (sp : Entity → State → Prop) (become : Event → State → Prop) (manner : Event → Prop) (hc : ∀ (x : Entity) (s : State), sp x s → ∃ (e : Event), become e s) (hm : ∀ (x : Entity) (s : State), sp x s → ∃ (v : Event), manner v) : (RootDen.mannerResult sp become manner hc hm).againOverRoot = againOverVP

Manner+result roots: root-scope and vP-scope again yield THE SAME presupposition, just like pure result roots. But the reason is RICHER: the root packages BECOME + manner, so root-scope again presupposes a prior mannered change event — which is strictly MORE than what vP-scope presupposes (just prior change).

Observable prediction: only repetitive reading available. Same as result roots, but for a different reason — manner is also caught in the collapse because it's inside the root.

theorem mannerResult_no_restitutive {Entity State Event : Type} (sp : Entity → State → Prop) (become : Event → State → Prop) (manner : Event → Prop) (hc : ∀ (x : Entity) (s : State), sp x s → ∃ (e : Event), become e s) (hm : ∀ (x : Entity) (s : State), sp x s → ∃ (v : Event), manner v) : (RootDen.mannerResult sp become manner hc hm).predictedAgainReadings = [AgainReading.repetitive]

Manner+result roots lack the restitutive reading.

theorem three_way_again_summary : RootType.propertyConcept.againReadings.length = 2 ∧ RootType.result.againReadings.length = 1 ∧ ∀ {Entity State Event : Type} (mr : RootDen Entity State Event), mr.denotationViolatesMRC = true → mr.predictedAgainReadings.length = 1

The three-way root denotation typology (B&@cite{beavers-koontz-garboden-2020} §4.5.5): PC, result, and manner+result roots ALL correctly predict again readings via the unified bkg_again_matches_boolean bridge.

PC roots: two readings (restitutive + repetitive) Result roots: one reading (repetitive) — change in root Manner+result roots: one reading (repetitive) — change + manner in root

theorem mrc_violation_implies_again_collapse {Entity State Event : Type} (rd : RootDen Entity State Event) (h : rd.denotationViolatesMRC = true) : rd.predictedAgainReadings = [AgainReading.repetitive]

Bridge: MRC-violating roots → collapsed again readings. If a root denotation violates MRC (manner+result), it has only repetitive again. The diagnostic MRC violation predicts the again collapse.

theorem again_collapse_not_sufficient_for_mrc {Entity State Event : Type} (sp : Entity → State → Prop) (become : Event → State → Prop) (hc : ∀ (x : Entity) (s : State), sp x s → ∃ (e : Event), become e s) : (RootDen.result sp become hc).predictedAgainReadings = [AgainReading.repetitive] ∧ (RootDen.result sp become hc).denotationViolatesMRC = false

Bridge: MRC-respecting result roots → collapsed again too. Collapsed again is necessary but NOT sufficient for MRC violation. Pure result roots also collapse, but they don't violate MRC.

theorem entails_change_implies_become_template (rt : RootType) (h : rt.entailsChange = true) : rt.requiresBECOME = true

Beavers et al.'s conclusion (§9): accepting that result roots entail change does NOT blunt the predictive power of event structures. It simply means the theory of possible root meanings is richer than bifurcation allows. A verb that entails change should have v_become-type grammatical behavior (argument structure, morphology) even if the change comes from the ROOT rather than the template.

Formally: if a root entails change, then the verb should be associated with a template containing BECOME.

theorem no_become_implies_no_change (rt : RootType) (h : rt.requiresBECOME = false) : rt.entailsChange = false

And conversely: if a root does NOT require BECOME, it doesn't entail change (it can stand alone as a simple stative).

theorem grand_unification (rt : RootType) : (rt.entailsChange = true → rt.hasSimpleStative = false ∧ rt.verbalFormIsMarked = false ∧ rt.allowsRestitutiveAgain = false ∧ rt.requiresBECOME = true ∧ rt.admitsBasicStative = false ∧ verbalMarkedness rt = Markedness.unmarked ∧ stativeMarkedness rt = Markedness.marked) ∧ (rt.entailsChange = false → rt.hasSimpleStative = true ∧ rt.verbalFormIsMarked = true ∧ rt.allowsRestitutiveAgain = true ∧ rt.requiresBECOME = false ∧ rt.admitsBasicStative = true ∧ verbalMarkedness rt = Markedness.marked ∧ stativeMarkedness rt = Markedness.unmarked)

The full correlation package.

Starting from the single Boolean entailsChange, we can derive ALL of the paper's morphosyntactic predictions. This is the formal content of the paper's main contribution: one semantic property (whether the root lexically entails change) is the sole determinant of six independently observable properties.

def Root.verbalMarkedness (r : Root) : Markedness

Predicted verbal markedness from change entailment.

Equations

• r.verbalMarkedness = verbalMarkedness r.changeType

def Root.stativeMarkedness (r : Root) : Markedness

Predicted stative markedness from change entailment.

Equations

• r.stativeMarkedness = stativeMarkedness r.changeType

def Root.break_ : Root

√BREAK: selects theme + entails change (result root, Levin 45.1). "Break X" — the root obligatorily takes a patient that undergoes breaking, and the root lexically entails a prior change event.

Equations

• Root.break_ = { arity := RootArity.selectsTheme, changeType := RootType.result, denotationType := some RootDenotationType.eventPred, levinClass := some LevinClass.break_ }

def Root.hit : Root

√HIT: selects theme + does not entail change (Levin 18.1). "Hit X" — the root takes a contactee, but hitting does not entail that the patient undergoes a change of state (@cite{levin-1993} pp. 5–8). .propertyConcept is used broadly here: the formal content (entailsChange = false) is what matters, not the label.

Equations

• Root.hit = { arity := RootArity.selectsTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.eventPred, levinClass := some LevinClass.hit }

def Root.die : Root

√DIE: no theme + entails change. "Die" — intransitive; the dying entity is introduced by functional structure (unaccusative vGO/vBE), not selected by the root. Dying lexically entails a prior change event (becoming dead).

Equations

• Root.die = { arity := RootArity.noTheme, changeType := RootType.result, denotationType := some RootDenotationType.eventPred }

def Root.sit : Root

√SIT: no theme + does not entail change (positional root). "Sit" — Coon's √POS class: denotes a spatial configuration state. No internal argument, no entailed change.

Equations

• Root.sit = { arity := RootArity.noTheme, changeType := RootType.propertyConcept, denotationType := some RootDenotationType.measureFn, levinClass := some LevinClass.assumePosition }

theorem arity_changeType_orthogonal : (∃ (r : Root), r.arity = RootArity.selectsTheme ∧ r.changeType = RootType.result) ∧ (∃ (r : Root), r.arity = RootArity.selectsTheme ∧ r.changeType = RootType.propertyConcept) ∧ (∃ (r : Root), r.arity = RootArity.noTheme ∧ r.changeType = RootType.result) ∧ ∃ (r : Root), r.arity = RootArity.noTheme ∧ r.changeType = RootType.propertyConcept

Orthogonality of arity and change entailment.

All four cells of the 2×2 cross-classification are inhabited. This proves the two dimensions are genuinely independent: knowing that a root selects a theme tells you nothing about whether it entails change, and vice versa.

theorem change_does_not_determine_arity : (∃ (r : Root), r.entailsChange = true ∧ r.arity = RootArity.selectsTheme) ∧ (∃ (r : Root), r.entailsChange = true ∧ r.arity = RootArity.noTheme) ∧ (∃ (r : Root), r.entailsChange = false ∧ r.arity = RootArity.selectsTheme) ∧ ∃ (r : Root), r.entailsChange = false ∧ r.arity = RootArity.noTheme

Change entailment does not determine arity (and vice versa).

Beavers et al.'s grand unification (§14) shows that entailsChange determines ALL morphosyntactic correlates (markedness, simple stative, again readings, template requirements). But it determines NOTHING about internal argument selection. Coon's arity adds an independent dimension of prediction: whether the root will surface with an internal argument across voice alternations.

theorem theme_persistence (r : Root) (h : r.arity = RootArity.selectsTheme) : r.arity.hasInternalArg = true

Theme persistence (@cite{coon-2019} main empirical claim).

If a root selects a theme, the internal argument persists regardless of what v/Voice⁰ head combines with it. In Chuj, √TV roots surface with an internal argument in transitive (Ø), passive (-ch, -j), and antipassive (-w) constructions alike.

This is expressed by design: arity is a field of Root, not of the derived verb. No functional head modifies it.

theorem root_markedness_from_change (r : Root) : r.verbalMarkedness = Markedness.unmarked ↔ r.entailsChange = true

Change entailment determines markedness in the unified Root.

theorem same_change_same_morphosyntax (r₁ r₂ : Root) (h : r₁.changeType = r₂.changeType) : r₁.verbalMarkedness = r₂.verbalMarkedness ∧ r₁.stativeMarkedness = r₂.stativeMarkedness ∧ r₁.entailsChange = r₂.entailsChange

Roots with the same change type have identical morphosyntactic behavior regardless of arity — markedness, stative forms, and again readings are orthogonal to internal argument selection.

structure FullRootSpec : Type

Full root specification: entailment features + structural position. This is B&@cite{beavers-koontz-garboden-2020}'s Table 12 in full — the 4 binary entailment features × 2 positions give 32 theoretical cells, of which 7 are attested and the rest are principled gaps.

• entailments : RootEntailments
• position : RootPosition

def instDecidableEqFullRootSpec.decEq (x✝ x✝¹ : FullRootSpec) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqFullRootSpec : DecidableEq FullRootSpec

Equations

• instDecidableEqFullRootSpec = instDecidableEqFullRootSpec.decEq

def instBEqFullRootSpec.beq : FullRootSpec → FullRootSpec → Bool

Equations

• instBEqFullRootSpec.beq { entailments := a, position := a_1 } { entailments := b, position := b_1 } = (a == b && a_1 == b_1)
• instBEqFullRootSpec.beq x✝¹ x✝ = false

instance instBEqFullRootSpec : BEq FullRootSpec

Equations

• instBEqFullRootSpec = { beq := instBEqFullRootSpec.beq }

def instReprFullRootSpec.repr : FullRootSpec → ℕ → Std.Format

Equations

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

instance instReprFullRootSpec : Repr FullRootSpec

Equations

• instReprFullRootSpec = { reprPrec := instReprFullRootSpec.repr }

def FullRootSpec.positionLicensed (s : FullRootSpec) : Bool

Adjoined position requires +manner: a root in adjunct position must specify a manner of action. Without manner, there is nothing to adjoin — the adjunct slot expects an action modifier.

Equations

• s.positionLicensed = match s.position with | RootPosition.adjoined => s.entailments.manner | RootPosition.complement => true

def FullRootSpec.semanticallyCoherent (s : FullRootSpec) : Bool

+manner +state −result −cause is semantically incoherent (B&KG §5.4.1): the root would specify both a manner of action and a state, but with no result or cause linking them. What would such a verb mean? "Perform manner M while in state S" — with no causal connection.

Equations

• s.semanticallyCoherent = !(s.entailments.manner && s.entailments.state && !s.entailments.result && !s.entailments.cause)

def FullRootSpec.wellFormed (s : FullRootSpec) : Bool

Full well-formedness: entailment constraints + position licensing + semantic coherence.

Equations

• s.wellFormed = (s.entailments.wellFormed && s.positionLicensed && s.semanticallyCoherent)

Attested cells of Table 12

def FullRootSpec.flat : FullRootSpec

√FLAT: +S −M −R −C, complement. Property concept root.

Equations

• FullRootSpec.flat = { entailments := RootEntailments.propertyConcept, position := RootPosition.complement }

def FullRootSpec.blossom : FullRootSpec

√BLOSSOM: +S −M +R −C, complement. Pure result root.

Equations

• FullRootSpec.blossom = { entailments := RootEntailments.pureResult, position := RootPosition.complement }

def FullRootSpec.crack : FullRootSpec

√CRACK: +S −M +R +C, complement. Causative result root.

Equations

• FullRootSpec.crack = { entailments := RootEntailments.causativeResult, position := RootPosition.complement }

def FullRootSpec.jog : FullRootSpec

√JOG: −S +M −R −C, adjoined. Pure manner root.

Equations

• FullRootSpec.jog = { entailments := RootEntailments.pureManner, position := RootPosition.adjoined }

def FullRootSpec.drown : FullRootSpec

√DROWN: +S +M +R +C, complement. Manner+result in complement position — the manner restricts HOW the state is caused.

Equations

• FullRootSpec.drown = { entailments := RootEntailments.fullSpec, position := RootPosition.complement }

def FullRootSpec.toss : FullRootSpec

√TOSS: +S +M +R +C, adjoined. Manner+result in adjunct position — the manner is the primary event that happens to cause a state change.

Equations

• FullRootSpec.toss = { entailments := RootEntailments.fullSpec, position := RootPosition.adjoined }

@[reducible, inline]

abbrev FullRootSpec.hand : FullRootSpec

√HAND: same entailments + position as √TOSS. The difference is in the ditransitive layer (DitransitiveRootClass.causedPossession vs .ballisticMotion), not in FullRootSpec's 4+1 features.

Equations

• FullRootSpec.hand = FullRootSpec.toss

def FullRootSpec.exist : FullRootSpec

√EXIST: −S −M −R −C, complement. Minimal stative root.

Equations

• FullRootSpec.exist = { entailments := RootEntailments.minimal, position := RootPosition.complement }

theorem flat_wf : FullRootSpec.flat.wellFormed = true

theorem blossom_wf : FullRootSpec.blossom.wellFormed = true

theorem crack_wf : FullRootSpec.crack.wellFormed = true

theorem jog_wf : FullRootSpec.jog.wellFormed = true

theorem drown_wf : FullRootSpec.drown.wellFormed = true

theorem toss_wf : FullRootSpec.toss.wellFormed = true

theorem hand_wf : FullRootSpec.hand.wellFormed = true

theorem exist_wf : FullRootSpec.exist.wellFormed = true

theorem drown_toss_same_entailments : FullRootSpec.drown.entailments = FullRootSpec.toss.entailments

√DROWN and √TOSS have identical entailments but different positions.

theorem drown_toss_diff_position : FullRootSpec.drown.position ≠ FullRootSpec.toss.position

inductive TemplateHead : Type

Templatic functional heads in event structure (B&@cite{beavers-koontz-garboden-2020} Table 13).

Each root type PREDICTS which templatic heads its verb will entail. If the root's own meaning already includes what a template head provides, that head is "entailed by the root" — its semantic contribution is redundant (though structurally still present).

v_act, v_cause, v_become are verbal heads. P_loc and P_have are prepositional heads specific to ditransitive structures.

• vAct : TemplateHead
• vCause : TemplateHead
• vBecome : TemplateHead
• pLoc : TemplateHead
• pHave : TemplateHead

instance instDecidableEqTemplateHead : DecidableEq TemplateHead

Equations

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

instance instReprTemplateHead : Repr TemplateHead

Equations

• instReprTemplateHead = { reprPrec := instReprTemplateHead.repr }

def instReprTemplateHead.repr : TemplateHead → ℕ → Std.Format

Equations

• instReprTemplateHead.repr TemplateHead.vAct prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.vAct")).group prec✝
• instReprTemplateHead.repr TemplateHead.vCause prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.vCause")).group prec✝
• instReprTemplateHead.repr TemplateHead.vBecome prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.vBecome")).group prec✝
• instReprTemplateHead.repr TemplateHead.pLoc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.pLoc")).group prec✝
• instReprTemplateHead.repr TemplateHead.pHave prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "TemplateHead.pHave")).group prec✝

instance instBEqTemplateHead : BEq TemplateHead

Equations

• instBEqTemplateHead = { beq := instBEqTemplateHead.beq }

def instBEqTemplateHead.beq : TemplateHead → TemplateHead → Bool

Equations

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

def RootEntailments.entailedHeads (r : RootEntailments) : List TemplateHead

Which template heads a root's entailments make redundant (Table 13).

The mapping is monotone: more root entailments → more heads entailed.

• +result → v_become (root entails the change v_become would provide)
• +cause → v_cause (root entails the causation v_cause would provide)
• +manner ∧ +cause → v_act (manner that causes = activity)
• +manner alone → no v_act (manner without causation doesn't entail activity — √JOG specifies jogging manner but v_act still provides the activity frame)

Equations

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

def DitransitiveRootClass.additionalHeads : DitransitiveRootClass → List TemplateHead

For ditransitive roots, additional prepositional heads beyond the verbal heads predicted by entailedHeads.

Equations

• DitransitiveRootClass.causedPossession.additionalHeads = [TemplateHead.pLoc, TemplateHead.pHave]
• DitransitiveRootClass.ballisticMotion.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.sending.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.accompaniedMotion.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.carrying.additionalHeads = [TemplateHead.pLoc]
• DitransitiveRootClass.futureHaving.additionalHeads = []

Table 13 verification

theorem jog_no_heads : RootEntailments.pureManner.entailedHeads = []

√JOG (pureManner): no template heads entailed. The root specifies jogging manner, but v_act still provides the activity frame — the root doesn't make it redundant.

theorem flat_no_heads : RootEntailments.propertyConcept.entailedHeads = []

√FLAT (propertyConcept): no template heads entailed. The root names a state, but doesn't entail change or cause.

theorem blossom_heads : RootEntailments.pureResult.entailedHeads = [TemplateHead.vBecome]

√BLOSSOM (pureResult): v_become entailed. The root entails change — v_become's contribution is redundant.

theorem crack_heads : RootEntailments.causativeResult.entailedHeads = [TemplateHead.vBecome, TemplateHead.vCause]

√CRACK (causativeResult): v_become + v_cause entailed. The root entails change AND causation.

theorem drown_heads : RootEntailments.fullSpec.entailedHeads = [TemplateHead.vBecome, TemplateHead.vCause, TemplateHead.vAct]

√DROWN (fullSpec): v_become + v_cause + v_act entailed. The root entails change, causation, AND activity (manner that causes).

theorem toss_heads : RootEntailments.fullSpec.entailedHeads ++ DitransitiveRootClass.ballisticMotion.additionalHeads = [TemplateHead.vBecome, TemplateHead.vCause, TemplateHead.vAct, TemplateHead.pLoc]

√TOSS (fullSpec + ballistic): v_become + v_cause + v_act + P_loc. Verbal heads from entailments + P_loc from ditransitive class.

theorem hand_heads : RootEntailments.fullSpec.entailedHeads ++ DitransitiveRootClass.causedPossession.additionalHeads = [TemplateHead.vBecome, TemplateHead.vCause, TemplateHead.vAct, TemplateHead.pLoc, TemplateHead.pHave]

√HAND (fullSpec + causedPossession): all 5 heads. Verbal heads from entailments + P_loc + P_have from ditransitive class.

theorem heads_monotone : RootEntailments.pureResult.entailedHeads.length ≤ RootEntailments.causativeResult.entailedHeads.length ∧ RootEntailments.causativeResult.entailedHeads.length ≤ RootEntailments.fullSpec.entailedHeads.length

Monotonicity: more root entailments → weakly more heads entailed. Pure result ⊂ causative result ⊂ full spec (by inclusion).

def FullRootSpec.isAttestedCell (s : FullRootSpec) : Bool

Whether a FullRootSpec cell is attested in B&KG's Table 12.

Equations

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

Gap explanations

B&KG (§5.4.1) identify three principled gap types:

1. Adjoined without manner: the adjunct position in event structure hosts manner modifiers. Without +manner, there's nothing to adjoin. This rules out all −manner roots in adjoined position.

2. +manner +state −result −cause: the root would need to encode both a manner of action and a state, with no causal/change connection between them. No known verb has this pattern.

3. Well-formedness violations: +result −state and +cause −result are ruled out by the entailment constraints (result→state, cause→result).

theorem gap_adjoined_no_manner : { entailments := RootEntailments.propertyConcept, position := RootPosition.adjoined }.positionLicensed = false

Gap type 1: adjoined position requires manner.

theorem gap_adjoined_result : { entailments := RootEntailments.pureResult, position := RootPosition.adjoined }.positionLicensed = false

theorem gap_adjoined_causativeResult : { entailments := RootEntailments.causativeResult, position := RootPosition.adjoined }.positionLicensed = false

theorem gap_adjoined_minimal : { entailments := RootEntailments.minimal, position := RootPosition.adjoined }.positionLicensed = false

theorem gap_manner_state_no_result : { entailments := { state := true, manner := true, result := false, cause := false }, position := RootPosition.complement }.semanticallyCoherent = false

Gap type 2: +manner +state −result −cause is incoherent.

theorem gap_manner_state_no_result_adj : { entailments := { state := true, manner := true, result := false, cause := false }, position := RootPosition.adjoined }.semanticallyCoherent = false

theorem gap_result_no_state : { state := false, manner := false, result := true, cause := false }.wellFormed = false

Gap type 3: well-formedness violations.

theorem gap_cause_no_result : { state := true, manner := false, result := false, cause := true }.wellFormed = false

Attested cells are well-formed and recognized

theorem flat_attested : FullRootSpec.flat.isAttestedCell = true

theorem blossom_attested : FullRootSpec.blossom.isAttestedCell = true

theorem crack_attested : FullRootSpec.crack.isAttestedCell = true

theorem jog_attested : FullRootSpec.jog.isAttestedCell = true

theorem drown_attested : FullRootSpec.drown.isAttestedCell = true

theorem toss_attested : FullRootSpec.toss.isAttestedCell = true

theorem exist_attested : FullRootSpec.exist.isAttestedCell = true

theorem mannerResult_complement_unattested : { entailments := RootEntailments.mannerResult, position := RootPosition.complement }.isAttestedCell = false

The open question: +S +M +R −C (mannerResult without cause) in complement position. B&KG note this cell may be inhabited by verbs like slide — manner of motion + change of location, without external causation. Left as NOT attested per Table 12, pending further research.

theorem fullSpec_both_positions : FullRootSpec.drown.isAttestedCell = true ∧ FullRootSpec.toss.isAttestedCell = true ∧ FullRootSpec.drown.entailments = FullRootSpec.toss.entailments

The complement/adjoined split for fullSpec roots is the only case where position differentiates otherwise identical entailments.