Chuj Modal Indefinite Fragment

@cite{alonso-ovalle-royer-2021} @cite{alonso-ovalle-royer-2024}

Lexical entries for Chuj modal indefinites yalnhej (singular) and komon (mass/plural), following @cite{alonso-ovalle-royer-2024}.

These entries reuse the ModalIndefiniteEntry type from Core/ModalIndefinite.lean, instantiating the three-dimensional typological profile for Chuj.

Connection to VerbBuilding.lean

The Chuj voice system (@cite{coon-2019}, formalized in VerbBuilding.lean) determines whether a yalnhej DP is in external or internal argument position, which in turn constrains the available modal flavor:

• vØ (active transitive): agent = external → epistemic only
• v_ch (passive): theme promoted, agent implicit → both flavors available
• v_w (agentive intransitive): agent = external → epistemic only
• v_j (agentless passive): no agent → internal argument → both flavors

This connection is proved in Phenomena/ModalIndefinites/Studies/AlonsoOvalleRoyer2024.lean.

def Fragments.Chuj.ModalIndefinites.yalnhejEntry : Core.ModalIndefinite.ModalIndefiniteEntry

yalnhej: singular modal indefinite. At-issue, epistemic + random choice, not upper-bounded.

Equations

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

def Fragments.Chuj.ModalIndefinites.komonEntry : Core.ModalIndefinite.ModalIndefiniteEntry

komon: mass/plural modal modifier. At-issue, random choice only, not upper-bounded.

Equations

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

theorem Fragments.Chuj.ModalIndefinites.yalnhej_at_issue : yalnhejEntry.status = Core.ModalIndefinite.ModalComponentStatus.atIssue

theorem Fragments.Chuj.ModalIndefinites.yalnhej_has_epistemic : yalnhejEntry.hasEpistemic = true

theorem Fragments.Chuj.ModalIndefinites.yalnhej_has_rc : yalnhejEntry.hasCircumstantial = true

theorem Fragments.Chuj.ModalIndefinites.yalnhej_not_ub : yalnhejEntry.upperBounded = false

theorem Fragments.Chuj.ModalIndefinites.yalnhej_pos_sensitive : yalnhejEntry.positionSensitive = true

theorem Fragments.Chuj.ModalIndefinites.komon_at_issue : komonEntry.status = Core.ModalIndefinite.ModalComponentStatus.atIssue

theorem Fragments.Chuj.ModalIndefinites.komon_rc_only : komonEntry.hasEpistemic = false ∧ komonEntry.hasCircumstantial = true

theorem Fragments.Chuj.ModalIndefinites.komon_not_ub : komonEntry.upperBounded = false

theorem Fragments.Chuj.ModalIndefinites.yalnhej_komon_flavor_difference : yalnhejEntry.hasEpistemic = true ∧ komonEntry.hasEpistemic = false

yalnhej and komon differ in flavor inventory: yalnhej has epistemic + RC, komon has RC only.