Auxiliary Verb Construction Typology — substrate

@cite{anderson-2006}

Type-level enums + data structure for auxiliary verb construction (AVC) typology following @cite{anderson-2006}. Anderson's core insight: the semantic head is always the lexical verb, but the inflectional host varies across 5 macro-patterns.

The Five Patterns

Pattern	Infl Host	Example Language
Aux-headed	AUX	English have eaten, is eating
Lex-headed	LEX	Pipil weli ni-nehnemi, Doyayo (Ch 3)
Doubled	AUX+LEX	Gorum miŋ ne-gaʔ-ru ne-laʔ-ru
Split	AUX or LEX	Jakaltek (abs/erg), Finnish (neg-aux ei)
Split/doubled	AUX+LEX	Pipil n-yu ni-mitsin-ilwitia, Doyayo (Ch 5), Hemba

Schema

• InflPattern: the 5-way macro-classification of inflectional distribution
• AVCElement: which element(s) of an AVC bear a given property
• AVCDatum: a per-language AVC datum (form, pattern, distribution, gloss)

What lives here vs. Phenomena/AuxiliaryVerbs/Studies/Anderson2006.lean

This file holds the substrate types and Fragment-independent invariants (semantic_head_always_lex, auxHeaded_infl_on_phrasal_head, etc.). Per-language AVCDatum instances + Fragment-grounding verification theorems live in the Anderson 2006 study file (paper-anchored data).

Core types

inductive Typology.AuxiliaryVerbs.InflPattern : Type

Anderson's 5-way inflectional pattern typology for AVCs.

• auxHeaded : InflPattern

  Inflection hosted on auxiliary; lexical verb is nonfinite. E.g., English will go, French va manger.

• lexHeaded : InflPattern

  Inflection hosted on lexical verb; auxiliary is grammaticalized. E.g., Pipil weli ni-nehnemi (AUX uninflected, LV carries person); Doyayo mi¹ (gi²) kpel¹-ko¹ (Ch 3 ex 15a).

• doubled : InflPattern

  Inflection appears on both auxiliary and lexical verb. E.g., Gorum miŋ ne-gaʔ-ru ne-laʔ-ru (subject + TAM on both).

• split : InflPattern

  Inflection split between AUX and LV (different features on each element, with no overlap). E.g., Jakaltek šk-ach w-ila (absolutive on AUX, ergative on LV); Finnish neg-aux ei (person/number on AUX, connegative + aspect on LV).

• splitDoubled : InflPattern

  Some categories on both AUX and LV (doubled), others exclusive to one element (split). @cite{anderson-2006} ch. 5 §5.2 dedicates ~30 pages to this pattern with 30+ language exemplars across §§5.2.1–5.2.3 (Limbu, Manam, Kuot, Doyayo, Mbay, Lamba, Pipil, Persian, Swahili, Panyjima, Kemantney, Oshikwanyama, Shambala, Vinmavis, Nambiquara, Baure, Luganda, Nasioi, Os, Xhosa, ...). Common, not marginal.

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instDecidableEqInflPattern : DecidableEq InflPattern

Equations

• Typology.AuxiliaryVerbs.instDecidableEqInflPattern x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instReprInflPattern : Repr InflPattern

Equations

• Typology.AuxiliaryVerbs.instReprInflPattern = { reprPrec := Typology.AuxiliaryVerbs.instReprInflPattern.repr }

def Typology.AuxiliaryVerbs.instReprInflPattern.repr : InflPattern → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instInhabitedInflPattern : Inhabited InflPattern

Equations

• Typology.AuxiliaryVerbs.instInhabitedInflPattern = { default := Typology.AuxiliaryVerbs.instInhabitedInflPattern.default }

def Typology.AuxiliaryVerbs.instInhabitedInflPattern.default : InflPattern

Equations

• Typology.AuxiliaryVerbs.instInhabitedInflPattern.default = Typology.AuxiliaryVerbs.InflPattern.auxHeaded

inductive Typology.AuxiliaryVerbs.AVCElement : Type

Which element(s) of an AVC bear a given property.

• aux : AVCElement
• lex : AVCElement
• both : AVCElement

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instDecidableEqAVCElement : DecidableEq AVCElement

Equations

• Typology.AuxiliaryVerbs.instDecidableEqAVCElement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Typology.AuxiliaryVerbs.instReprAVCElement.repr : AVCElement → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instReprAVCElement : Repr AVCElement

Equations

• Typology.AuxiliaryVerbs.instReprAVCElement = { reprPrec := Typology.AuxiliaryVerbs.instReprAVCElement.repr }

Key functions

def Typology.AuxiliaryVerbs.InflPattern.semanticHead : InflPattern → AVCElement

The semantic head is always the lexical verb (Anderson's invariant).

Equations

• x✝.semanticHead = Typology.AuxiliaryVerbs.AVCElement.lex

def Typology.AuxiliaryVerbs.InflPattern.inflHost : InflPattern → AVCElement

Which element hosts inflection in each pattern.

Equations

• Typology.AuxiliaryVerbs.InflPattern.auxHeaded.inflHost = Typology.AuxiliaryVerbs.AVCElement.aux
• Typology.AuxiliaryVerbs.InflPattern.lexHeaded.inflHost = Typology.AuxiliaryVerbs.AVCElement.lex
• Typology.AuxiliaryVerbs.InflPattern.doubled.inflHost = Typology.AuxiliaryVerbs.AVCElement.both
• Typology.AuxiliaryVerbs.InflPattern.split.inflHost = Typology.AuxiliaryVerbs.AVCElement.both
• Typology.AuxiliaryVerbs.InflPattern.splitDoubled.inflHost = Typology.AuxiliaryVerbs.AVCElement.both

def Typology.AuxiliaryVerbs.InflPattern.inflOnlyOnPhrasalHead : InflPattern → Bool

Whether inflection is hosted exclusively on the phrasal head (= AUX). Only aux-headed AVCs have this property: the AUX hosts all inflection and the LV is fully nonfinite. In doubled AVCs, both elements carry inflection, so the phrasal head is not the sole inflectional host.

Equations

• Typology.AuxiliaryVerbs.InflPattern.auxHeaded.inflOnlyOnPhrasalHead = true
• Typology.AuxiliaryVerbs.InflPattern.lexHeaded.inflOnlyOnPhrasalHead = false
• Typology.AuxiliaryVerbs.InflPattern.doubled.inflOnlyOnPhrasalHead = false
• Typology.AuxiliaryVerbs.InflPattern.split.inflOnlyOnPhrasalHead = false
• Typology.AuxiliaryVerbs.InflPattern.splitDoubled.inflOnlyOnPhrasalHead = false

def Typology.AuxiliaryVerbs.InflPattern.lvVerbForm : InflPattern → UD.VerbForm

Expected verb form of the lexical verb in each AVC pattern. Aux-headed: LV is nonfinite (infinitive/participle). Lex-headed: LV is finite (carries TAM). Doubled/split/splitDoubled: LV is finite (carries at least some inflection).

Equations

• Typology.AuxiliaryVerbs.InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf
• Typology.AuxiliaryVerbs.InflPattern.lexHeaded.lvVerbForm = UD.VerbForm.Fin
• Typology.AuxiliaryVerbs.InflPattern.doubled.lvVerbForm = UD.VerbForm.Fin
• Typology.AuxiliaryVerbs.InflPattern.split.lvVerbForm = UD.VerbForm.Fin
• Typology.AuxiliaryVerbs.InflPattern.splitDoubled.lvVerbForm = UD.VerbForm.Fin

AVC datum schema

structure Typology.AuxiliaryVerbs.AVCDatum : Type

A cross-linguistic AVC datum.

• language : String
• form : String
• inflPattern : InflPattern
• distribution : Option Core.Morphology.InflDistribution
• gloss : String

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instReprAVCDatum : Repr AVCDatum

Equations

• Typology.AuxiliaryVerbs.instReprAVCDatum = { reprPrec := Typology.AuxiliaryVerbs.instReprAVCDatum.repr }

def Typology.AuxiliaryVerbs.instReprAVCDatum.repr : AVCDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Typology.AuxiliaryVerbs.instBEqAVCDatum : BEq AVCDatum

Equations

• Typology.AuxiliaryVerbs.instBEqAVCDatum = { beq := Typology.AuxiliaryVerbs.instBEqAVCDatum.beq }

def Typology.AuxiliaryVerbs.instBEqAVCDatum.beq : AVCDatum → AVCDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Typology.AuxiliaryVerbs.instBEqAVCDatum.beq x✝¹ x✝ = false

Invariant theorems

These theorems are about InflPattern itself — Fragment-independent substrate-level facts. Per-language verification theorems live in the Anderson 2006 study file.

theorem Typology.AuxiliaryVerbs.semantic_head_always_lex (p : InflPattern) : p.semanticHead = AVCElement.lex

Anderson's key insight: the semantic head is always the lexical verb, regardless of inflectional pattern.

theorem Typology.AuxiliaryVerbs.auxHeaded_infl_on_phrasal_head : InflPattern.auxHeaded.inflOnlyOnPhrasalHead = true

In aux-headed AVCs, inflection is exclusively on the phrasal head (AUX).

theorem Typology.AuxiliaryVerbs.lexHeaded_infl_not_on_phrasal_head : InflPattern.lexHeaded.inflOnlyOnPhrasalHead = false

In lex-headed AVCs, inflection is not on the phrasal head.

theorem Typology.AuxiliaryVerbs.doubled_infl_not_only_on_phrasal_head : InflPattern.doubled.inflOnlyOnPhrasalHead = false

In doubled AVCs, inflection appears on both elements, so the phrasal head is not the sole host.

theorem Typology.AuxiliaryVerbs.auxHeaded_lv_nonfinite : InflPattern.auxHeaded.lvVerbForm = UD.VerbForm.Inf

In aux-headed AVCs, the lexical verb is nonfinite.

theorem Typology.AuxiliaryVerbs.lexHeaded_lv_finite : InflPattern.lexHeaded.lvVerbForm = UD.VerbForm.Fin

In lex-headed AVCs, the lexical verb is finite.