Hausa TAM and the Person-Aspect-Complex (PAC) — mathlib-style

@cite{newman-2000} @cite{jaggar-2001}

Hausa inflection is concentrated in a portmanteau preverbal element called the PAC (person-aspect-complex), which fuses:

• the subject's person, number and (in 2sg/3sg) gender, and
• the TAM of the clause (completive, continuous, future, subjunctive, habitual, …).

(@cite{newman-2000} ch. 70.) Because the PAC is the only inflectional locus, the verb stem itself is unmarked for tense or person agreement — all of that information lives in the PAC.

The General / Relative split

A second axis cross-cuts the TAM dimension: a General (matrix declarative) vs Relative form. The Relative forms surface in three syntactic environments (@cite{newman-2000} ch. 64–65):

1. relative clauses headed by dà;
2. wh-questions (in-situ or ex-situ); and
3. ex-situ focus constructions licensed by the stabilizer nē/cē.

The Relative form is morphologically distinct in only the completive and continuous TAMs (others are syncretic with the General form). This yields a four-way diagnostic that we encode here as a TAM × Mode pair. The Focus fragment (Hausa/Focus.lean) consumes this split as the licensing condition on ex-situ focus.

PAC.WellFormed is a propositional predicate (Prop with a Decidable instance). It is not enforced as a Subtype invariant — ill-formed PACs are constructible by direct field assignment. The mkGeneralPAC and mkRelativePAC constructors are ergonomic helpers: the relative one takes a proof obligation tam.HasRelativeForm so that PACs built via it are well-formed by construction, but a downstream file is free to construct a deliberately ill-formed PAC and prove it ill-formed (see Focus.lean's exSitu_with_genCmp, which is exactly that pattern).

inductive Fragments.Hausa.Inflection.TAM : Type

The seven core TAM categories of the PAC. We follow Newman's labels; the modally-ambiguous "potential" TAM is included for completeness but rarely controls the General/Relative split.

• completive : TAM
• continuous : TAM
• future : TAM
• subjunctive : TAM
• habitual : TAM
• rhetorical : TAM
• potential : TAM

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instDecidableEqTAM : DecidableEq TAM

Equations

• Fragments.Hausa.Inflection.instDecidableEqTAM x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Fragments.Hausa.Inflection.instReprTAM.repr : TAM → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instReprTAM : Repr TAM

Equations

• Fragments.Hausa.Inflection.instReprTAM = { reprPrec := Fragments.Hausa.Inflection.instReprTAM.repr }

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instInhabitedTAM : Inhabited TAM

Equations

• Fragments.Hausa.Inflection.instInhabitedTAM = { default := Fragments.Hausa.Inflection.instInhabitedTAM.default }

def Fragments.Hausa.Inflection.instInhabitedTAM.default : TAM

Equations

• Fragments.Hausa.Inflection.instInhabitedTAM.default = Fragments.Hausa.Inflection.TAM.completive

def Fragments.Hausa.Inflection.TAM.all : List TAM

The seven TAMs in canonical order.

Equations

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

def Fragments.Hausa.Inflection.TAM.HasRelativeForm : TAM → Prop

The General/Relative split surfaces morphologically only for the completive and continuous TAMs (@cite{newman-2000} §64.2, Table 32). HasRelativeForm is the propositional predicate; downstream constructors take it as a proof obligation.

Equations

• Fragments.Hausa.Inflection.TAM.completive.HasRelativeForm = True
• Fragments.Hausa.Inflection.TAM.continuous.HasRelativeForm = True
• x✝.HasRelativeForm = False

@[implicit_reducible]

instance Fragments.Hausa.Inflection.TAM.instDecidableHasRelativeForm (t : TAM) : Decidable t.HasRelativeForm

Equations

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

inductive Fragments.Hausa.Inflection.Mode : Type

General vs Relative form. Most TAMs are syncretic between the two; completive and continuous are the empirically diagnostic cases.

• general : Mode
• relative : Mode

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instDecidableEqMode : DecidableEq Mode

Equations

• Fragments.Hausa.Inflection.instDecidableEqMode x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instReprMode : Repr Mode

Equations

• Fragments.Hausa.Inflection.instReprMode = { reprPrec := Fragments.Hausa.Inflection.instReprMode.repr }

def Fragments.Hausa.Inflection.instReprMode.repr : Mode → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instInhabitedMode : Inhabited Mode

Equations

• Fragments.Hausa.Inflection.instInhabitedMode = { default := Fragments.Hausa.Inflection.instInhabitedMode.default }

def Fragments.Hausa.Inflection.instInhabitedMode.default : Mode

Equations

• Fragments.Hausa.Inflection.instInhabitedMode.default = Fragments.Hausa.Inflection.Mode.general

structure Fragments.Hausa.Inflection.Subject : Type

The subject slot of the PAC. Hausa makes a 2sg / 3sg gender distinction (M vs F), absent in the plural and 1st person. We use Features.Person.Category for the singular/group cut and add a gender field that is empty (none) outside the 2sg/3sg cells.

• person : Features.Person.Category
• gender : Option Features.SurfaceGender

def Fragments.Hausa.Inflection.instDecidableEqSubject.decEq (x✝ x✝¹ : Subject) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instDecidableEqSubject : DecidableEq Subject

Equations

• Fragments.Hausa.Inflection.instDecidableEqSubject = Fragments.Hausa.Inflection.instDecidableEqSubject.decEq

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instReprSubject : Repr Subject

Equations

• Fragments.Hausa.Inflection.instReprSubject = { reprPrec := Fragments.Hausa.Inflection.instReprSubject.repr }

def Fragments.Hausa.Inflection.instReprSubject.repr : Subject → ℕ → Std.Format

Equations

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

def Fragments.Hausa.Inflection.Subject.HasGenderContrast (s : Subject) : Prop

A subject has a gender contrast iff its gender field is non-empty. Propositional predicate (with Decidable), not Bool.

Equations

• s.HasGenderContrast = (s.gender ≠ none)

@[implicit_reducible]

instance Fragments.Hausa.Inflection.Subject.instDecidableHasGenderContrast (s : Subject) : Decidable s.HasGenderContrast

Equations

• s.instDecidableHasGenderContrast = Fragments.Hausa.Inflection.Subject.instDecidableHasGenderContrast._aux_1 s

def Fragments.Hausa.Inflection.hausaSubjects : List Subject

The subject inventory of Hausa. We restrict to the cells that actually appear in the PAC paradigm (Person.Category includes inclusive/exclusive distinctions that Hausa lacks).

Equations

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

theorem Fragments.Hausa.Inflection.gender_contrast_only_in_singular (s : Subject) : s ∈ hausaSubjects → s.HasGenderContrast → s.person = Features.Person.Category.s2 ∨ s.person = Features.Person.Category.s3

Gender contrast is restricted to the singular. A Hausa subject has a gender contrast only in 2sg or 3sg cells.

structure Fragments.Hausa.Inflection.PAC : Type

A PAC: subject × TAM × mode → surface form. The WellFormed invariant (relative mode requires a TAM that admits the relative form) is enforced at construction time by mkRelativePAC; PACs built via mkGeneralPAC are well-formed unconditionally. The full paradigm is in @cite{newman-2000} §70 Table 38.

• subj : Subject
• tam : TAM
• mode : Mode
• form : String

  Surface form (graphic, with marked tones).

def Fragments.Hausa.Inflection.instReprPAC.repr : PAC → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instReprPAC : Repr PAC

Equations

• Fragments.Hausa.Inflection.instReprPAC = { reprPrec := Fragments.Hausa.Inflection.instReprPAC.repr }

def Fragments.Hausa.Inflection.PAC.WellFormed (p : PAC) : Prop

A PAC is well-formed iff the relative mode is licensed by the TAM. Propositional predicate (with Decidable).

Equations

• p.WellFormed = (p.mode = Fragments.Hausa.Inflection.Mode.relative → p.tam.HasRelativeForm)

@[implicit_reducible]

instance Fragments.Hausa.Inflection.instDecidableWellFormed (p : PAC) : Decidable p.WellFormed

Equations

• Fragments.Hausa.Inflection.instDecidableWellFormed p = Fragments.Hausa.Inflection.instDecidableWellFormed._aux_1 p

def Fragments.Hausa.Inflection.mkGeneralPAC (subj : Subject) (tam : TAM) (form : String) : PAC

Smart constructor for a General-mode PAC. Always well-formed.

Equations

• Fragments.Hausa.Inflection.mkGeneralPAC subj tam form = { subj := subj, tam := tam, mode := Fragments.Hausa.Inflection.Mode.general, form := form }

def Fragments.Hausa.Inflection.mkRelativePAC (subj : Subject) (tam : TAM) (form : String) : tam.HasRelativeForm → PAC

Smart constructor for a Relative-mode PAC. Takes a proof that the TAM admits a relative form; well-formedness then follows immediately (see mkRelativePAC_wellFormed).

Equations

• Fragments.Hausa.Inflection.mkRelativePAC subj tam form x✝ = { subj := subj, tam := tam, mode := Fragments.Hausa.Inflection.Mode.relative, form := form }

theorem Fragments.Hausa.Inflection.mkRelativePAC_wellFormed (s : Subject) (t : TAM) (f : String) (h : t.HasRelativeForm) : (mkRelativePAC s t f h).WellFormed

A PAC built by mkRelativePAC is well-formed: the proof obligation threaded through the smart constructor is the witness.

def Fragments.Hausa.Inflection.cmp_3sm_G : PAC

3sg.M completive, General form yā (high tone).

Equations

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

def Fragments.Hausa.Inflection.cmp_3sm_R : PAC

3sg.M completive, Relative form yà (low tone). The G/R contrast here is purely tonal — a textbook minimal pair.

Equations

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

def Fragments.Hausa.Inflection.cmp_3sf_R : PAC

3sg.F completive, Relative form ta (@cite{newman-2000} §70.2, @cite{hartmann-zimmermann-2007} eq. 24).

Equations

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

def Fragments.Hausa.Inflection.cont_3sm_G : PAC

3sg.M continuous, General form yanā.

Equations

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

def Fragments.Hausa.Inflection.cont_3sm_R : PAC

3sg.M continuous, Relative form yake — a stem alternation, not just a tone change (@cite{newman-2000} §70.2).

Equations

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

def Fragments.Hausa.Inflection.cont_3sf_R : PAC

3sg.F continuous, Relative form takèe (@cite{hartmann-zimmermann-2007} eq. 22).

Equations

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

def Fragments.Hausa.Inflection.cmp_1sg_G : PAC

1sg completive, General form naa (@cite{hartmann-zimmermann-2007} eq. 23).

Equations

• Fragments.Hausa.Inflection.cmp_1sg_G = Fragments.Hausa.Inflection.mkGeneralPAC { person := Features.Person.Category.s1, gender := none } Fragments.Hausa.Inflection.TAM.completive "naa"

def Fragments.Hausa.Inflection.cont_1sg_R : PAC

1sg continuous, Relative form nakèe (@cite{hartmann-zimmermann-2007} eq. 29).

Equations

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

def Fragments.Hausa.Inflection.fut_1sg : PAC

1sg future zân (@cite{hartmann-zimmermann-2007} eqs. 25, 30). No General/Relative contrast in the future TAM.

Equations

• Fragments.Hausa.Inflection.fut_1sg = Fragments.Hausa.Inflection.mkGeneralPAC { person := Features.Person.Category.s1, gender := none } Fragments.Hausa.Inflection.TAM.future "zân"

def Fragments.Hausa.Inflection.subj_3sm : PAC

3sg.M subjunctive yà. No General/Relative contrast in this TAM.

Equations

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

def Fragments.Hausa.Inflection.representativePACs : List PAC

The PAC registry: representative cells used by downstream fragments (notably Hausa/Focus.lean). Every entry is well-formed by construction (see all_representative_PACs_wellFormed).

Equations

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

theorem Fragments.Hausa.Inflection.only_cmp_cont_split (t : TAM) : t.HasRelativeForm ↔ t = TAM.completive ∨ t = TAM.continuous

The G/R contrast is morphologically distinct only in completive and continuous. In our representative TAM list, exactly the completive and continuous admit a Relative form.

theorem Fragments.Hausa.Inflection.completive_3sm_G_R_contrast : cmp_3sm_G.form = "yā" ∧ cmp_3sm_R.form = "yà"

The completive G/R minimal pair. The 3sg.M completive surfaces as yā (G) vs yà (R) — a tonal minimal pair.

theorem Fragments.Hausa.Inflection.all_representative_PACs_wellFormed (p : PAC) : p ∈ representativePACs → p.WellFormed

Every PAC built by the smart constructors is well-formed. The representative registry is well-formed because every entry is built via mkGeneralPAC or mkRelativePAC.

theorem Fragments.Hausa.Inflection.registry_covers_relative_TAMs (t : TAM) : t.HasRelativeForm → (∃ p ∈ representativePACs, p.tam = t ∧ p.mode = Mode.general) ∧ ∃ p ∈ representativePACs, p.tam = t ∧ p.mode = Mode.relative

The registry covers both modes for every TAM that admits the split. This is what makes the registry a genuine empirical sample of the G/R contrast rather than a one-sided collection.