Lexical Salience Classes

@cite{lucy-1994}

A 4-way classification of verbal roots by which argument(s) the underived root form makes "salient" (in @cite{lucy-1994}'s sense: default case-role assignment at the propositional level). The four classes — agent, agent-patient, patient, positional — are derivable from the B&K-G feature signature alone.

This file lifts the classification out of any specific empirical study so that other Fragment / Theory modules can refer to it (e.g., the Yukatek 5-way verb stem classification, which refines this 4-way cut). The full @cite{lucy-1994} analysis — operator orbits, motion-roots-non-class theorem, per-root verifications — lives in Phenomena/ArgumentStructure/Studies/Lucy1994.lean.

inductive Semantics.Lexical.Roots.SalienceClass : Type

The 4-way salience classification of verbal roots (@cite{lucy-1994}). "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 Semantics.Lexical.Roots.instDecidableEqSalienceClass : DecidableEq SalienceClass

Equations

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

def Semantics.Lexical.Roots.instReprSalienceClass.repr : SalienceClass → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.Roots.instReprSalienceClass : Repr SalienceClass

Equations

• Semantics.Lexical.Roots.instReprSalienceClass = { reprPrec := Semantics.Lexical.Roots.instReprSalienceClass.repr }

Named structural conditions characterising membership in each @cite{lucy-1994} salience class. These predicates 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 Semantics.Lexical.Roots.FeatureSignature.IsAgentSalient (s : FeatureSignature) : Prop

Agent-salient: manner without result (intransitive activity that requires =t to transitivise; @cite{lucy-1994}).

Equations

• s.IsAgentSalient = (s.manner = true ∧ s.result = false)

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsAgentSalient (s : FeatureSignature) : Decidable s.IsAgentSalient

Equations

• Semantics.Lexical.Roots.instDecidableIsAgentSalient s = id inferInstance

def Semantics.Lexical.Roots.FeatureSignature.IsAgentPatientSalient (s : FeatureSignature) : Prop

Agent-patient salient: manner and result (already lexically transitive; @cite{lucy-1994}).

Equations

• s.IsAgentPatientSalient = (s.manner = true ∧ s.result = true)

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsAgentPatientSalient (s : FeatureSignature) : Decidable s.IsAgentPatientSalient

Equations

• Semantics.Lexical.Roots.instDecidableIsAgentPatientSalient s = id inferInstance

def Semantics.Lexical.Roots.FeatureSignature.IsPatientSalient (s : FeatureSignature) : Prop

Patient-salient: result without manner (intransitive change-of-state that requires =s to transitivise; @cite{lucy-1994}).

Equations

• s.IsPatientSalient = (s.manner = false ∧ s.result = true)

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsPatientSalient (s : FeatureSignature) : Decidable s.IsPatientSalient

Equations

• Semantics.Lexical.Roots.instDecidableIsPatientSalient s = id inferInstance

def Semantics.Lexical.Roots.FeatureSignature.IsPositional (s : FeatureSignature) : Prop

Positional: pure stative root — state without manner, result, or cause (requires -tal for the inchoative; @cite{lucy-1994}).

Equations

• s.IsPositional = (s.state = true ∧ s.manner = false ∧ s.result = false ∧ s.cause = false)

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsPositional (s : FeatureSignature) : Decidable s.IsPositional

Equations

• Semantics.Lexical.Roots.instDecidableIsPositional s = id inferInstance

Per-root convenience versions, lifted via featureSignature.

def Semantics.Lexical.Roots.Root.IsAgentSalient (r : Root) : Prop

Agent-salient root (lifted to roots; cf. FeatureSignature.IsAgentSalient).

Equations

• r.IsAgentSalient = r.featureSignature.IsAgentSalient

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsAgentSalient_1 (r : Root) : Decidable r.IsAgentSalient

Equations

• Semantics.Lexical.Roots.instDecidableIsAgentSalient_1 r = id inferInstance

def Semantics.Lexical.Roots.Root.IsAgentPatientSalient (r : Root) : Prop

Agent-patient salient root.

Equations

• r.IsAgentPatientSalient = r.featureSignature.IsAgentPatientSalient

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsAgentPatientSalient_1 (r : Root) : Decidable r.IsAgentPatientSalient

Equations

• Semantics.Lexical.Roots.instDecidableIsAgentPatientSalient_1 r = id inferInstance

def Semantics.Lexical.Roots.Root.IsPatientSalient (r : Root) : Prop

Patient-salient root.

Equations

• r.IsPatientSalient = r.featureSignature.IsPatientSalient

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsPatientSalient_1 (r : Root) : Decidable r.IsPatientSalient

Equations

• Semantics.Lexical.Roots.instDecidableIsPatientSalient_1 r = id inferInstance

def Semantics.Lexical.Roots.Root.IsPositional (r : Root) : Prop

Positional root.

Equations

• r.IsPositional = r.featureSignature.IsPositional

@[implicit_reducible]

instance Semantics.Lexical.Roots.instDecidableIsPositional_1 (r : Root) : Decidable r.IsPositional

Equations

• Semantics.Lexical.Roots.instDecidableIsPositional_1 r = id inferInstance

def Semantics.Lexical.Roots.classOfSignature (s : FeatureSignature) : Option SalienceClass

Map a B&K-G feature signature to its salience class (@cite{lucy-1994}). The arms align with operator applicability conditions in Fragments/Mayan/Yukatek/Operators.lean:

(state, manner, result, cause)	predicted class
(_, true, false, _)	agent
(_, true, true, _)	agentPatient
(_, false, true, _)	patient
(true, false, false, false)	positional
otherwise	none

The positional row requires cause = false: positional roots are pure stative configurations (orientation, posture, location) with no causing event. The four arms equivalently dispatch on the four named predicates IsAgentSalient, IsAgentPatientSalient, IsPatientSalient, IsPositional — see classOfSignature_eq_dispatch.

Equations

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

def Semantics.Lexical.Roots.Root.predictedSalience (r : Root) : Option SalienceClass

A root's predicted salience class is classOfSignature of its feature signature.

Equations

• r.predictedSalience = Semantics.Lexical.Roots.classOfSignature r.featureSignature

theorem Semantics.Lexical.Roots.predictedSalience_depends_only_on_signature (r₁ r₂ : Root) (h : r₁.featureSignature = r₂.featureSignature) : r₁.predictedSalience = r₂.predictedSalience

Two roots with the same B&K-G feature signature get the same salience class.

theorem Semantics.Lexical.Roots.classOfSignature_eq_dispatch (s : FeatureSignature) : classOfSignature s = if s.IsAgentSalient then some SalienceClass.agent else if s.IsAgentPatientSalient then some SalienceClass.agentPatient else if s.IsPatientSalient then some SalienceClass.patient else if s.IsPositional then some SalienceClass.positional else none

The classOfSignature table is equivalent to dispatching on the four named predicates. Establishes that the classifier really is the disjunction of the named conditions — not an arbitrary table.

theorem Semantics.Lexical.Roots.classes_pairwise_disjoint (s : FeatureSignature) : ¬(s.IsAgentSalient ∧ s.IsAgentPatientSalient) ∧ ¬(s.IsAgentSalient ∧ s.IsPatientSalient) ∧ ¬(s.IsAgentSalient ∧ s.IsPositional) ∧ ¬(s.IsAgentPatientSalient ∧ s.IsPatientSalient) ∧ ¬(s.IsAgentPatientSalient ∧ s.IsPositional) ∧ ¬(s.IsPatientSalient ∧ s.IsPositional)

The four named predicates are pairwise disjoint: at most one fires on any given signature. (They are jointly not exhaustive — the ⟨false, false, _, _⟩ rows that the positional arm doesn't catch fall outside all four; see classOfSignature_eq_none_iff.)

theorem Semantics.Lexical.Roots.classOfSignature_eq_none_iff (s : FeatureSignature) : classOfSignature s = none ↔ ¬s.IsAgentSalient ∧ ¬s.IsAgentPatientSalient ∧ ¬s.IsPatientSalient ∧ ¬s.IsPositional

classOfSignature s = none iff s falls outside all four named predicates. Characterises the gap in the diagnostic: the (¬manner, ¬result) rows that lack the positional configuration (state ∧ ¬cause) are unclassified by Lucy's Yukatek diagnostic.