Cross-Linguistic Typology of Change-of-State Verbs

@cite{dixon-1982} @cite{levin-1993} @cite{beavers-etal-2021} @cite{rose-nichols-2021} @cite{coon-2019}

Empirical data from 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.

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%.

inductive BeaversEtAl2021.CoSRootClass : Type

Two classes of change-of-state verb roots, defined by morphological and semantic diagnostics (@cite{beavers-etal-2021} §3.1).

Classification criteria:

• PC roots: the root of deadjectival CoS verbs (@cite{levin-1993}:245); describe @cite{dixon-1982}'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

@[implicit_reducible]

instance BeaversEtAl2021.instDecidableEqCoSRootClass : DecidableEq CoSRootClass

Equations

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

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

Equations

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

@[implicit_reducible]

instance BeaversEtAl2021.instReprCoSRootClass : Repr CoSRootClass

Equations

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

inductive BeaversEtAl2021.PCSubclass : Type

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

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

@[implicit_reducible]

instance BeaversEtAl2021.instDecidableEqPCSubclass : DecidableEq PCSubclass

Equations

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

@[implicit_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 (@cite{levin-1993}; @cite{beavers-etal-2021} ex. 6).

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

@[implicit_reducible]

instance BeaversEtAl2021.instDecidableEqResultSubclass : DecidableEq ResultSubclass

Equations

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

@[implicit_reducible]

instance BeaversEtAl2021.instReprResultSubclass : Repr ResultSubclass

Equations

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

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

Equations

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

inductive BeaversEtAl2021.ParadigmPosition : Type

The five positions in a CoS verb paradigm (@cite{beavers-etal-2021} eq. 40). Every root meaning is associated with (up to) five forms.

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

@[implicit_reducible]

instance BeaversEtAl2021.instDecidableEqParadigmPosition : DecidableEq ParadigmPosition

Equations

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

@[implicit_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 (@cite{beavers-etal-2021} eq. 41, generalizing @cite{haspelmath-1993}:90–92).

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

@[implicit_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.

@[implicit_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)

@[implicit_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; @cite{beavers-etal-2021} 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 : ℕ

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

Equations

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

@[implicit_reducible]

instance BeaversEtAl2021.instReprTypologicalComparison : Repr TypologicalComparison

Equations

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

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

@[implicit_reducible]

instance BeaversEtAl2021.instDecidableEqDiagnosticResult : DecidableEq DiagnosticResult

Equations

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

@[implicit_reducible]

instance BeaversEtAl2021.instReprDiagnosticResult : Repr DiagnosticResult

Equations

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

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

Equations

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

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.

@[implicit_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

@[implicit_reducible]

instance BeaversEtAl2021.instDecidableEqLanguageType : DecidableEq LanguageType

Equations

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

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

Equations

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

@[implicit_reducible]

instance BeaversEtAl2021.instReprLanguageType : Repr LanguageType

Equations

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

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.

The §§8–14 sections below were originally housed in Phenomena/Causation/Studies/Coon2019.lean as bridge content between Coon's Chuj data, the present empirical typology, and RootTypology.lean. 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 : RootType → CoSRootClass

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

Equations

• BeaversEtAl2021.toCoSRootClass RootType.propertyConcept = BeaversEtAl2021.CoSRootClass.propertyConcept
• BeaversEtAl2021.toCoSRootClass RootType.result = BeaversEtAl2021.CoSRootClass.result

def BeaversEtAl2021.fromCoSRootClass : CoSRootClass → RootType

Map back from empirical to theory.

Equations

• BeaversEtAl2021.fromCoSRootClass BeaversEtAl2021.CoSRootClass.propertyConcept = RootType.propertyConcept
• BeaversEtAl2021.fromCoSRootClass BeaversEtAl2021.CoSRootClass.result = RootType.result

theorem BeaversEtAl2021.roundtrip_left (rt : RootType) : fromCoSRootClass (toCoSRootClass rt) = rt

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: RootType.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 : RootType.propertyConcept.hasSimpleStative = 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 : RootType.result.hasSimpleStative = 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 RootType.propertyConcept = Markedness.marked ∧ verbalMarkedness RootType.result = Markedness.unmarked ∧ simpleStativeComparison.pcMedian > simpleStativeComparison.resultMedian ∧ verbalMarkednessComparison.pcMedian > verbalMarkednessComparison.resultMedian

Theory predicts: PC verbs are morphologically marked; result verbs are unmarked (Markedness Generalization, @cite{beavers-etal-2021}). Data confirms: PC median marked % (56.01) > result median (15.20).

theorem BeaversEtAl2021.unattested_type_matches_complementarity : LanguageType.allAttested.length = 3 ∧ ∀ (rt : RootType), verbalMarkedness rt ≠ stativeMarkedness rt

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.

theorem BeaversEtAl2021.chuj_tv_res_is_result_root : Fragments.Chuj.rootTV_res.entailsChange = true ∧ Fragments.Chuj.rootTV_res.changeType.hasSimpleStative = false ∧ Fragments.Chuj.rootTV_res.verbalMarkedness = 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 : Fragments.Chuj.rootTV_pc.entailsChange = false ∧ Fragments.Chuj.rootTV_pc.changeType.hasSimpleStative = true ∧ Fragments.Chuj.rootTV_pc.verbalMarkedness = 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 : Fragments.Chuj.rootTV_res.arity = RootArity.selectsTheme ∧ Fragments.Chuj.rootTV_res.changeType = RootType.result ∧ Fragments.Chuj.rootTV_pc.arity = RootArity.selectsTheme ∧ Fragments.Chuj.rootTV_pc.changeType = RootType.propertyConcept ∧ Fragments.Chuj.rootITV.arity = RootArity.noTheme ∧ Fragments.Chuj.rootITV.changeType = RootType.propertyConcept

The Chuj fragment witnesses the full orthogonality theorem: all four cells of the (arity × changeType) matrix are inhabited.

theorem BeaversEtAl2021.chuj_roots_satisfy_grand_unification : (Fragments.Chuj.rootTV_res.changeType.hasSimpleStative = false ∧ Fragments.Chuj.rootTV_res.changeType.verbalFormIsMarked = false ∧ Fragments.Chuj.rootTV_res.changeType.allowsRestitutiveAgain = false) ∧ (Fragments.Chuj.rootTV_pc.changeType.hasSimpleStative = true ∧ Fragments.Chuj.rootTV_pc.changeType.verbalFormIsMarked = true ∧ Fragments.Chuj.rootTV_pc.changeType.allowsRestitutiveAgain = true) ∧ Fragments.Chuj.rootITV.changeType.hasSimpleStative = true ∧ Fragments.Chuj.rootITV.changeType.verbalFormIsMarked = true ∧ Fragments.Chuj.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 ∧ RootType.propertyConcept.hasSimpleStative = 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 ∧ RootType.result.hasSimpleStative = false

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

theorem BeaversEtAl2021.subclass_counts_match : [PCSubclass.dimension, PCSubclass.age, PCSubclass.value, PCSubclass.color, PCSubclass.physicalProperty, PCSubclass.speed].length = 6 ∧ [PCClass.dimension, PCClass.age, PCClass.value, PCClass.color, PCClass.physicalProperty, PCClass.humanPropensity, PCClass.speed].length = 7 ∧ [ResultClass.entitySpecificCoS, ResultClass.cooking, ResultClass.breaking, ResultClass.bending, ResultClass.killing, ResultClass.destroying, ResultClass.calibratableCoS, ResultClass.inherentlyDirectedMotion].length = [ResultSubclass.entitySpecificCoS, ResultSubclass.cooking, ResultSubclass.breaking, ResultSubclass.bending, ResultSubclass.killing, ResultSubclass.destroying, ResultSubclass.calibratableCoS, ResultSubclass.inherentlyDirectedMotion].length

The subclass taxonomies are aligned: B&KG's PCSubclass has 6 categories (matching their Table 2); the theory's PCClass has 7 (adding humanPropensity from @cite{dixon-1982}, attested in @cite{hanink-koontz-garboden-2025}). ResultClass and ResultSubclass match exactly (8 subclasses).