Chuj Verb Building: Empirical Data and Bridge Theorems

@cite{coon-2019}

Minimalist analysis and bridge theorems for @cite{coon-2019} "Building verbs in Chuj: Consequences for the nature of roots." Journal of Linguistics 55(1): 35–81.

Theory-neutral data (root classes, voice morphology, paradigm grammaticality, -aj distribution, agent diagnostics, root lexicon) lives in the Chuj fragment (Fragments/Chuj/VerbBuilding.lean). This file provides:

Paradigm examples (§§1–2)

Glossed Chuj sentences with root, voice suffix, and grammaticality.

Minimalist analysis (§§3–9)

Voice heads as Minimalism.VoiceHead instances, event decomposition via buildDecomposition, existential closure (-aj), and division of labor / causative alternation proved from the Voice–root split.

Bridge theorems (§§10–16)

Connect the fragment's theory-neutral types (CRootClass, ChujVoiceSuffix, isGrammatical, etc.) to Minimalist VoiceHead properties and to the @cite{beavers-etal-2021} root typology.

Chuj fragment bridge (§§10–15)

1. Root class ↔ Root arity: CRootClass maps to Root values. √TV = selectsTheme, others = noTheme.
2. Voice suffix ↔ VoiceHead: theta assignment, D feature, phase head.
3. Paradigm predictions: isGrammatical matches data attestation.
4. -aj predictions: hasImplicitExternal / triggersAj match -aj distribution.
5. Agent diagnostics: assignsTheta matches agent adverb / by-phrase.
6. Division of labor: formsBareTransitive aligns with arity.

Root typology bridge (§§17–23)

Connects Theories/Morphology/RootTypology.lean (@cite{beavers-etal-2021}) to empirical data in Phenomena/Causation/Studies/BeaversEtAl2021.lean.

1. Classification isomorphism: The theory's RootType and the phenomena's CoSRootClass are provably isomorphic — they describe the same partition.

2. Diagnostic alignment: The phenomena's semantic diagnostics (changeDenialTest, restitutiveAgainTest) agree exactly with the theory's Boolean correlates (entailsChange, allowsRestitutiveAgain).

3. Prediction ↔ attestation: The theory predicts PC roots HAVE simple statives and result roots LACK them; the empirical data confirms this (PC: 7/8 sample roots ≥ 50%; result: all 10 sample roots ≤ 10%).

4. Markedness prediction: The theory predicts PC verbs are marked and result verbs are unmarked; the statistical comparison confirms PC median (56.01%) exceeds result median (15.20%).

5. Fragment grounding: The Chuj fragment's Root values instantiate the theory's predictions — e.g., rootTV_res.entailsChange = true matches the theory's RootType.entailsChange.result = true.

structure Phenomena.Causation.Studies.Coon2019.ChujExample : Type

A glossed Chuj example sentence.

• exNumber : ℕ

  Example number in the paper

• page : ℕ

  Page number

• chuj : String

  Chuj form

• english : String

  English translation

• verb : Fragments.Chuj.ChujRoot

  Root used (from the Chuj fragment lexicon)

• voice : Fragments.Chuj.ChujVoiceSuffix

  Voice suffix

• grammatical : Bool

  Whether the example is grammatical

def Phenomena.Causation.Studies.Coon2019.instReprChujExample.repr : ChujExample → ℕ → Std.Format

Equations

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

instance Phenomena.Causation.Studies.Coon2019.instReprChujExample : Repr ChujExample

Equations

• Phenomena.Causation.Studies.Coon2019.instReprChujExample = { reprPrec := Phenomena.Causation.Studies.Coon2019.instReprChujExample.repr }

def Phenomena.Causation.Studies.Coon2019.ex10a : ChujExample

(10a) Active transitive: √TV + Ø (§2.2, p. 41).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex7a : ChujExample

(7a) √ITV + null v (§2.1, p. 40).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex23a : ChujExample

(23a) √POS + -w (§3, p. 48).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex16b : ChujExample

(16b) √NOM + -w (§2.5, p. 45).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex62 : ChujExample

(62) √TV + -chaj (passive, §4.1.1, p. 68).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex59 : ChujExample

(59) √TV + -j (agentless passive, §4.1.2, p. 67).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex63a : ChujExample

(63a) Agent adverb with -chaj: grammatical (§4.1.1, p. 68).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex67a : ChujExample

(67a) Agent adverb with -j: ungrammatical (§4.1.2, p. 70).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex54a : ChujExample

(54a) √TV + -w incorporation antipassive (§4, p. 64).

Equations

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

def Phenomena.Causation.Studies.Coon2019.ex55 : ChujExample

(55b) √TV + -w absolutive antipassive (§4, p. 65).

Equations

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

theorem Phenomena.Causation.Studies.Coon2019.examples_grammaticality : ex10a.grammatical = true ∧ ex7a.grammatical = true ∧ ex23a.grammatical = true ∧ ex16b.grammatical = true ∧ ex62.grammatical = true ∧ ex59.grammatical = true ∧ ex63a.grammatical = true ∧ ex67a.grammatical = false ∧ ex54a.grammatical = true ∧ ex55.grammatical = true

Grammatical examples are predicted grammatical; ungrammatical examples are predicted ungrammatical.

def Phenomena.Causation.Studies.Coon2019.vØ : Minimalism.VoiceHead

Active transitive v/Voice⁰ (Ø): introduces overt agent in Spec,VoiceP, assigns ergative case, phase head (v*).

Equations

• Phenomena.Causation.Studies.Coon2019.vØ = { flavor := Minimalism.VoiceFlavor.agentive, hasD := true, phaseHead := true }

def Phenomena.Causation.Studies.Coon2019.v_w : Minimalism.VoiceHead

Agentive intransitive v/Voice⁰ (-w): introduces overt agent in Spec,VoiceP but assigns absolutive (not ergative) case (p. 54). Merges directly with root — cannot attach to derived stems (p. 54, (34b)). Used with √NOM and √POS to verbalize roots, and with √TV in incorporation antipassives (where the theme is a bare NP). Also models the null intransitive v/Voice⁰ for √ITV roots (p. 40): both introduce an agent and assign absolutive, differing only in overt (-w) vs null morphological realization.

Equations

• Phenomena.Causation.Studies.Coon2019.v_w = { flavor := Minimalism.VoiceFlavor.agentive, hasD := true, phaseHead := false }

def Phenomena.Causation.Studies.Coon2019.v_ch : Minimalism.VoiceHead

Passive v/Voice⁰ (-ch): assigns θ-role to an implicit (existentially bound) external argument (p. 68–69). Agent-oriented adverbs and by-phrases are licensed, confirming semantic presence of agent. Only combines with √TV roots.

Equations

• Phenomena.Causation.Studies.Coon2019.v_ch = { flavor := Minimalism.VoiceFlavor.agentive, hasD := false, phaseHead := false }

def Phenomena.Causation.Studies.Coon2019.v_j : Minimalism.VoiceHead

Agentless passive v/Voice⁰ (-j): verbalizes stem but introduces no external argument — neither overt nor implicit (p. 70: "does not assign a thematic role and does not merge an external argument"). No agent-oriented adverbs, no agentive by-phrases. Used with √TV (agentless passive) and non-transitive roots (inchoative/stative readings).

Equations

• Phenomena.Causation.Studies.Coon2019.v_j = { flavor := Minimalism.VoiceFlavor.nonThematic, hasD := false, phaseHead := false }

def Phenomena.Causation.Studies.Coon2019.resultLower : List Minimalism.VerbHead

Lower event structure for result roots: cause + change + result state.

Equations

• Phenomena.Causation.Studies.Coon2019.resultLower = [Minimalism.VerbHead.vCAUSE, Minimalism.VerbHead.vGO, Minimalism.VerbHead.vBE]

def Phenomena.Causation.Studies.Coon2019.activityLower : List Minimalism.VerbHead

Lower event structure for activity roots (√TV PC, √ITV, √NOM): no sub-eventive decomposition below Voice.

Equations

• Phenomena.Causation.Studies.Coon2019.activityLower = []

def Phenomena.Causation.Studies.Coon2019.positionalLower : List Minimalism.VerbHead

Lower event structure for positional roots (√POS): stative.

Equations

• Phenomena.Causation.Studies.Coon2019.positionalLower = [Minimalism.VerbHead.vBE]

theorem Phenomena.Causation.Studies.Coon2019.agentive_voices_assign_theta : vØ.assignsTheta = true ∧ v_w.assignsTheta = true ∧ v_ch.assignsTheta = true

All three agentive voices (Ø, -w, -ch) assign a θ-role.

theorem Phenomena.Causation.Studies.Coon2019.v_j_no_theta : v_j.assignsTheta = false

-j does NOT assign a θ-role: agentless (p. 70).

theorem Phenomena.Causation.Studies.Coon2019.only_vØ_is_phase : vØ.phaseHead = true ∧ v_w.phaseHead = false ∧ v_ch.phaseHead = false ∧ v_j.phaseHead = false

Only Ø is a phase head (assigns ergative case).

theorem Phenomena.Causation.Studies.Coon2019.tv_res_active : Minimalism.isCausative (Minimalism.buildDecomposition vØ resultLower) = true

√TV result + Ø → causative [vDO, vGO, vBE] (active transitive).

theorem Phenomena.Causation.Studies.Coon2019.tv_res_passive_ch : Minimalism.isCausative (Minimalism.buildDecomposition v_ch resultLower) = true

√TV result + -ch → causative [vDO, vGO, vBE] (passive with implicit agent). Event structure is still causative — the agent is semantically present.

theorem Phenomena.Causation.Studies.Coon2019.tv_res_agentless : Minimalism.isInchoative (Minimalism.buildDecomposition v_j resultLower) = true

√TV result + -j → inchoative [vGO, vBE] (agentless passive / anticausative). No agent at all — the event is a pure change-of-state (p. 70).

theorem Phenomena.Causation.Studies.Coon2019.itv_intransitive : Minimalism.isActivity (Minimalism.buildDecomposition v_w activityLower) = true

√ITV + v/Voice⁰ → activity [vDO] (intransitive). Uses v_w, which shares formal properties with the null intransitive v/Voice⁰ for √ITV (both are agentive, non-ERG-assigning; p. 40).

theorem Phenomena.Causation.Studies.Coon2019.pos_agentive : Minimalism.buildDecomposition v_w positionalLower = [Minimalism.VerbHead.vDO, Minimalism.VerbHead.vBE]

√POS + -w → [vDO, vBE]: agent assumes a position (agentive stative). (p. 48, (23)): chot-w-i "The frog hopped."

theorem Phenomena.Causation.Studies.Coon2019.nom_agentive : Minimalism.isActivity (Minimalism.buildDecomposition v_w activityLower) = true

√NOM + -w → activity [vDO] (denominal agentive intransitive). (p. 45, (16b)): chanhal-w-i "I danced."

def Phenomena.Causation.Studies.Coon2019.hasImplicitExternal (v : Minimalism.VoiceHead) : Bool

Does this Voice head have an implicit (existentially bound) external argument? True when Voice assigns θ but has no overt specifier.

Equations

• Phenomena.Causation.Studies.Coon2019.hasImplicitExternal v = (v.assignsTheta && !v.hasD)

def Phenomena.Causation.Studies.Coon2019.triggersAj (v : Minimalism.VoiceHead) (implicitInternal : Bool) : Bool

-aj (Existential Closure) surfaces when there is any implicit argument: implicit external (from Voice, as in -ch) or implicit internal (from theme suppression in absolutive antipassive -w-aj).

implicitInternal is true when a √TV root's theme is not filled by an overt DP (absolutive antipassive, not incorporation antipassive).

Equations

• Phenomena.Causation.Studies.Coon2019.triggersAj v implicitInternal = (Phenomena.Causation.Studies.Coon2019.hasImplicitExternal v || implicitInternal)

theorem Phenomena.Causation.Studies.Coon2019.ch_triggers_aj : hasImplicitExternal v_ch = true

-ch always triggers -aj (implicit external agent; p. 69).

theorem Phenomena.Causation.Studies.Coon2019.vØ_no_implicit : hasImplicitExternal vØ = false

Ø never has an implicit external (agent is overt ERG DP).

theorem Phenomena.Causation.Studies.Coon2019.v_w_no_implicit : hasImplicitExternal v_w = false

-w never has an implicit external (agent is overt ABS DP; p. 54).

theorem Phenomena.Causation.Studies.Coon2019.v_j_no_implicit : hasImplicitExternal v_j = false

-j has no implicit external (there is no agent at all, not even implicit; p. 70: "no thematic agent, implicit or otherwise").

theorem Phenomena.Causation.Studies.Coon2019.ch_aj_passive : triggersAj v_ch false = true

-ch-aj: passive of √TV with implicit agent (ex. (58), p. 66).

theorem Phenomena.Causation.Studies.Coon2019.w_aj_antipassive : triggersAj v_w true = true

-w-aj: absolutive antipassive (√TV theme is implicit; ex. (58), p. 66).

theorem Phenomena.Causation.Studies.Coon2019.w_incorporation_no_aj : triggersAj v_w false = false

-w incorporation antipassive: theme is overt bare NP → no -aj (ex. (58), p. 66; cf. (26b), p. 50).

theorem Phenomena.Causation.Studies.Coon2019.w_cross_class : Minimalism.isActivity (Minimalism.buildDecomposition v_w activityLower) = true ∧ Minimalism.buildDecomposition v_w positionalLower = [Minimalism.VerbHead.vDO, Minimalism.VerbHead.vBE] ∧ Minimalism.isActivity (Minimalism.buildDecomposition v_w activityLower) = true

-w serves the same structural function across three root classes: it merges directly with the root, verbalizes it, and introduces an agent without assigning ERG (p. 54–56). The only difference is the root's lower event structure.

theorem Phenomena.Causation.Studies.Coon2019.minimalist_division_of_labor : Minimalism.isCausative (Minimalism.buildDecomposition vØ resultLower) = true ∧ Minimalism.isInchoative (Minimalism.buildDecomposition v_j resultLower) = true ∧ Fragments.Chuj.rootTV_res.arity.hasInternalArg = true ∧ Fragments.Chuj.rootITV.arity.hasInternalArg = false

Division of labor (@cite{coon-2019}, ex. (2)/(77), p. 75): the root determines whether a theme is present; Voice determines whether an agent is present. Same root with different Voice → different event type; same Voice with different root → same external argument status.

theorem Phenomena.Causation.Studies.Coon2019.chuj_causative_alternation_result : Minimalism.isCausative (Minimalism.buildDecomposition vØ resultLower) = vØ.assignsTheta ∧ Minimalism.isCausative (Minimalism.buildDecomposition v_w resultLower) = v_w.assignsTheta ∧ Minimalism.isCausative (Minimalism.buildDecomposition v_ch resultLower) = v_ch.assignsTheta ∧ Minimalism.isCausative (Minimalism.buildDecomposition v_j resultLower) = v_j.assignsTheta

The causative alternation in Chuj is determined by Voice, not by the root (instantiation of voice_determines_causativity_go_be for Chuj heads). For result roots, causativity tracks exactly with θ-assignment.

def Phenomena.Causation.Studies.Coon2019.toFragmentRoot : Fragments.Chuj.CRootClass → Root

Map the phenomena's root class to the fragment's Root. This connects theory-neutral distributional classes to the theoretically analyzed Root structure. √TV maps to rootTV_res as a representative — the choice between rootTV_res and rootTV_pc is arbitrary for arity (both are selectsTheme); only changeType differs.

Equations

• Phenomena.Causation.Studies.Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.tv = Fragments.Chuj.rootTV_res
• Phenomena.Causation.Studies.Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.itv = Fragments.Chuj.rootITV
• Phenomena.Causation.Studies.Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.pos = Fragments.Chuj.rootPOS
• Phenomena.Causation.Studies.Coon2019.toFragmentRoot Fragments.Chuj.CRootClass.nom = Fragments.Chuj.rootNOM

theorem Phenomena.Causation.Studies.Coon2019.root_class_arity_alignment : (toFragmentRoot Fragments.Chuj.CRootClass.tv).arity = RootArity.selectsTheme ∧ (toFragmentRoot Fragments.Chuj.CRootClass.itv).arity = RootArity.noTheme ∧ (toFragmentRoot Fragments.Chuj.CRootClass.pos).arity = RootArity.noTheme ∧ (toFragmentRoot Fragments.Chuj.CRootClass.nom).arity = RootArity.noTheme

√TV maps to a theme-selecting root; all others map to non-theme roots. This is the formal content of the observation that only √TV forms bare transitive stems (§2.2).

theorem Phenomena.Causation.Studies.Coon2019.bare_transitive_iff_theme (rc : Fragments.Chuj.CRootClass) : Fragments.Chuj.formsBareTransitive rc = (toFragmentRoot rc).arity.hasInternalArg

The data's formsBareTransitive matches the fragment's hasInternalArg. Only roots that select a theme can form bare transitive stems.

def Phenomena.Causation.Studies.Coon2019.toVoiceHead : Fragments.Chuj.ChujVoiceSuffix → Minimalism.VoiceHead

Map the phenomena's voice suffix to the Minimalist VoiceHead.

Equations

• Phenomena.Causation.Studies.Coon2019.toVoiceHead Fragments.Chuj.ChujVoiceSuffix.null = Phenomena.Causation.Studies.Coon2019.vØ
• Phenomena.Causation.Studies.Coon2019.toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch = Phenomena.Causation.Studies.Coon2019.v_ch
• Phenomena.Causation.Studies.Coon2019.toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j = Phenomena.Causation.Studies.Coon2019.v_j
• Phenomena.Causation.Studies.Coon2019.toVoiceHead Fragments.Chuj.ChujVoiceSuffix.w = Phenomena.Causation.Studies.Coon2019.v_w

theorem Phenomena.Causation.Studies.Coon2019.theta_alignment (vs : Fragments.Chuj.ChujVoiceSuffix) : vs.hasAgent = (toVoiceHead vs).assignsTheta

Theta assignment matches: the data's hasAgent agrees with the fragment's assignsTheta for all four voice suffixes.

theorem Phenomena.Causation.Studies.Coon2019.d_feature_alignment : (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.null).hasD = true ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.w).hasD = true ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch).hasD = false ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j).hasD = false

External argument status matches D feature: overt external arg ↔ hasD = true.

theorem Phenomena.Causation.Studies.Coon2019.phase_head_alignment : (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.null).phaseHead = true ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch).phaseHead = false ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j).phaseHead = false ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.w).phaseHead = false

Only Ø is a phase head (assigns ERG case).

theorem Phenomena.Causation.Studies.Coon2019.agent_adverb_matches_theta (vs : Fragments.Chuj.ChujVoiceSuffix) : Fragments.Chuj.agentAdverbOK vs = (toVoiceHead vs).assignsTheta

The data's agent adverb diagnostic matches the fragment's theta assignment. Agent-oriented adverbs require a theta-role-bearing Voice head.

theorem Phenomena.Causation.Studies.Coon2019.passive_contrast : (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.ch).assignsTheta = true ∧ Fragments.Chuj.agentAdverbOK Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ Fragments.Chuj.byPhraseOK Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ (toVoiceHead Fragments.Chuj.ChujVoiceSuffix.j).assignsTheta = false ∧ Fragments.Chuj.agentAdverbOK Fragments.Chuj.ChujVoiceSuffix.j = false ∧ Fragments.Chuj.byPhraseOK Fragments.Chuj.ChujVoiceSuffix.j = false

The -ch vs -j contrast is the critical test: both are passives (no overt external arg), but they differ in theta assignment. The agent diagnostic data confirms the fragment's distinction.

theorem Phenomena.Causation.Studies.Coon2019.aj_passive_matches_implicit (vs : Fragments.Chuj.ChujVoiceSuffix) : Fragments.Chuj.ajOnPassive vs = hasImplicitExternal (toVoiceHead vs)

The data's -aj on passives matches the fragment's hasImplicitExternal. -aj appears when there is an implicit (but not absent) external argument.

theorem Phenomena.Causation.Studies.Coon2019.aj_full_distribution : triggersAj v_ch false = true ∧ Fragments.Chuj.ajOnPassive Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ triggersAj v_j false = false ∧ Fragments.Chuj.ajOnPassive Fragments.Chuj.ChujVoiceSuffix.j = false ∧ triggersAj v_w true = true ∧ Fragments.Chuj.ajOnAntipassive Fragments.Chuj.AntipassiveType.absolutive = true ∧ triggersAj v_w false = false ∧ Fragments.Chuj.ajOnAntipassive Fragments.Chuj.AntipassiveType.incorporation = false

The fragment's triggersAj predicts the data's full -aj distribution:

• -ch (implicit ext) → -aj
• -j (no ext) → no -aj
• -w absolutive (implicit int) → -aj
• -w incorporation (overt int) → no -aj

theorem Phenomena.Causation.Studies.Coon2019.event_decomposition_matches_data : Minimalism.isCausative (Minimalism.buildDecomposition vØ resultLower) = true ∧ Minimalism.isInchoative (Minimalism.buildDecomposition v_j resultLower) = true ∧ Minimalism.isCausative (Minimalism.buildDecomposition v_ch resultLower) = true ∧ Minimalism.isActivity (Minimalism.buildDecomposition v_w activityLower) = true

The fragment predicts correct event decompositions for each root×voice combination attested in the data.

√TV result + Ø → causative (active transitive) √TV result + -j → inchoative (agentless passive / anticausative) √TV result + -ch → causative (passive with implicit agent) √ITV + -w → activity (intransitive)

theorem Phenomena.Causation.Studies.Coon2019.division_of_labor_matches_data : Fragments.Chuj.formsBareTransitive Fragments.Chuj.CRootClass.tv = true ∧ Fragments.Chuj.rootTV_res.arity.hasInternalArg = true ∧ Fragments.Chuj.formsBareTransitive Fragments.Chuj.CRootClass.itv = false ∧ Fragments.Chuj.rootITV.arity.hasInternalArg = false ∧ Fragments.Chuj.ChujVoiceSuffix.null.extArgStatus = Fragments.Chuj.ExtArgStatus.overt_erg ∧ Fragments.Chuj.ChujVoiceSuffix.ch.extArgStatus = Fragments.Chuj.ExtArgStatus.implicit ∧ Fragments.Chuj.ChujVoiceSuffix.j.extArgStatus = Fragments.Chuj.ExtArgStatus.absent

The core empirical claim (ex. (2)/(77), p. 75): roots determine internal arguments, Voice determines external arguments.

The data confirms this in two ways:

1. Theme persistence: √TV always has an internal arg regardless of Voice
2. Voice determines agent: same root with Ø has overt agent, with -ch has implicit agent, with -j has no agent

theorem Phenomena.Causation.Studies.Coon2019.theme_persists_all_voices : Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.null = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.ch = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.j = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.tv Fragments.Chuj.ChujVoiceSuffix.w = true ∧ Fragments.Chuj.rootTV_res.arity.hasInternalArg = true

Theme persistence across all four voice forms for √TV. The data shows √TV maintains its internal argument in active (Ø), passive (-ch), agentless passive (-j), and antipassive (-w). The fragment encodes this as a root property (arity), not a derived property — so it holds by construction.

theorem Phenomena.Causation.Studies.Coon2019.denotation_type_alignment : (toFragmentRoot Fragments.Chuj.CRootClass.tv).denotationType = some RootDenotationType.eventPred ∧ (toFragmentRoot Fragments.Chuj.CRootClass.itv).denotationType = some RootDenotationType.eventPred ∧ (toFragmentRoot Fragments.Chuj.CRootClass.pos).denotationType = some RootDenotationType.measureFn ∧ (toFragmentRoot Fragments.Chuj.CRootClass.nom).denotationType = some RootDenotationType.entityPred

The four root classes have distinct denotation types (@cite{coon-2019}, (3)). The fragment's denotationType field captures these: √TV/√ITV = eventPred ⟨e,⟨s,t⟩⟩, √POS = measureFn ⟨e,⟨s,d⟩⟩, √NOM = entityPred ⟨e,t⟩.

theorem Phenomena.Causation.Studies.Coon2019.tv_itv_same_type_different_arity : (toFragmentRoot Fragments.Chuj.CRootClass.tv).denotationType = (toFragmentRoot Fragments.Chuj.CRootClass.itv).denotationType ∧ (toFragmentRoot Fragments.Chuj.CRootClass.tv).arity ≠ (toFragmentRoot Fragments.Chuj.CRootClass.itv).arity

√TV and √ITV share semantic type (event predicate) but differ in arity. This is the formal content of the observation that both compose with an entity argument per @cite{davis-1997}, but only √TV projects a syntactic complement.

theorem Phenomena.Causation.Studies.Coon2019.w_verbalization_cross_class : Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.pos Fragments.Chuj.ChujVoiceSuffix.w = true ∧ Fragments.Chuj.isGrammatical Fragments.Chuj.CRootClass.nom Fragments.Chuj.ChujVoiceSuffix.w = true ∧ Minimalism.buildDecomposition v_w positionalLower = [Minimalism.VerbHead.vDO, Minimalism.VerbHead.vBE] ∧ Minimalism.isActivity (Minimalism.buildDecomposition v_w activityLower) = true

The -w suffix cross-class generalization: -w verbalizes √POS and √NOM roots (data: both take -w), and the fragment predicts different event structures depending on the root's lower structure.

def Phenomena.Causation.Studies.Coon2019.toCoSRootClass : RootType → BeaversEtAl2021.CoSRootClass

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

Equations

• Phenomena.Causation.Studies.Coon2019.toCoSRootClass RootType.propertyConcept = Phenomena.Causation.Studies.BeaversEtAl2021.CoSRootClass.propertyConcept
• Phenomena.Causation.Studies.Coon2019.toCoSRootClass RootType.result = Phenomena.Causation.Studies.BeaversEtAl2021.CoSRootClass.result

def Phenomena.Causation.Studies.Coon2019.fromCoSRootClass : BeaversEtAl2021.CoSRootClass → RootType

Map back from phenomena to theory.

Equations

• Phenomena.Causation.Studies.Coon2019.fromCoSRootClass Phenomena.Causation.Studies.BeaversEtAl2021.CoSRootClass.propertyConcept = RootType.propertyConcept
• Phenomena.Causation.Studies.Coon2019.fromCoSRootClass Phenomena.Causation.Studies.BeaversEtAl2021.CoSRootClass.result = RootType.result

theorem Phenomena.Causation.Studies.Coon2019.roundtrip_left (rt : RootType) : fromCoSRootClass (toCoSRootClass rt) = rt

The mapping is a bijection (left inverse).

theorem Phenomena.Causation.Studies.Coon2019.roundtrip_right (rc : BeaversEtAl2021.CoSRootClass) : toCoSRootClass (fromCoSRootClass rc) = rc

The mapping is a bijection (right inverse).

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

The phenomena's changeDenialTest agrees with the theory's entailsChange.

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

The relationship is: entailsChange = true ↔ changeDenial = negative. That is, entailing change means the change-denial test FAILS.

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

The phenomena's restitutiveAgainTest agrees with the theory's allowsRestitutiveAgain.

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

Both diagnostics jointly align with the full semantic correlate package. This is the bridge version of semantic_determines_morphosyntax.

theorem Phenomena.Causation.Studies.Coon2019.pc_stative_prediction_matches_data : RootType.propertyConcept.hasSimpleStative = true ∧ (List.filter (fun (r : BeaversEtAl2021.RootMeaning) => decide (r.nSimpleStative * 2 ≥ r.nLanguages)) BeaversEtAl2021.pcRoots).length ≥ BeaversEtAl2021.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 Beavers et al. as a crosslinguistic outlier.

theorem Phenomena.Causation.Studies.Coon2019.result_no_stative_prediction_matches_data : RootType.result.hasSimpleStative = false ∧ (BeaversEtAl2021.resultRoots.all fun (r : BeaversEtAl2021.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 Phenomena.Causation.Studies.Coon2019.markedness_prediction_matches_statistics : verbalMarkedness RootType.propertyConcept = Markedness.marked ∧ verbalMarkedness RootType.result = Markedness.unmarked ∧ BeaversEtAl2021.simpleStativeComparison.pcMedian > BeaversEtAl2021.simpleStativeComparison.resultMedian ∧ BeaversEtAl2021.verbalMarkednessComparison.pcMedian > BeaversEtAl2021.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 Phenomena.Causation.Studies.Coon2019.unattested_type_matches_complementarity : BeaversEtAl2021.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 Phenomena.Causation.Studies.Coon2019.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 Phenomena.Causation.Studies.Coon2019.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 Phenomena.Causation.Studies.Coon2019.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 Phenomena.Causation.Studies.Coon2019.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 Phenomena.Causation.Studies.Coon2019.pc_roots_classified_and_predicted : (BeaversEtAl2021.pcRoots.all fun (x : BeaversEtAl2021.RootMeaning) => x.rootClass == BeaversEtAl2021.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 Phenomena.Causation.Studies.Coon2019.result_roots_classified_and_predicted : (BeaversEtAl2021.resultRoots.all fun (x : BeaversEtAl2021.RootMeaning) => x.rootClass == BeaversEtAl2021.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 Phenomena.Causation.Studies.Coon2019.subclass_counts_match : [PCClass.dimension, PCClass.age, PCClass.value, PCClass.color, PCClass.physicalProperty, PCClass.speed].length = [BeaversEtAl2021.PCSubclass.dimension, BeaversEtAl2021.PCSubclass.age, BeaversEtAl2021.PCSubclass.value, BeaversEtAl2021.PCSubclass.color, BeaversEtAl2021.PCSubclass.physicalProperty, BeaversEtAl2021.PCSubclass.speed].length ∧ [ResultClass.entitySpecificCoS, ResultClass.cooking, ResultClass.breaking, ResultClass.bending, ResultClass.killing, ResultClass.destroying, ResultClass.calibratableCoS, ResultClass.inherentlyDirectedMotion].length = [BeaversEtAl2021.ResultSubclass.entitySpecificCoS, BeaversEtAl2021.ResultSubclass.cooking, BeaversEtAl2021.ResultSubclass.breaking, BeaversEtAl2021.ResultSubclass.bending, BeaversEtAl2021.ResultSubclass.killing, BeaversEtAl2021.ResultSubclass.destroying, BeaversEtAl2021.ResultSubclass.calibratableCoS, BeaversEtAl2021.ResultSubclass.inherentlyDirectedMotion].length

The subclass taxonomies are parallel: the theory's PCClass and the phenomena's PCSubclass have the same constructors. Similarly for ResultClass and ResultSubclass. This is verified by exhaustive mapping (both have 6 PC subclasses and 8 result subclasses).