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

[New00] [Jag01]

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, …).

([New00] 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 ([New00] 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 Hausa.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 Hausa.instDecidableEqTAM : DecidableEq TAM

Equations

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

@[implicit_reducible]

instance Hausa.instReprTAM : Repr TAM

Equations

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

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

Equations

• Hausa.instReprTAM.repr Hausa.TAM.completive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.completive")).group prec✝
• Hausa.instReprTAM.repr Hausa.TAM.continuous prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.continuous")).group prec✝
• Hausa.instReprTAM.repr Hausa.TAM.future prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.future")).group prec✝
• Hausa.instReprTAM.repr Hausa.TAM.subjunctive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.subjunctive")).group prec✝
• Hausa.instReprTAM.repr Hausa.TAM.habitual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.habitual")).group prec✝
• Hausa.instReprTAM.repr Hausa.TAM.rhetorical prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.rhetorical")).group prec✝
• Hausa.instReprTAM.repr Hausa.TAM.potential prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.TAM.potential")).group prec✝

@[implicit_reducible]

instance Hausa.instInhabitedTAM : Inhabited TAM

Equations

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

def Hausa.TAM.all : List TAM

The seven TAMs in canonical order.

Equations

• Hausa.TAM.all = [Hausa.TAM.completive, Hausa.TAM.continuous, Hausa.TAM.future, Hausa.TAM.subjunctive, Hausa.TAM.habitual, Hausa.TAM.rhetorical, Hausa.TAM.potential]

def Hausa.TAM.HasRelativeForm : TAM → Prop

The General/Relative split surfaces morphologically only for the completive and continuous TAMs ([New00] §64.2, Table 32). HasRelativeForm is the propositional predicate; downstream constructors take it as a proof obligation.

Equations

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

@[implicit_reducible]

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

Equations

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

inductive Hausa.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 Hausa.instDecidableEqMode : DecidableEq Mode

Equations

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

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

Equations

• Hausa.instReprMode.repr Hausa.Mode.general prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Mode.general")).group prec✝
• Hausa.instReprMode.repr Hausa.Mode.relative prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Hausa.Mode.relative")).group prec✝

@[implicit_reducible]

instance Hausa.instReprMode : Repr Mode

Equations

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

@[implicit_reducible]

instance Hausa.instInhabitedMode : Inhabited Mode

Equations

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

structure Hausa.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 Person.Category for the singular/group cut and add a gender field that is empty (none) outside the 2sg/3sg cells.

• person : Person.Category
• gender : Option Gender

@[implicit_reducible]

instance Hausa.instDecidableEqSubject : DecidableEq Subject

Equations

• Hausa.instDecidableEqSubject = Hausa.instDecidableEqSubject.decEq

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

Equations

• Hausa.instDecidableEqSubject.decEq { person := a, gender := a_1 } { person := b, gender := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

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

Equations

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

@[implicit_reducible]

instance Hausa.instReprSubject : Repr Subject

Equations

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

def Hausa.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 Hausa.Subject.instDecidableHasGenderContrast (s : Subject) : Decidable s.HasGenderContrast

Equations

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

def Hausa.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 Hausa.gender_contrast_only_in_singular (s : Subject) : s ∈ hausaSubjects → s.HasGenderContrast → s.person = Person.Category.s2 ∨ s.person = Person.Category.s3

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

structure Hausa.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 [New00] §70 Table 38.

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

  Surface form (graphic, with marked tones).

@[implicit_reducible]

instance Hausa.instReprPAC : Repr PAC

Equations

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

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

Equations

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

def Hausa.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 = Hausa.Mode.relative → p.tam.HasRelativeForm)

@[implicit_reducible]

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

Equations

• Hausa.instDecidableWellFormed p = Hausa.instDecidableWellFormed._aux_1 p

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

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

Equations

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

def Hausa.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

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

theorem Hausa.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 Hausa.cmp_3sm_G : PAC

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

Equations

• Hausa.cmp_3sm_G = Hausa.mkGeneralPAC { person := Person.Category.s3, gender := some Gender.masculine } Hausa.TAM.completive "yā"

def Hausa.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

• Hausa.cmp_3sm_R = Hausa.mkRelativePAC { person := Person.Category.s3, gender := some Gender.masculine } Hausa.TAM.completive "yà" trivial

def Hausa.cmp_3sf_R : PAC

3sg.F completive, Relative form ta ([New00] §70.2, [HZ07] eq. 24).

Equations

• Hausa.cmp_3sf_R = Hausa.mkRelativePAC { person := Person.Category.s3, gender := some Gender.feminine } Hausa.TAM.completive "ta" trivial

def Hausa.cont_3sm_G : PAC

3sg.M continuous, General form yanā.

Equations

• Hausa.cont_3sm_G = Hausa.mkGeneralPAC { person := Person.Category.s3, gender := some Gender.masculine } Hausa.TAM.continuous "yanā"

def Hausa.cont_3sm_R : PAC

3sg.M continuous, Relative form yake — a stem alternation, not just a tone change ([New00] §70.2).

Equations

• Hausa.cont_3sm_R = Hausa.mkRelativePAC { person := Person.Category.s3, gender := some Gender.masculine } Hausa.TAM.continuous "yake" trivial

def Hausa.cont_3sf_R : PAC

3sg.F continuous, Relative form takèe ([HZ07] eq. 22).

Equations

• Hausa.cont_3sf_R = Hausa.mkRelativePAC { person := Person.Category.s3, gender := some Gender.feminine } Hausa.TAM.continuous "takèe" trivial

def Hausa.cmp_1sg_G : PAC

1sg completive, General form naa ([HZ07] eq. 23).

Equations

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

def Hausa.cont_1sg_R : PAC

1sg continuous, Relative form nakèe ([HZ07] eq. 29).

Equations

• Hausa.cont_1sg_R = Hausa.mkRelativePAC { person := Person.Category.s1, gender := none } Hausa.TAM.continuous "nakèe" trivial

def Hausa.fut_1sg : PAC

1sg future zân ([HZ07] eqs. 25, 30). No General/Relative contrast in the future TAM.

Equations

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

def Hausa.subj_3sm : PAC

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

Equations

• Hausa.subj_3sm = Hausa.mkGeneralPAC { person := Person.Category.s3, gender := some Gender.masculine } Hausa.TAM.subjunctive "yà"

def Hausa.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 Hausa.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 Hausa.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 Hausa.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 Hausa.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.