Cross-Linguistic Typology of Change-of-State Verbs

[Dix82] [Lev93] [BEJ+21] [Coo19]

Empirical data from Beavers, Everdell, Jerro, Kauhanen, [BEJ+21] "States and changes of state: A crosslinguistic study of the roots of verbal meaning." Language 97(3), 439–484.

88-language balanced sample (WALS 100 + additions). For each of 36 property concept (PC) and 36 result root meanings, the authors collected five-item paradigms (underlying root, simple stative, inchoative, causative, result stative) and coded morphological relationships.

Key findings (theory-neutral)

1. Simple statives: PC roots overwhelmingly have simple stative forms (median = 95.67% of languages); result roots overwhelmingly lack them (median = 1.59%). Mann-Whitney U = 1266.5, p < 0.001.

2. Verbal markedness: PC root verbs tend to be marked (median = 56.01%); result root verbs tend to be unmarked (median = 15.20%). Mann-Whitney U = 1291, p < 0.001.

3. Subclass clustering: PC subclasses (dimension, color, value, physical property, speed) cluster near 100% simple statives. Result subclasses (breaking, cooking, killing, destroying, directed motion) cluster near 0%.

Theory apparatus

The change-entailment theory (§§3–14 below) is stated over the substrate Verb.Root.ChangeType; this paper is its sole consumer. The "Markedness Generalization" label is the formaliser's — the content (ex. (44)) is faithful to the paper.

inductive BeaversEtAl2021.CoSRootClass : Type

Two classes of change-of-state verb roots, defined by morphological and semantic diagnostics ([BEJ+21] §3.1).

Classification criteria:

• PC roots: the root of deadjectival CoS verbs ([Lev93]:245); describe [Dix82]'s basic property types
• Result roots: the root of non-deadjectival CoS verbs; describe specific result states (physical damage, cooking, etc.)

• propertyConcept : CoSRootClass
• result : CoSRootClass

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqCoSRootClass : DecidableEq CoSRootClass

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprCoSRootClass : Repr CoSRootClass

Equations

• BeaversEtAl2021.instReprCoSRootClass = { reprPrec := BeaversEtAl2021.instReprCoSRootClass.repr }

def BeaversEtAl2021.instReprCoSRootClass.repr : CoSRootClass → ℕ → Std.Format

Equations

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

inductive BeaversEtAl2021.PCSubclass : Type

PC subclasses ([Dix82]; [BEJ+21] ex. 5).

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

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqPCSubclass : DecidableEq PCSubclass

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprPCSubclass : Repr PCSubclass

Equations

• BeaversEtAl2021.instReprPCSubclass = { reprPrec := BeaversEtAl2021.instReprPCSubclass.repr }

def BeaversEtAl2021.instReprPCSubclass.repr : PCSubclass → ℕ → Std.Format

Equations

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

inductive BeaversEtAl2021.ResultSubclass : Type

Result root subclasses ([Lev93]; [BEJ+21] ex. 6).

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

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqResultSubclass : DecidableEq ResultSubclass

Equations

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

def BeaversEtAl2021.instReprResultSubclass.repr : ResultSubclass → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprResultSubclass : Repr ResultSubclass

Equations

• BeaversEtAl2021.instReprResultSubclass = { reprPrec := BeaversEtAl2021.instReprResultSubclass.repr }

inductive BeaversEtAl2021.ParadigmPosition : Type

The five positions in a CoS verb paradigm ([BEJ+21] eq. 40). Every root meaning is associated with (up to) five forms.

• underlyingRoot : ParadigmPosition
• simpleStative : ParadigmPosition
• inchoative : ParadigmPosition
• causative : ParadigmPosition
• resultStative : ParadigmPosition

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqParadigmPosition : DecidableEq ParadigmPosition

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprParadigmPosition : Repr ParadigmPosition

Equations

• BeaversEtAl2021.instReprParadigmPosition = { reprPrec := BeaversEtAl2021.instReprParadigmPosition.repr }

def BeaversEtAl2021.instReprParadigmPosition.repr : ParadigmPosition → ℕ → Std.Format

Equations

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

inductive BeaversEtAl2021.MorphRelation : Type

Morphological relationship codes between forms ([BEJ+21] eq. 41, generalizing [Has93]:90–92).

• input : MorphRelation
• derived : MorphRelation
• transitive : MorphRelation
• labile : MorphRelation
• equipollent : MorphRelation
• unrelated : MorphRelation
• unattested : MorphRelation
• suppletive : MorphRelation

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqMorphRelation : DecidableEq MorphRelation

Equations

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

def BeaversEtAl2021.instReprMorphRelation.repr : MorphRelation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprMorphRelation : Repr MorphRelation

Equations

• BeaversEtAl2021.instReprMorphRelation = { reprPrec := BeaversEtAl2021.instReprMorphRelation.repr }

structure BeaversEtAl2021.RootMeaning : Type

A root meaning with its crosslinguistic attestation.

• gloss : String

  English gloss(es)

• rootClass : CoSRootClass

  PC or result root

• subclass : Option (PCSubclass ⊕ ResultSubclass)

  Subclass, if applicable

• nSimpleStative : ℕ

  Number of languages with a simple stative for this root (Table A1)

• nLanguages : ℕ

  Number of languages with any data for this root (Table A1)

• nMarkedVerbal : ℕ

  Number of languages with a marked verbal paradigm (Table A2)

• nVerbalLanguages : ℕ

  Number of languages with verbal paradigm data (Table A2)

@[instance_reducible]

instance BeaversEtAl2021.instReprRootMeaning : Repr RootMeaning

Equations

• BeaversEtAl2021.instReprRootMeaning = { reprPrec := BeaversEtAl2021.instReprRootMeaning.repr }

def BeaversEtAl2021.instReprRootMeaning.repr : RootMeaning → ℕ → Std.Format

Equations

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

def BeaversEtAl2021.RootMeaning.pctSimpleStative (r : RootMeaning) : ℚ

Percentage of languages with simple stative (exact ℚ — kernel-decidable).

Equations

• r.pctSimpleStative = if r.nLanguages = 0 then 0 else ↑r.nSimpleStative * 100 / ↑r.nLanguages

def BeaversEtAl2021.RootMeaning.pctMarkedVerbal (r : RootMeaning) : ℚ

Percentage of languages with marked verbal paradigm (exact ℚ).

Equations

• r.pctMarkedVerbal = if r.nVerbalLanguages = 0 then 0 else ↑r.nMarkedVerbal * 100 / ↑r.nVerbalLanguages

def BeaversEtAl2021.coldRoot : RootMeaning

Equations

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

def BeaversEtAl2021.largeRoot : RootMeaning

Equations

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

def BeaversEtAl2021.redRoot : RootMeaning

Equations

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

def BeaversEtAl2021.longRoot : RootMeaning

Equations

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

def BeaversEtAl2021.goodRoot : RootMeaning

Equations

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

def BeaversEtAl2021.dryRoot : RootMeaning

Equations

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

def BeaversEtAl2021.oldRoot : RootMeaning

Equations

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

def BeaversEtAl2021.whiteRoot : RootMeaning

Equations

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

def BeaversEtAl2021.brokenRoot : RootMeaning

Equations

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

def BeaversEtAl2021.cookedRoot : RootMeaning

Equations

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

def BeaversEtAl2021.deadRoot : RootMeaning

Equations

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

def BeaversEtAl2021.meltedRoot : RootMeaning

Equations

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

def BeaversEtAl2021.shatteredRoot : RootMeaning

Equations

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

def BeaversEtAl2021.bentRoot : RootMeaning

Equations

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

def BeaversEtAl2021.burnedRoot : RootMeaning

Equations

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

def BeaversEtAl2021.tornRoot : RootMeaning

Equations

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

def BeaversEtAl2021.goneRoot : RootMeaning

Equations

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

def BeaversEtAl2021.destroyedRoot : RootMeaning

Equations

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

def BeaversEtAl2021.pcRoots : List RootMeaning

Equations

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

def BeaversEtAl2021.resultRoots : List RootMeaning

Equations

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

structure BeaversEtAl2021.TypologicalComparison : Type

Summary of a crosslinguistic comparison between PC and result roots. Numeric fields are exact ℚ (mathlib idiom for kernel-decidable arithmetic; [BEJ+21] reports values to 2 decimal places).

• measure : String

  What is being measured

• pcMedian : ℚ

  PC root median percentage

• resultMedian : ℚ

  Result root median percentage

• uStatistic : ℚ

  Mann-Whitney U statistic

• pThreshold : ℚ

  One-tailed p-value threshold

• nPC : ℕ

  Sample sizes (PC roots, result roots)

• nResult : ℕ

@[instance_reducible]

instance BeaversEtAl2021.instReprTypologicalComparison : Repr TypologicalComparison

Equations

• BeaversEtAl2021.instReprTypologicalComparison = { reprPrec := BeaversEtAl2021.instReprTypologicalComparison.repr }

def BeaversEtAl2021.instReprTypologicalComparison.repr : TypologicalComparison → ℕ → Std.Format

Equations

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

def BeaversEtAl2021.simpleStativeComparison : TypologicalComparison

Simple stative form comparison (§6, Fig. 1). Medians: 95.67% and 1.59% encoded as exact rationals via OfScientific.

Equations

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

def BeaversEtAl2021.verbalMarkednessComparison : TypologicalComparison

Verbal markedness comparison (§7, Fig. 5). Medians: 56.01% and 15.20% encoded as exact rationals via OfScientific.

Equations

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

theorem BeaversEtAl2021.both_comparisons_significant : simpleStativeComparison.pcMedian > simpleStativeComparison.resultMedian ∧ verbalMarkednessComparison.pcMedian > verbalMarkednessComparison.resultMedian

Both comparisons are statistically significant.

inductive BeaversEtAl2021.DiagnosticResult : Type

Empirical diagnostics for classifying roots. Each diagnostic independently sorts roots into two classes that align with the PC vs result distinction.

• positive : DiagnosticResult
• negative : DiagnosticResult

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqDiagnosticResult : DecidableEq DiagnosticResult

Equations

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

def BeaversEtAl2021.instReprDiagnosticResult.repr : DiagnosticResult → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprDiagnosticResult : Repr DiagnosticResult

Equations

• BeaversEtAl2021.instReprDiagnosticResult = { reprPrec := BeaversEtAl2021.instReprDiagnosticResult.repr }

def BeaversEtAl2021.changeDenialTest : CoSRootClass → DiagnosticResult

Stative form + change denial test (§3.3, ex. 10–11). "The bright photo has never brightened" → OK (PC) "#The shattered vase has never shattered" → contradictory (result)

Equations

• BeaversEtAl2021.changeDenialTest BeaversEtAl2021.CoSRootClass.propertyConcept = BeaversEtAl2021.DiagnosticResult.positive
• BeaversEtAl2021.changeDenialTest BeaversEtAl2021.CoSRootClass.result = BeaversEtAl2021.DiagnosticResult.negative

def BeaversEtAl2021.restitutiveAgainTest : CoSRootClass → DiagnosticResult

Restitutive 'again' test (§3.4, ex. 15–16). "John sharpened the knife again" → can be just one sharpening (PC) "#Chris thawed the meat again" → necessarily two thawings (result)

Equations

• BeaversEtAl2021.restitutiveAgainTest BeaversEtAl2021.CoSRootClass.propertyConcept = BeaversEtAl2021.DiagnosticResult.positive
• BeaversEtAl2021.restitutiveAgainTest BeaversEtAl2021.CoSRootClass.result = BeaversEtAl2021.DiagnosticResult.negative

theorem BeaversEtAl2021.diagnostics_agree (rc : CoSRootClass) : changeDenialTest rc = restitutiveAgainTest rc

The two diagnostics always agree.

structure BeaversEtAl2021.LanguageProfile : Type

A language's CoS verb typological profile.

• language : String
• family : String
• nPCParadigms : ℕ

  Number of PC root verbal paradigms with data

• nResultParadigms : ℕ

  Number of result root verbal paradigms with data

• pctPCMarked : ℚ

  % of PC paradigms that are marked (exact ℚ)

• pctResultMarked : ℚ

  % of result paradigms that are marked (exact ℚ)

def BeaversEtAl2021.instReprLanguageProfile.repr : LanguageProfile → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprLanguageProfile : Repr LanguageProfile

Equations

• BeaversEtAl2021.instReprLanguageProfile = { reprPrec := BeaversEtAl2021.instReprLanguageProfile.repr }

def BeaversEtAl2021.kakataibo : LanguageProfile

The six in-depth case study languages (§4).

Equations

• BeaversEtAl2021.kakataibo = { language := "Kakataibo", family := "Panoan", nPCParadigms := 59, nResultParadigms := 64, pctPCMarked := 23.73, pctResultMarked := 31.25 }

def BeaversEtAl2021.kinyarwanda : LanguageProfile

Equations

• BeaversEtAl2021.kinyarwanda = { language := "Kinyarwanda", family := "Northeastern Bantu", nPCParadigms := 69, nResultParadigms := 33, pctPCMarked := 4.17, pctResultMarked := 9.09 }

def BeaversEtAl2021.hebrew : LanguageProfile

Equations

• BeaversEtAl2021.hebrew = { language := "Hebrew (Modern)", family := "Semitic", nPCParadigms := 35, nResultParadigms := 42, pctPCMarked := 97.62, pctResultMarked := 0.98 }

def BeaversEtAl2021.marathi : LanguageProfile

Equations

• BeaversEtAl2021.marathi = { language := "Marathi", family := "Indic", nPCParadigms := 40, nResultParadigms := 35, pctPCMarked := 20.41, pctResultMarked := 21.33 }

def BeaversEtAl2021.greek : LanguageProfile

Equations

• BeaversEtAl2021.greek = { language := "Greek (Modern)", family := "Indo-European", nPCParadigms := 76, nResultParadigms := 57, pctPCMarked := 2.63, pctResultMarked := 2.15 }

def BeaversEtAl2021.english : LanguageProfile

Equations

• BeaversEtAl2021.english = { language := "English", family := "Germanic", nPCParadigms := 43, nResultParadigms := 60, pctPCMarked := 0.0, pctResultMarked := 0.0 }

def BeaversEtAl2021.caseStudyLanguages : List LanguageProfile

Equations

• BeaversEtAl2021.caseStudyLanguages = [BeaversEtAl2021.kakataibo, BeaversEtAl2021.kinyarwanda, BeaversEtAl2021.hebrew, BeaversEtAl2021.marathi, BeaversEtAl2021.greek, BeaversEtAl2021.english]

inductive BeaversEtAl2021.LanguageType : Type

Attested language types (§7.2, §8).

• asymmetric : LanguageType
• highMarking : LanguageType
• lowMarking : LanguageType

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqLanguageType : DecidableEq LanguageType

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprLanguageType : Repr LanguageType

Equations

• BeaversEtAl2021.instReprLanguageType = { reprPrec := BeaversEtAl2021.instReprLanguageType.repr }

def BeaversEtAl2021.instReprLanguageType.repr : LanguageType → ℕ → Std.Format

Equations

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

def BeaversEtAl2021.LanguageType.allAttested : List LanguageType

The fourth logically possible type (result marked, PC unmarked) is UNATTESTED — predicted by the markedness generalization.

Equations

• BeaversEtAl2021.LanguageType.allAttested = [BeaversEtAl2021.LanguageType.asymmetric, BeaversEtAl2021.LanguageType.highMarking, BeaversEtAl2021.LanguageType.lowMarking]

theorem BeaversEtAl2021.three_attested_types : LanguageType.allAttested.length = 3

Three and only three types are attested.

theorem BeaversEtAl2021.pcRoots_all_pc : (pcRoots.all fun (x : RootMeaning) => x.rootClass == CoSRootClass.propertyConcept) = true

All entries in our PC root sample are classified as PC.

theorem BeaversEtAl2021.resultRoots_all_result : (resultRoots.all fun (x : RootMeaning) => x.rootClass == CoSRootClass.result) = true

All entries in our result root sample are classified as result.

theorem BeaversEtAl2021.most_pc_roots_have_statives : (List.filter (fun (r : RootMeaning) => decide (r.nSimpleStative * 2 ≥ r.nLanguages)) pcRoots).length ≥ pcRoots.length - 1

Most PC roots in the sample have ≥ 50% simple stative attestation.

theorem BeaversEtAl2021.result_roots_rare_statives : (resultRoots.all fun (r : RootMeaning) => decide (r.nSimpleStative * 10 ≤ r.nLanguages)) = true

No result root in the sample exceeds 10% simple stative attestation.

def BeaversEtAl2021.hasSimpleStative : Verb.Root.ChangeType → Bool

PC roots have simple (unmarked) stative forms; result roots lack them. English: "bright" (PC, simple adj) vs *"shattered" requires prior change. Crosslinguistic evidence (§6, Fig. 1): PC median = 95.67%, result median = 1.59% (Mann-Whitney U = 1266.5, p < 0.001, n₁ = n₂ = 36).

Equations

• BeaversEtAl2021.hasSimpleStative Verb.Root.ChangeType.propertyConcept = true
• BeaversEtAl2021.hasSimpleStative Verb.Root.ChangeType.result = false

def BeaversEtAl2021.verbalFormIsMarked : Verb.Root.ChangeType → Bool

PC root verbs TEND to be morphologically marked (wid-en, flat-ten); result root verbs tend to be unmarked (break, crack). The cross-linguistic DEFAULT, not a universal — [HKG25] §4 notes deviating Wá·šiw Class 1 roots. Crosslinguistic evidence (§7, Fig. 5): PC median = 56.01%, result median = 15.20% (U = 1291, p < 0.001).

Equations

• BeaversEtAl2021.verbalFormIsMarked Verb.Root.ChangeType.propertyConcept = true
• BeaversEtAl2021.verbalFormIsMarked Verb.Root.ChangeType.result = false

theorem BeaversEtAl2021.semantic_determines_morphosyntax (ct : Verb.Root.ChangeType) : ct.entailsChange = true ↔ hasSimpleStative ct = false ∧ verbalFormIsMarked ct = false ∧ ct.allowsRestitutiveAgain = false

The main theorem. A root's entailment of change determines all of its morphosyntactic behavior in a single biconditional: result roots lack simple statives (§6), have unmarked verbal forms (§7), and lack restitutive again (§3.4); PC roots are the reverse. Refutes the Bifurcation Thesis.

theorem BeaversEtAl2021.pc_determines_morphosyntax (ct : Verb.Root.ChangeType) : ct.entailsChange = false ↔ hasSimpleStative ct = true ∧ verbalFormIsMarked ct = true ∧ ct.allowsRestitutiveAgain = true

The converse: NOT entailing change determines the opposite package.

def BeaversEtAl2021.bifurcationThesis (rootEntailsChange : Verb.Root.ChangeType → Bool) : Prop

The Bifurcation Thesis for Roots ([Emb09]:1, [Ara05]:79; [BEJ+21] ex. 2): a component of meaning introduced by a templatic operator cannot be part of a root's meaning — so NO root should entail change.

Equations

• BeaversEtAl2021.bifurcationThesis rootEntailsChange = ∀ (ct : Verb.Root.ChangeType), rootEntailsChange ct = false

theorem BeaversEtAl2021.bifurcation_fails : ¬bifurcationThesis Verb.Root.ChangeType.entailsChange

[BEJ+21] main result: bifurcation does not hold. Result roots entail change, violating the thesis (§§3.3, 3.6, 9).

theorem BeaversEtAl2021.result_roots_witness_against_bifurcation : Verb.Root.ChangeType.result.entailsChange = true

Result roots witness bifurcation failure.

theorem BeaversEtAl2021.pc_roots_consistent_with_bifurcation : Verb.Root.ChangeType.propertyConcept.entailsChange = false

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

theorem BeaversEtAl2021.bkg_bifurcation_fails_all_dimensions : Verb.LexKind.result ∈ Verb.Root.Kinds.fullSpec ∧ Verb.LexKind.cause ∈ Verb.Root.Kinds.fullSpec ∧ Verb.LexKind.manner ∈ Verb.Root.Kinds.fullSpec ∧ Verb.LexKind.state ∈ Verb.Root.Kinds.fullSpec

B&[BKG20] strengthened bifurcation failure via Root.Kinds. [BEJ+21] show roots can entail CHANGE; B&[BKG20] show roots can entail CHANGE, CAUSATION, and MANNER simultaneously (√GUILLOTINE, √HAND) — a strictly stronger refutation. Witness: Root.Kinds.fullSpec carries all four kinds.

theorem BeaversEtAl2021.bkg_bifurcation_multiple_witnesses : Verb.LexKind.result ∈ ArgumentStructure.LevinClass.cut.rootEntailments ∧ Verb.LexKind.manner ∈ ArgumentStructure.LevinClass.cut.rootEntailments ∧ Verb.LexKind.cause ∈ ArgumentStructure.LevinClass.give.rootEntailments ∧ Verb.LexKind.manner ∈ ArgumentStructure.LevinClass.give.rootEntailments

Multiple Levin classes witness the stronger bifurcation failure.

inductive BeaversEtAl2021.Markedness : Type

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

• unmarked : Markedness
• marked : Markedness

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqMarkedness : DecidableEq Markedness

Equations

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

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

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprMarkedness : Repr Markedness

Equations

• BeaversEtAl2021.instReprMarkedness = { reprPrec := BeaversEtAl2021.instReprMarkedness.repr }

def BeaversEtAl2021.verbalMarkedness (ct : Verb.Root.ChangeType) : Markedness

The Markedness Generalization ([BEJ+21] ex. 44): morphological markedness reflects semantic mismatch between a functional head and its root complement. A verb is unmarked when v_become is redundant with the root's change entailment; a stative is unmarked when no change need be stripped. This yields the three attested language types (English-type asymmetric, equipollent, labile) and rules out the unattested fourth.

Equations

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

def BeaversEtAl2021.stativeMarkedness (ct : Verb.Root.ChangeType) : Markedness

Stative markedness is the mirror image of verbal markedness.

Equations

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

theorem BeaversEtAl2021.markedness_complementarity (ct : Verb.Root.ChangeType) : verbalMarkedness ct ≠ stativeMarkedness ct

Verbal and stative markedness are always complementary.

theorem BeaversEtAl2021.result_root_unmarked_verb : verbalMarkedness Verb.Root.ChangeType.result = Markedness.unmarked

Result roots produce unmarked verbs.

theorem BeaversEtAl2021.pc_root_marked_verb : verbalMarkedness Verb.Root.ChangeType.propertyConcept = Markedness.marked

PC roots produce marked verbs.

theorem BeaversEtAl2021.result_root_marked_stative : stativeMarkedness Verb.Root.ChangeType.result = Markedness.marked

Result roots produce marked statives.

theorem BeaversEtAl2021.pc_root_unmarked_stative : stativeMarkedness Verb.Root.ChangeType.propertyConcept = Markedness.unmarked

PC roots produce unmarked statives.

theorem BeaversEtAl2021.markedness_from_semantics (ct : Verb.Root.ChangeType) : verbalMarkedness ct = Markedness.unmarked ↔ ct.entailsChange = true

The markedness generalization is equivalent to the semantic distinction.

def BeaversEtAl2021.rootTypeFromChangeEntailment (p : ArgumentStructure.EntailmentProfile) : Verb.Root.ChangeType

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

Equations

• BeaversEtAl2021.rootTypeFromChangeEntailment p = if p.changeOfState = true then Verb.Root.ChangeType.result else Verb.Root.ChangeType.propertyConcept

theorem BeaversEtAl2021.result_object_has_changeOfState : rootTypeFromChangeEntailment ArgumentStructure.accomplishmentObjectProfile = Verb.Root.ChangeType.result ∧ rootTypeFromChangeEntailment ArgumentStructure.contactObject = Verb.Root.ChangeType.propertyConcept

A result verb's object (accomplishment template) has changeOfState = true, so it patterns with result roots. Contact-verb objects (kick: CA+St, no entailed change per [Bea11]) fall on the other side of the bridge.

theorem BeaversEtAl2021.die_result_pattern : rootTypeFromChangeEntailment ArgumentStructure.disappearance.subjectProfile = Verb.Root.ChangeType.result

Die subject undergoes change → result-type pattern.

def BeaversEtAl2021.requiresBECOME : Verb.Root.ChangeType → Bool

Result roots MUST combine with a template containing BECOME (achievement or accomplishment): the root's change entailment is redundant with BECOME. PC roots CAN combine with any template.

Equations

• BeaversEtAl2021.requiresBECOME Verb.Root.ChangeType.result = true
• BeaversEtAl2021.requiresBECOME Verb.Root.ChangeType.propertyConcept = false

theorem BeaversEtAl2021.result_root_gets_become_template : requiresBECOME Verb.Root.ChangeType.result = true

Result roots always get templates with BECOME.

def BeaversEtAl2021.templateHasBECOME : ArgumentStructure.EventStructure.Template → Bool

Achievement and accomplishment templates contain BECOME.

Equations

• BeaversEtAl2021.templateHasBECOME ArgumentStructure.EventStructure.Template.achievement = true
• BeaversEtAl2021.templateHasBECOME ArgumentStructure.EventStructure.Template.accomplishment = true
• BeaversEtAl2021.templateHasBECOME x✝ = false

theorem BeaversEtAl2021.result_templates_have_become : templateHasBECOME ArgumentStructure.EventStructure.Template.achievement = true ∧ templateHasBECOME ArgumentStructure.EventStructure.Template.accomplishment = true

The templates result roots combine with always have BECOME.

theorem BeaversEtAl2021.state_template_no_become : templateHasBECOME ArgumentStructure.EventStructure.Template.state = false

State template lacks BECOME — only available to PC roots.

theorem BeaversEtAl2021.become_templates_telic : ArgumentStructure.EventStructure.Template.achievement.vendlerClass = Features.VendlerClass.achievement ∧ ArgumentStructure.EventStructure.Template.accomplishment.vendlerClass = Features.VendlerClass.accomplishment

Templates with BECOME map to achievement/accomplishment Vendler classes, both telic.

def BeaversEtAl2021.stativeAspectualProfile : Verb.Root.ChangeType → Features.AspectualProfile

Aspectual profile for root types in their stative use.

Equations

• BeaversEtAl2021.stativeAspectualProfile Verb.Root.ChangeType.propertyConcept = Features.stateProfile
• BeaversEtAl2021.stativeAspectualProfile Verb.Root.ChangeType.result = Features.achievementProfile

def BeaversEtAl2021.stativeVendlerClass (ct : Verb.Root.ChangeType) : Features.VendlerClass

Result root verbs pattern as achievements/accomplishments; PC roots in stative use are states.

Equations

• BeaversEtAl2021.stativeVendlerClass ct = (BeaversEtAl2021.stativeAspectualProfile ct).toVendlerClass

theorem BeaversEtAl2021.root_stative_vendler : stativeVendlerClass Verb.Root.ChangeType.propertyConcept = Features.VendlerClass.state ∧ stativeVendlerClass Verb.Root.ChangeType.result = Features.VendlerClass.achievement

PC roots in stative use are states; result roots pattern as achievements.

inductive BeaversEtAl2021.AdjectivalStructure : Type

[Emb04] posits basic statives ([AspP AspS √ROOT], PC roots only) and result statives ([AspP AspR [vP DP v_become √ROOT]], deverbal; result roots always, PC roots optionally).

• basicStative : AdjectivalStructure
• resultStative : AdjectivalStructure

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqAdjectivalStructure : DecidableEq AdjectivalStructure

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprAdjectivalStructure : Repr AdjectivalStructure

Equations

• BeaversEtAl2021.instReprAdjectivalStructure = { reprPrec := BeaversEtAl2021.instReprAdjectivalStructure.repr }

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

Equations

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

def BeaversEtAl2021.admitsBasicStative : Verb.Root.ChangeType → Bool

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

Equations

• BeaversEtAl2021.admitsBasicStative Verb.Root.ChangeType.propertyConcept = true
• BeaversEtAl2021.admitsBasicStative Verb.Root.ChangeType.result = false

theorem BeaversEtAl2021.admitsBasicStative_iff_no_change (ct : Verb.Root.ChangeType) : admitsBasicStative ct = true ↔ ct.entailsChange = false

This is equivalent to NOT entailing change.

inductive BeaversEtAl2021.AgainReading : Type

Sublexical again attaches low (to the root, restitutive) or high (over vbecome, repetitive). Restitutive is available iff the root is change-free; a result root's state itself entails change, collapsing its low attachment into the repetitive reading.

• restitutive : AgainReading
• repetitive : AgainReading

@[instance_reducible]

instance BeaversEtAl2021.instDecidableEqAgainReading : DecidableEq AgainReading

Equations

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

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

Equations

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

@[instance_reducible]

instance BeaversEtAl2021.instReprAgainReading : Repr AgainReading

Equations

• BeaversEtAl2021.instReprAgainReading = { reprPrec := BeaversEtAl2021.instReprAgainReading.repr }

def BeaversEtAl2021.againReadings : Verb.Root.ChangeType → List AgainReading

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

Equations

• BeaversEtAl2021.againReadings Verb.Root.ChangeType.propertyConcept = [BeaversEtAl2021.AgainReading.restitutive, BeaversEtAl2021.AgainReading.repetitive]
• BeaversEtAl2021.againReadings Verb.Root.ChangeType.result = [BeaversEtAl2021.AgainReading.repetitive]

theorem BeaversEtAl2021.pc_more_again_readings : (againReadings Verb.Root.ChangeType.propertyConcept).length > (againReadings Verb.Root.ChangeType.result).length

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

theorem BeaversEtAl2021.result_no_restitutive : AgainReading.restitutive ∉ againReadings Verb.Root.ChangeType.result

Result roots lack the restitutive reading.

theorem BeaversEtAl2021.pc_has_restitutive : AgainReading.restitutive ∈ againReadings Verb.Root.ChangeType.propertyConcept

PC roots have the restitutive reading.

theorem BeaversEtAl2021.entails_change_implies_become_template (ct : Verb.Root.ChangeType) (h : ct.entailsChange = true) : requiresBECOME ct = true

If a root entails change, its verb is associated with a template containing BECOME (§9) — even when the change comes from the ROOT, not the template.

theorem BeaversEtAl2021.no_become_implies_no_change (ct : Verb.Root.ChangeType) (h : requiresBECOME ct = false) : ct.entailsChange = false

Conversely: a root not requiring BECOME does not entail change.

theorem BeaversEtAl2021.grand_unification (ct : Verb.Root.ChangeType) : (ct.entailsChange = true → hasSimpleStative ct = false ∧ verbalFormIsMarked ct = false ∧ ct.allowsRestitutiveAgain = false ∧ requiresBECOME ct = true ∧ admitsBasicStative ct = false ∧ verbalMarkedness ct = Markedness.unmarked ∧ stativeMarkedness ct = Markedness.marked) ∧ (ct.entailsChange = false → hasSimpleStative ct = true ∧ verbalFormIsMarked ct = true ∧ ct.allowsRestitutiveAgain = true ∧ requiresBECOME ct = false ∧ admitsBasicStative ct = true ∧ verbalMarkedness ct = Markedness.marked ∧ stativeMarkedness ct = Markedness.unmarked)

The full correlation package. From the single Boolean entailsChange, all of the paper's morphosyntactic predictions follow: one semantic property is the sole determinant of six independently observable properties.

theorem BeaversEtAl2021.root_markedness_from_change (r : Verb.Root.Classification) : verbalMarkedness r.changeType = Markedness.unmarked ↔ r.entailsChange = true

Change entailment determines markedness in the unified Classification.

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

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

The §§8–14 sections below were originally housed in Studies/Coon2019.lean as bridge content between Coon's Chuj data, the present empirical typology, and the root typology substrate. They are relocated here per the chronological- dependency rule (Coon 2019 < Beavers et al. 2021 — only the later paper may reference the earlier).

def BeaversEtAl2021.toCoSRootClass : Verb.Root.ChangeType → CoSRootClass

Map the theory's change type to the empirical root class. These are parallel enums — the bridge makes the correspondence explicit.

Equations

• BeaversEtAl2021.toCoSRootClass Verb.Root.ChangeType.propertyConcept = BeaversEtAl2021.CoSRootClass.propertyConcept
• BeaversEtAl2021.toCoSRootClass Verb.Root.ChangeType.result = BeaversEtAl2021.CoSRootClass.result

def BeaversEtAl2021.fromCoSRootClass : CoSRootClass → Verb.Root.ChangeType

Map back from empirical to theory.

Equations

• BeaversEtAl2021.fromCoSRootClass BeaversEtAl2021.CoSRootClass.propertyConcept = Verb.Root.ChangeType.propertyConcept
• BeaversEtAl2021.fromCoSRootClass BeaversEtAl2021.CoSRootClass.result = Verb.Root.ChangeType.result

theorem BeaversEtAl2021.roundtrip_left (ct : Verb.Root.ChangeType) : fromCoSRootClass (toCoSRootClass ct) = ct

The mapping is a bijection (left inverse).

theorem BeaversEtAl2021.roundtrip_right (rc : CoSRootClass) : toCoSRootClass (fromCoSRootClass rc) = rc

The mapping is a bijection (right inverse).

theorem BeaversEtAl2021.change_denial_matches_entailsChange (rc : CoSRootClass) : changeDenialTest rc = DiagnosticResult.positive ↔ (fromCoSRootClass rc).entailsChange = false

The empirical changeDenialTest agrees with the theory's entailsChange.

Theory: ChangeType.entailsChange .result = true (result roots entail change) Empirical: changeDenialTest.result =.negative ("#The shattered vase has never shattered" is contradictory — the state entails prior change)

The relationship is: entailsChange = true ↔ changeDenial = negative.

theorem BeaversEtAl2021.restitutive_again_matches (rc : CoSRootClass) : restitutiveAgainTest rc = DiagnosticResult.positive ↔ (fromCoSRootClass rc).allowsRestitutiveAgain = true

The empirical restitutiveAgainTest agrees with the theory's allowsRestitutiveAgain.

theorem BeaversEtAl2021.diagnostics_align_with_theory (rc : CoSRootClass) : have rt := fromCoSRootClass rc; (changeDenialTest rc = DiagnosticResult.negative ↔ rt.entailsChange = true) ∧ (restitutiveAgainTest rc = DiagnosticResult.negative ↔ rt.allowsRestitutiveAgain = false)

Both diagnostics jointly align with the full semantic correlate package. The bridge form of semantic_determines_morphosyntax.

theorem BeaversEtAl2021.pc_stative_prediction_matches_data : hasSimpleStative Verb.Root.ChangeType.propertyConcept = true ∧ (List.filter (fun (r : RootMeaning) => decide (r.nSimpleStative * 2 ≥ r.nLanguages)) pcRoots).length ≥ pcRoots.length - 1

Theory predicts: PC roots have simple statives. Data confirms: 7 of 8 PC sample roots have ≥ 50% attestation. The one exception (oldRoot, age class) has 0 — noted by the present paper as a crosslinguistic outlier.

theorem BeaversEtAl2021.result_no_stative_prediction_matches_data : hasSimpleStative Verb.Root.ChangeType.result = false ∧ (resultRoots.all fun (r : RootMeaning) => decide (r.nSimpleStative * 10 ≤ r.nLanguages)) = true

Theory predicts: result roots LACK simple statives. Data confirms: all 10 result sample roots have ≤ 10% attestation.

theorem BeaversEtAl2021.markedness_prediction_matches_statistics : verbalMarkedness Verb.Root.ChangeType.propertyConcept = Markedness.marked ∧ verbalMarkedness Verb.Root.ChangeType.result = Markedness.unmarked ∧ simpleStativeComparison.pcMedian > simpleStativeComparison.resultMedian ∧ verbalMarkednessComparison.pcMedian > verbalMarkednessComparison.resultMedian

Theory predicts: PC verbs are morphologically marked; result verbs are unmarked (Markedness Generalization, [BEJ+21]). Data confirms: PC median marked % (56.01) > result median (15.20).

theorem BeaversEtAl2021.unattested_type_matches_complementarity : LanguageType.allAttested.length = 3 ∧ ∀ (ct : Verb.Root.ChangeType), verbalMarkedness ct ≠ stativeMarkedness ct

The theory's markedness complementarity predicts that if a language marks PC verbs, it should NOT also show result verbs as more marked than PC verbs. The fourth logically possible language type (result marked, PC unmarked) is unattested — exactly 3 types are attested. This matches the theory: markedness_complementarity says verbal and stative markedness are always opposite.

def BeaversEtAl2021.rootTV_res : Verb.Root.Classification

[BEJ+21]'s result-root row for [Coo19]'s √TV class: the shared coordinates are RootClass.toClassification; only the change-entailment column is this paper's subdivision (Coon does not subdivide √TV).

Equations

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

def BeaversEtAl2021.rootTV_pc : Verb.Root.Classification

The property-concept row of the √TV subdivision (no change entailment).

Equations

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

def BeaversEtAl2021.rootITV : Verb.Root.Classification

Coon's √ITV coordinates, reused unchanged.

Equations

• BeaversEtAl2021.rootITV = Chuj.RootClass.itv.toClassification

def BeaversEtAl2021.rootPOS : Verb.Root.Classification

Coon's √POS coordinates, reused unchanged.

Equations

• BeaversEtAl2021.rootPOS = Chuj.RootClass.pos.toClassification

theorem BeaversEtAl2021.chuj_tv_res_is_result_root : rootTV_res.entailsChange = true ∧ hasSimpleStative rootTV_res.changeType = false ∧ verbalMarkedness rootTV_res.changeType = Markedness.unmarked

Chuj √TV result roots instantiate the theory's result root predictions: entails change, no simple stative, unmarked verb.

theorem BeaversEtAl2021.chuj_tv_pc_is_pc_root : rootTV_pc.entailsChange = false ∧ hasSimpleStative rootTV_pc.changeType = true ∧ verbalMarkedness rootTV_pc.changeType = Markedness.marked

Chuj √TV PC roots instantiate the theory's PC root predictions: no change entailment, has simple stative, marked verb.

theorem BeaversEtAl2021.chuj_witnesses_orthogonality : rootTV_res.valency = {ArgumentStructure.ArgPosition.internal} ∧ rootTV_res.changeType = Verb.Root.ChangeType.result ∧ rootTV_pc.valency = {ArgumentStructure.ArgPosition.internal} ∧ rootTV_pc.changeType = Verb.Root.ChangeType.propertyConcept ∧ rootPOS.valency = ∅ ∧ rootPOS.changeType = Verb.Root.ChangeType.propertyConcept

The Chuj fragment witnesses cells of the (valency × changeType) matrix: theme-taking roots with and without change entailment, and valency-free property-concept roots (√POS — √ITV is unaccusative and theme-taking per [Coo19] §3.3).

theorem BeaversEtAl2021.chuj_roots_satisfy_grand_unification : (hasSimpleStative rootTV_res.changeType = false ∧ verbalFormIsMarked rootTV_res.changeType = false ∧ rootTV_res.changeType.allowsRestitutiveAgain = false) ∧ (hasSimpleStative rootTV_pc.changeType = true ∧ verbalFormIsMarked rootTV_pc.changeType = true ∧ rootTV_pc.changeType.allowsRestitutiveAgain = true) ∧ hasSimpleStative rootITV.changeType = true ∧ verbalFormIsMarked rootITV.changeType = true ∧ rootITV.changeType.allowsRestitutiveAgain = true

Per-root class verification: each Chuj root's change entailment matches its predicted morphosyntactic correlates via grand_unification.

theorem BeaversEtAl2021.pc_roots_classified_and_predicted : (pcRoots.all fun (x : RootMeaning) => x.rootClass == CoSRootClass.propertyConcept) = true ∧ hasSimpleStative Verb.Root.ChangeType.propertyConcept = true

Every PC root in the empirical sample is classified as PC, and the theory predicts PC roots should have simple statives — they do.

theorem BeaversEtAl2021.result_roots_classified_and_predicted : (resultRoots.all fun (x : RootMeaning) => x.rootClass == CoSRootClass.result) = true ∧ hasSimpleStative Verb.Root.ChangeType.result = false

Every result root in the empirical sample is classified as result, and the theory predicts result roots lack simple statives — they do.