Lexical Salience Classes

[Luc94]'s classification of verbal roots by which argument(s) the underived root form makes "salient" (default case-role assignment at the propositional level): a 3-way salience cut by required transitiviser — agent (=t), agent-patient (=∅), patient (=s) — plus the separately-derived positional class (-tal), systematized here as one enum.

The structural characterization of each class needs two dimensions. Agent-patient salience is root transitivity: these roots "require two arguments and refer to events involving the action of one entity on another" ([Luc94]) — Root.Arity.selectsTheme, the Mayan root-transitive class of [Coo19]. It is NOT a B&K-G feature configuration: p'is 'measure' and lo'š 'punch' are manner roots with no entailed change of state. The two intransitive classes are then separated by the signature (manner vs result), matching the Sapir/Perlmutter unaccusativity split [Luc94] cites. This two-dimensional characterization is a cross-framework reconstruction ([Luc94] predates both [Coo19] and [BKG20]), not Lucy's own formulation.

The full [Luc94] analysis — operator applicability, motion-roots-non-class theorem, per-root verifications — lives in Studies/Lucy1994.lean.

Main declarations

• SalienceClass
• IsAgentSalient, IsAgentPatientSalient, IsPatientSalient, IsPositional — conditions over (signature × arity)
• classOf — the salience classifier

inductive Verb.SalienceClass : Type

Salience classification of verbal roots ([Luc94]): the 3-way transitiviser cut plus the positional class. "Salience" is shorthand for "default case-role assignment at the propositional level" — not a substantive feature [±agent] written into the root.

• agent : SalienceClass

  Underived intransitive whose argument is the agent.

• agentPatient : SalienceClass

  Underived transitive — both arguments lexically salient.

• patient : SalienceClass

  Underived intransitive whose argument is the patient.

• positional : SalienceClass

  Stative root (positional / configurational).

@[implicit_reducible]

instance Verb.instDecidableEqSalienceClass : DecidableEq SalienceClass

Equations

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

@[implicit_reducible]

instance Verb.instReprSalienceClass : Repr SalienceClass

Equations

• Verb.instReprSalienceClass = { reprPrec := Verb.instReprSalienceClass.repr }

def Verb.instReprSalienceClass.repr : SalienceClass → ℕ → Std.Format

Equations

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

Named class conditions

Structural conditions characterising membership in each [Luc94] salience class, over the pair (B&K-G kind signature × Coon arity). These conditions are language-independent: the same conditions characterise the class in any inventory whose transitivisers respect the diagnostic. They appear directly as the applies field of each Yukatek operator in Fragments/Mayan/Yukatek/Operators.lean, making the operator-applicability ↔ salience-class connection true by construction rather than only provable per-case.

def Verb.IsAgentSalient (s : Root.Kinds) (ar : Root.Arity) : Prop

Agent-salient: intransitive manner-of-action root (requires =t to transitivise; [Luc94]: "actions or activities that some entity undertakes").

Equations

• Verb.IsAgentSalient s ar = (ar = Verb.Root.Arity.noTheme ∧ Verb.LexKind.manner ∈ s ∧ Verb.LexKind.result ∉ s)

@[implicit_reducible]

instance Verb.instDecidableIsAgentSalient (s : Root.Kinds) (ar : Root.Arity) : Decidable (IsAgentSalient s ar)

Equations

• Verb.instDecidableIsAgentSalient s ar = Verb.instDecidableIsAgentSalient._aux_1 s ar

def Verb.IsAgentPatientSalient (ar : Root.Arity) : Prop

Agent-patient salient: the root is lexically transitive — it "require[s] two arguments" ([Luc94]), i.e. selects a theme ([Coo19]'s √TV). Signature-independent: root transitives need not entail any change of state (p'is 'measure').

Equations

• Verb.IsAgentPatientSalient ar = (ar = Verb.Root.Arity.selectsTheme)

@[implicit_reducible]

instance Verb.instDecidableIsAgentPatientSalient (ar : Root.Arity) : Decidable (IsAgentPatientSalient ar)

Equations

• Verb.instDecidableIsAgentPatientSalient ar = Verb.instDecidableIsAgentPatientSalient._aux_1 ar

def Verb.IsPatientSalient (s : Root.Kinds) (ar : Root.Arity) : Prop

Patient-salient: intransitive change-of-state root (requires =s to transitivise; [Luc94]: "state changes that some entity undergoes more or less spontaneously").

Equations

• Verb.IsPatientSalient s ar = (ar = Verb.Root.Arity.noTheme ∧ Verb.LexKind.manner ∉ s ∧ Verb.LexKind.result ∈ s)

@[implicit_reducible]

instance Verb.instDecidableIsPatientSalient (s : Root.Kinds) (ar : Root.Arity) : Decidable (IsPatientSalient s ar)

Equations

• Verb.instDecidableIsPatientSalient s ar = Verb.instDecidableIsPatientSalient._aux_1 s ar

def Verb.IsPositional (s : Root.Kinds) (ar : Root.Arity) : Prop

Positional: pure stative configurational root (requires -tal for the inchoative; [Luc94]).

Equations

• Verb.IsPositional s ar = (ar = Verb.Root.Arity.noTheme ∧ s = {Verb.LexKind.state})

@[implicit_reducible]

instance Verb.instDecidableIsPositional (s : Root.Kinds) (ar : Root.Arity) : Decidable (IsPositional s ar)

Equations

• Verb.instDecidableIsPositional s ar = Verb.instDecidableIsPositional._aux_1 s ar

Salience classifier

def Verb.classOf (s : Root.Kinds) (ar : Root.Arity) : Option SalienceClass

Map a (B&K-G kind signature × Coon arity) pair to its salience class ([Luc94]) by dispatching on the four named conditions, which align with operator applicability conditions in Fragments/Mayan/Yukatek/Operators.lean.

Equations

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

Pairwise disjointness of class conditions

theorem Verb.classes_pairwise_disjoint (s : Root.Kinds) (ar : Root.Arity) : ¬(IsAgentSalient s ar ∧ IsAgentPatientSalient ar) ∧ ¬(IsAgentSalient s ar ∧ IsPatientSalient s ar) ∧ ¬(IsAgentSalient s ar ∧ IsPositional s ar) ∧ ¬(IsAgentPatientSalient ar ∧ IsPatientSalient s ar) ∧ ¬(IsAgentPatientSalient ar ∧ IsPositional s ar) ∧ ¬(IsPatientSalient s ar ∧ IsPositional s ar)

The four named conditions are pairwise disjoint: at most one fires on any (signature, arity) pair. (They are jointly not exhaustive — intransitive signatures with neither manner nor result that are not pure {state} fall outside all four; see classOf_eq_none_iff.)

theorem Verb.classOf_eq_none_iff (s : Root.Kinds) (ar : Root.Arity) : classOf s ar = none ↔ ¬IsAgentSalient s ar ∧ ¬IsAgentPatientSalient ar ∧ ¬IsPatientSalient s ar ∧ ¬IsPositional s ar

classOf s ar = none iff the pair falls outside all four named conditions. Characterises the gap in the diagnostic: intransitive roots with neither a manner nor a result kind, other than pure {state}, are unclassified by Lucy's Yukatek diagnostic.