Taos Verbal Agreement Fragment

@cite{kontak-kunkel-1987} @cite{watkins-1984} @cite{harrington-1916} @cite{harbour-2014} @cite{harbour-2016} @cite{middleton-2026}

Taos (Kiowa-Tanoan, Northern Tiwa) verbal agreement prefixes index up to three arguments — agent (A), goal (G), object (O) — linearized in that order @cite{watkins-1984}. The prefix decomposes into person and number morphemes whose exponence and ordering are described by @cite{middleton-2026} (building on @cite{harbour-2003}, @cite{harbour-2008}, @cite{harbour-2011}, @cite{harbour-2014}).

This fragment provides only the morpheme inventory and a representation of agreement prefixes as FeatureBundle lists. The postsyntactic rules of impoverishment and metathesis that derive the surface forms — and the theorems about ordering — live in Phenomena/Allomorphy/Studies/Middleton2026.lean.

Person and Number Features (Harbour)

Number features are [±atomic] and [±minimal] (@cite{harbour-2014}); person features are [±participant] and [±author] (@cite{harbour-2016}). Their denotations on Taos:

• singular s = [+atomic +minimal]
• dual d = [−atomic +minimal]
• plural p = [−atomic −minimal]
• 1 = [+participant +author]
• 2 = [+participant −author]
• 3 = [−participant −author]

(Following @cite{middleton-2026} fn. 4, [−atomic] is used in place of A&N's [−singular] for direct compatibility with @cite{harbour-2014}.)

inductive Fragments.Taos.Agreement.ArgRole : Type

Argument position in a Taos verbal prefix. The linearization is A G O (agent, goal, object) per @cite{watkins-1984}.

• agent : ArgRole
• goal : ArgRole
• object : ArgRole

@[implicit_reducible]

instance Fragments.Taos.Agreement.instDecidableEqArgRole : DecidableEq ArgRole

Equations

• Fragments.Taos.Agreement.instDecidableEqArgRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Taos.Agreement.instReprArgRole : Repr ArgRole

Equations

• Fragments.Taos.Agreement.instReprArgRole = { reprPrec := Fragments.Taos.Agreement.instReprArgRole.repr }

def Fragments.Taos.Agreement.instReprArgRole.repr : ArgRole → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Fragments.Taos.Agreement.fAtomic (b : Bool) : Minimalist.FeatureVal

A [±atomic] feature (@cite{harbour-2014}).

Equations

• Fragments.Taos.Agreement.fAtomic b = Minimalist.FeatureVal.atomic b

@[reducible, inline]

abbrev Fragments.Taos.Agreement.fMinimal (b : Bool) : Minimalist.FeatureVal

A [±minimal] feature (@cite{harbour-2014}).

Equations

• Fragments.Taos.Agreement.fMinimal b = Minimalist.FeatureVal.minimal b

@[reducible, inline]

abbrev Fragments.Taos.Agreement.fParticipant (b : Bool) : Minimalist.FeatureVal

A [±participant] feature (@cite{harbour-2016}).

Equations

• Fragments.Taos.Agreement.fParticipant b = Minimalist.FeatureVal.participant b

@[reducible, inline]

abbrev Fragments.Taos.Agreement.fAuthor (b : Bool) : Minimalist.FeatureVal

A [±author] feature (@cite{harbour-2016}).

Equations

• Fragments.Taos.Agreement.fAuthor b = Minimalist.FeatureVal.author b

def Fragments.Taos.Agreement.person1 : List Minimalist.FeatureVal

1st person bundle: [+participant +author].

Equations

• Fragments.Taos.Agreement.person1 = [Fragments.Taos.Agreement.fParticipant true, Fragments.Taos.Agreement.fAuthor true]

def Fragments.Taos.Agreement.person2 : List Minimalist.FeatureVal

2nd person bundle: [+participant −author].

Equations

• Fragments.Taos.Agreement.person2 = [Fragments.Taos.Agreement.fParticipant true, Fragments.Taos.Agreement.fAuthor false]

def Fragments.Taos.Agreement.person3 : List Minimalist.FeatureVal

3rd person bundle: [−participant −author].

Equations

• Fragments.Taos.Agreement.person3 = [Fragments.Taos.Agreement.fParticipant false, Fragments.Taos.Agreement.fAuthor false]

def Fragments.Taos.Agreement.numSg : List Minimalist.FeatureVal

Singular: [+atomic +minimal].

Equations

• Fragments.Taos.Agreement.numSg = [Fragments.Taos.Agreement.fAtomic true, Fragments.Taos.Agreement.fMinimal true]

def Fragments.Taos.Agreement.numDu : List Minimalist.FeatureVal

Dual: [−atomic +minimal].

Equations

• Fragments.Taos.Agreement.numDu = [Fragments.Taos.Agreement.fAtomic false, Fragments.Taos.Agreement.fMinimal true]

def Fragments.Taos.Agreement.numPl : List Minimalist.FeatureVal

Plural: [−atomic −minimal].

Equations

• Fragments.Taos.Agreement.numPl = [Fragments.Taos.Agreement.fAtomic false, Fragments.Taos.Agreement.fMinimal false]

def Fragments.Taos.Agreement.argBundle (person number : List Minimalist.FeatureVal) : Minimalist.FeatureBundle

An argument bundle = its person features then its number features, aligned per the Taos ordering convention [±part]:[±auth]:[±atom]:[±min] (@cite{middleton-2026} ex. 4 and 5).

Equations

• Fragments.Taos.Agreement.argBundle person number = List.map Minimalist.GramFeature.valued (person ++ number)

def Fragments.Taos.Agreement.prefix_1s3i_possessive_goal : Minimalist.FeatureBundle

The 1s:3i possessive prefix tó — the case in §4.2.5 where a paradigmatic rule must precede a syntagmatic one. Goal is 1s, object is 3i (3rd inverse). The agent slot is empty in possessive prefixes.

Equations

• Fragments.Taos.Agreement.prefix_1s3i_possessive_goal = Fragments.Taos.Agreement.argBundle Fragments.Taos.Agreement.person1 Fragments.Taos.Agreement.numSg

def Fragments.Taos.Agreement.prefix_1d3p_agent : Minimalist.FeatureBundle

The 1d:3p prefix opénôw — fully-articulated, no impoverishment.

Equations

• Fragments.Taos.Agreement.prefix_1d3p_agent = Fragments.Taos.Agreement.argBundle Fragments.Taos.Agreement.person1 Fragments.Taos.Agreement.numDu

def Fragments.Taos.Agreement.prefix_3s_agent : Minimalist.FeatureBundle

The 3s agent (transitive) bundle, the target of paradigmatic rule (35) 3s → ∅ / [[A _] (O)].

Equations

• Fragments.Taos.Agreement.prefix_3s_agent = Fragments.Taos.Agreement.argBundle Fragments.Taos.Agreement.person3 Fragments.Taos.Agreement.numSg

inductive Fragments.Taos.Agreement.Morpheme : Type

The Taos morphemes named in @cite{middleton-2026}. We carry them as strings; vocabulary insertion is not modeled in this fragment (it would require a full DM exponent-competition model). The relevant facts are exponence rules (20–22), (31), (33), (34), (38), (42).

• pé : Morpheme
• n : Morpheme
• o : Morpheme
• m : Morpheme
• k : Morpheme
• mo : Morpheme
• w : Morpheme
• i : Morpheme
• u : Morpheme
• ô : Morpheme

@[implicit_reducible]

instance Fragments.Taos.Agreement.instDecidableEqMorpheme : DecidableEq Morpheme

Equations

• Fragments.Taos.Agreement.instDecidableEqMorpheme x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Taos.Agreement.instReprMorpheme.repr : Morpheme → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Taos.Agreement.instReprMorpheme : Repr Morpheme

Equations

• Fragments.Taos.Agreement.instReprMorpheme = { reprPrec := Fragments.Taos.Agreement.instReprMorpheme.repr }

def Fragments.Taos.Agreement.Morpheme.surface : Morpheme → String

Render a morpheme as its surface form.

Equations

• Fragments.Taos.Agreement.Morpheme.pé.surface = "pé"
• Fragments.Taos.Agreement.Morpheme.n.surface = "n"
• Fragments.Taos.Agreement.Morpheme.o.surface = "o"
• Fragments.Taos.Agreement.Morpheme.m.surface = "m"
• Fragments.Taos.Agreement.Morpheme.k.surface = "k"
• Fragments.Taos.Agreement.Morpheme.mo.surface = "mo"
• Fragments.Taos.Agreement.Morpheme.w.surface = "w"
• Fragments.Taos.Agreement.Morpheme.i.surface = "i"
• Fragments.Taos.Agreement.Morpheme.u.surface = "u"
• Fragments.Taos.Agreement.Morpheme.ô.surface = "ô"