Basque Auxiliary Postsyntactic Inventory @cite{arregi-nevins-2012} @cite{middleton-2026}

@cite{halle-marantz-1993} @cite{harbour-2014} @cite{harbour-2016}

The fragment-level data needed to formalize the postsyntactic argument about Basque auxiliaries in @cite{middleton-2026} §3.1 (extending @cite{arregi-nevins-2012} §3.1.1, §4.6).

A finite Basque auxiliary linearizes as a sequence of terminal nodes (each a FeatureBundle): an absolutive clitic, a T head, an ergative clitic, and a complementizer. The two postsyntactic rules that diagnose the impoverishment-before-metathesis ordering operate on whole terminals, not on features within a single bundle:

• Rule (16) Participant Dissimilation — deletes a 1p ([+participant +author]) absolutive clitic when followed by a participant ergative clitic.
• Rule (13) Ergative Metathesis — swaps the T head with an immediately-following ergative clitic when T is leftmost in the auxiliary.

This file provides only the bundle constructors and predicates the rules need to fire. The rules themselves and the divergence proof live in Phenomena/Allomorphy/Studies/Middleton2026.lean.

Encoding choices

• Clitics carry a [CL] marker via the .case .erg/.case .abs constructor (already in Minimalist.FeatureVal); together with the [+participant]/[+author] Harbour features this is enough to distinguish the four configurations the rules care about.
• T is marked with [+tense], present in Minimalist.FeatureVal.
• The complementizer is dropped from the witness phrase: it is not referenced by either rule, and including it would add noise.

def Fragments.Basque.Postsyntax.abs1pAuthor : Minimalist.FeatureBundle

A 1st-person absolutive clitic: [CL ABS +participant +author]. The trigger of @cite{middleton-2026} (16) Participant Dissimilation.

Equations

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

def Fragments.Basque.Postsyntax.erg2s : Minimalist.FeatureBundle

A 2nd-person ergative clitic: [CL ERG +participant −author]. The right-context of @cite{middleton-2026} (16) — the participant ergative that licenses deletion of abs1pAuthor.

Equations

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

def Fragments.Basque.Postsyntax.tPast : Minimalist.FeatureBundle

A T head with [+tense]. The leftmost-position trigger and swap-source of @cite{middleton-2026} (13) Ergative Metathesis.

Equations

• Fragments.Basque.Postsyntax.tPast = [Minimalist.GramFeature.valued (Minimalist.FeatureVal.tense true)]

def Fragments.Basque.Postsyntax.isT (fb : Minimalist.FeatureBundle) : Bool

Does the bundle bear [+tense]? Diagnoses a T head.

Equations

• Fragments.Basque.Postsyntax.isT fb = List.any fb fun (f : Minimalist.GramFeature) => f.featureType.sameType (Minimalist.FeatureVal.tense true)

def Fragments.Basque.Postsyntax.isErgClitic (fb : Minimalist.FeatureBundle) : Bool

Does the bundle bear an ergative case marker? Diagnoses an ERG clitic.

Equations

• Fragments.Basque.Postsyntax.isErgClitic fb = List.any fb fun (f : Minimalist.GramFeature) => f.featureType.sameType (Minimalist.FeatureVal.case UD.Case.erg)

def Fragments.Basque.Postsyntax.isAbsClitic (fb : Minimalist.FeatureBundle) : Bool

Does the bundle bear an absolutive case marker? Diagnoses an ABS clitic.

Equations

• Fragments.Basque.Postsyntax.isAbsClitic fb = List.any fb fun (f : Minimalist.GramFeature) => f.featureType.sameType (Minimalist.FeatureVal.case UD.Case.abs)

def Fragments.Basque.Postsyntax.isParticipant (fb : Minimalist.FeatureBundle) : Bool

Does the bundle bear [+participant]?

Equations

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

def Fragments.Basque.Postsyntax.isAuthor (fb : Minimalist.FeatureBundle) : Bool

Does the bundle bear [+author]?

Equations

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

def Fragments.Basque.Postsyntax.isAbsParticipantAuthor (fb : Minimalist.FeatureBundle) : Bool

A 1st-person absolutive clitic — [CL ABS +participant +author], the deletion target of Participant Dissimilation.

Equations

• Fragments.Basque.Postsyntax.isAbsParticipantAuthor fb = (Fragments.Basque.Postsyntax.isAbsClitic fb && Fragments.Basque.Postsyntax.isParticipant fb && Fragments.Basque.Postsyntax.isAuthor fb)

def Fragments.Basque.Postsyntax.isErgParticipant (fb : Minimalist.FeatureBundle) : Bool

A participant ergative clitic — [CL ERG +participant ...], the right-context that licenses Participant Dissimilation.

Equations

• Fragments.Basque.Postsyntax.isErgParticipant fb = (Fragments.Basque.Postsyntax.isErgClitic fb && Fragments.Basque.Postsyntax.isParticipant fb)

theorem Fragments.Basque.Postsyntax.abs1pAuthor_isAbsParticipantAuthor : isAbsParticipantAuthor abs1pAuthor = true

abs1pAuthor is recognised as an absolutive 1p clitic.

theorem Fragments.Basque.Postsyntax.erg2s_isErgParticipant : isErgParticipant erg2s = true

erg2s is recognised as an ergative participant clitic.

theorem Fragments.Basque.Postsyntax.tPast_isT : isT tPast = true

tPast is recognised as a T head.

theorem Fragments.Basque.Postsyntax.tPast_not_isErgClitic : isErgClitic tPast = false

T is not an ergative clitic.

theorem Fragments.Basque.Postsyntax.erg2s_not_isT : isT erg2s = false

ERG is not a T head.