Basque Auxiliary Postsyntactic Inventory [AN12] [Mid26]

[HM93] [Har14a] [Har16a]

The fragment-level data needed to formalize the postsyntactic argument about Basque auxiliaries in [Mid26] §3.1 (extending [AN12] §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 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 Basque.Postsyntax.abs1pAuthor : Minimalist.FeatureBundle

A 1st-person absolutive clitic: [CL ABS +participant +author]. The trigger of [Mid26] (16) Participant Dissimilation.

Equations

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

def Basque.Postsyntax.erg2s : Minimalist.FeatureBundle

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

Equations

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

def Basque.Postsyntax.tPast : Minimalist.FeatureBundle

A T head with [+tense]. The leftmost-position trigger and swap-source of [Mid26] (13) Ergative Metathesis.

Equations

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

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

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

Equations

• Basque.Postsyntax.isT fb = (fb Minimalist.FeatureType.tense).isSpecified

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

Does the bundle bear an ergative case marker? Diagnoses an ERG clitic. (Matching is by dimension — any valued/unvalued case feature.)

Equations

• Basque.Postsyntax.isErgClitic fb = (fb Minimalist.FeatureType.case).isSpecified

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

Does the bundle bear an absolutive case marker? Diagnoses an ABS clitic. (Matching is by dimension — any valued/unvalued case feature.)

Equations

• Basque.Postsyntax.isAbsClitic fb = (fb Minimalist.FeatureType.case).isSpecified

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

Does the bundle bear [+participant]?

Equations

• Basque.Postsyntax.isParticipant fb = match fb Minimalist.FeatureType.participant with | Features.FeatureSlot.valued true => true | x => false

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

Does the bundle bear [+author]?

Equations

• Basque.Postsyntax.isAuthor fb = match fb Minimalist.FeatureType.author with | Features.FeatureSlot.valued true => true | x => false

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

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

Equations

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

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

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

Equations

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

theorem Basque.Postsyntax.abs1pAuthor_isAbsParticipantAuthor : isAbsParticipantAuthor abs1pAuthor = true

abs1pAuthor is recognised as an absolutive 1p clitic.

theorem Basque.Postsyntax.erg2s_isErgParticipant : isErgParticipant erg2s = true

erg2s is recognised as an ergative participant clitic.

theorem Basque.Postsyntax.tPast_isT : isT tPast = true

tPast is recognised as a T head.

theorem Basque.Postsyntax.tPast_not_isErgClitic : isErgClitic tPast = false

T is not an ergative clitic.

theorem Basque.Postsyntax.erg2s_not_isT : isT erg2s = false

ERG is not a T head.