Hausa Focus and the Stabilizer nē/cē — mathlib-style

@cite{newman-2000} @cite{jaggar-green-2003} @cite{hartmann-zimmermann-2007}

Hausa expresses focus by two principal strategies (@cite{newman-2000} ch. 28, ch. 66):

1. In-situ focus: the focused constituent stays in its canonical position; focus is signaled prosodically (and contextually) without any morphosyntactic reflex.
2. Ex-situ focus: the focused constituent fronts to a clause-initial position. Two morphosyntactic reflexes are diagnostic:
   • the stabilizer nē (M / non-feminine-singular) or cē (F.SG) optionally surfaces after the focused phrase, agreeing in gender and number with the focus (@cite{newman-2000} §66.1).
   • the clause's TAM shifts to the Relative form (in completive and continuous; cf. Hausa/TAM.lean §1).

The Relative-form requirement is the main empirical hook: it ties ex-situ focus to the broader morphological General/Relative split shared with relative clauses and wh-questions (@cite{jaggar-green-2003} argue this is movement to a single CP-internal position, but we stay theory-neutral here and just record the licensing condition).

FocusConfig.Licensed is propositional (Prop with Decidable). It is not enforced as a Subtype invariant: the structure is unrestricted, and exSitu_with_genCmp below is an explicit ill-licensed example used to prove the predicate non-vacuous. The mkInSitu/mkExSitu constructors are ergonomic helpers; the ex-situ one takes a proof obligation that licenses what it builds.

inductive Fragments.Hausa.Focus.Strategy : Type

The two focus strategies in Hausa. Contrastive vs information focus distinctions cut across both strategies and live in study files.

• inSitu : Strategy
• exSitu : Strategy

@[implicit_reducible]

instance Fragments.Hausa.Focus.instDecidableEqStrategy : DecidableEq Strategy

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Focus.instReprStrategy : Repr Strategy

Equations

• Fragments.Hausa.Focus.instReprStrategy = { reprPrec := Fragments.Hausa.Focus.instReprStrategy.repr }

def Fragments.Hausa.Focus.instReprStrategy.repr : Strategy → ℕ → Std.Format

Equations

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

def Fragments.Hausa.Focus.instInhabitedStrategy.default : Strategy

Equations

• Fragments.Hausa.Focus.instInhabitedStrategy.default = Fragments.Hausa.Focus.Strategy.inSitu

@[implicit_reducible]

instance Fragments.Hausa.Focus.instInhabitedStrategy : Inhabited Strategy

Equations

• Fragments.Hausa.Focus.instInhabitedStrategy = { default := Fragments.Hausa.Focus.instInhabitedStrategy.default }

inductive Fragments.Hausa.Focus.Stabilizer : Type

The stabilizer surfaces with two allomorphs in agreement with the focused constituent: cē with feminine-singular focus, nē elsewhere (masculine singular and all plurals). The plural agrees with nē regardless of gender (@cite{newman-2000} §66.1).

• nee : Stabilizer
• cee : Stabilizer

@[implicit_reducible]

instance Fragments.Hausa.Focus.instDecidableEqStabilizer : DecidableEq Stabilizer

Equations

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

def Fragments.Hausa.Focus.instReprStabilizer.repr : Stabilizer → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Focus.instReprStabilizer : Repr Stabilizer

Equations

• Fragments.Hausa.Focus.instReprStabilizer = { reprPrec := Fragments.Hausa.Focus.instReprStabilizer.repr }

@[implicit_reducible]

instance Fragments.Hausa.Focus.instInhabitedStabilizer : Inhabited Stabilizer

Equations

• Fragments.Hausa.Focus.instInhabitedStabilizer = { default := Fragments.Hausa.Focus.instInhabitedStabilizer.default }

def Fragments.Hausa.Focus.instInhabitedStabilizer.default : Stabilizer

Equations

• Fragments.Hausa.Focus.instInhabitedStabilizer.default = Fragments.Hausa.Focus.Stabilizer.nee

def Fragments.Hausa.Focus.Stabilizer.form : Stabilizer → String

Surface form of the stabilizer.

Equations

• Fragments.Hausa.Focus.Stabilizer.nee.form = "nē"
• Fragments.Hausa.Focus.Stabilizer.cee.form = "cē"

def Fragments.Hausa.Focus.stabilizerFor (g : Features.SurfaceGender) (singular : Bool) : Stabilizer

Pick the stabilizer for a focused constituent of the given gender and number. The cē allomorph appears iff the focus is feminine AND singular.

Equations

• Fragments.Hausa.Focus.stabilizerFor Features.SurfaceGender.feminine true = Fragments.Hausa.Focus.Stabilizer.cee
• Fragments.Hausa.Focus.stabilizerFor g singular = Fragments.Hausa.Focus.Stabilizer.nee

structure Fragments.Hausa.Focus.FocusConfig : Type

A focused-clause configuration. The Strategy field determines whether the constituent fronts; in the ex-situ case, a stabilizer is optionally inserted and the clause's PAC must surface in Relative mode (when the TAM admits it).

• pac : Inflection.PAC

  The clause's PAC (subject + TAM + mode + form).

• strategy : Strategy

  The focus strategy.

• focusG : Features.SurfaceGender

  The gender of the focused constituent (determines nē vs cē).

• focusSG : Bool

  Whether the focused constituent is singular.

• hasStab : Bool

  Whether a stabilizer surfaces (optional in ex-situ; absent in-situ).

@[implicit_reducible]

instance Fragments.Hausa.Focus.instReprFocusConfig : Repr FocusConfig

Equations

• Fragments.Hausa.Focus.instReprFocusConfig = { reprPrec := Fragments.Hausa.Focus.instReprFocusConfig.repr }

def Fragments.Hausa.Focus.instReprFocusConfig.repr : FocusConfig → ℕ → Std.Format

Equations

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

def Fragments.Hausa.Focus.FocusConfig.stab? (c : FocusConfig) : Option Stabilizer

Stabilizer realised by this configuration, if any.

Equations

• c.stab? = if c.hasStab = true then some (Fragments.Hausa.Focus.stabilizerFor c.focusG c.focusSG) else none

def Fragments.Hausa.Focus.FocusConfig.Licensed (c : FocusConfig) : Prop

A FocusConfig is licensed iff:

• in-situ focus places no constraint on TAM mode, or
• ex-situ focus has the PAC in Relative mode whenever the PAC's TAM admits a Relative form (otherwise vacuously licensed).

This recovers the textbook generalisation that ex-situ focus is incompatible with the General-form completive/continuous, but morphologically vacuous for TAMs that lack a Relative form.

Equations

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

@[implicit_reducible]

instance Fragments.Hausa.Focus.instDecidableLicensed (c : FocusConfig) : Decidable c.Licensed

Equations

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

def Fragments.Hausa.Focus.mkInSitu (pac : Inflection.PAC) (focusG : Features.SurfaceGender) (focusSG : Bool) : FocusConfig

Smart constructor for an in-situ focus configuration. Always licensed; defaults to no stabilizer (in-situ focus carries no morphological reflex).

Equations

• Fragments.Hausa.Focus.mkInSitu pac focusG focusSG = { pac := pac, strategy := Fragments.Hausa.Focus.Strategy.inSitu, focusG := focusG, focusSG := focusSG, hasStab := false }

def Fragments.Hausa.Focus.mkExSitu (pac : Inflection.PAC) (focusG : Features.SurfaceGender) (focusSG : Bool) (hasStab : Bool := true) : (pac.tam.HasRelativeForm → pac.mode = Inflection.Mode.relative) → FocusConfig

Smart constructor for an ex-situ focus configuration. Takes a proof that if the TAM admits a Relative form, the PAC's mode is Relative; licensing then follows immediately (see mkExSitu_licensed).

Equations

• Fragments.Hausa.Focus.mkExSitu pac focusG focusSG hasStab x✝ = { pac := pac, strategy := Fragments.Hausa.Focus.Strategy.exSitu, focusG := focusG, focusSG := focusSG, hasStab := hasStab }

theorem Fragments.Hausa.Focus.mkExSitu_licensed (p : Inflection.PAC) (g : Features.SurfaceGender) (sg hs : Bool) (h : p.tam.HasRelativeForm → p.mode = Inflection.Mode.relative) : (mkExSitu p g sg hs h).Licensed

A FocusConfig built by mkExSitu is licensed: the proof obligation threaded through the smart constructor is the witness.

def Fragments.Hausa.Focus.exSitu_fem_relCmp : FocusConfig

Ex-situ focus of a feminine singular NP with the relative completive: fully licensed; surfaces with cē.

Equations

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

def Fragments.Hausa.Focus.inSitu_any : FocusConfig

In-situ focus places no morphological constraint: any PAC is OK.

Equations

• Fragments.Hausa.Focus.inSitu_any = Fragments.Hausa.Focus.mkInSitu Fragments.Hausa.Inflection.cmp_3sm_G Features.SurfaceGender.masculine true

def Fragments.Hausa.Focus.exSitu_with_genCmp : FocusConfig

An unlicensed ex-situ configuration with the General completive, constructed directly to demonstrate that the predicate has bite.

Equations

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

def Fragments.Hausa.Focus.focusConfigs : List FocusConfig

The focus-configuration registry: licensed examples used downstream. exSitu_with_genCmp is not in the registry — it is the explicit counterexample showing the predicate is non-vacuous.

Equations

• Fragments.Hausa.Focus.focusConfigs = [Fragments.Hausa.Focus.exSitu_fem_relCmp, Fragments.Hausa.Focus.inSitu_any]

theorem Fragments.Hausa.Focus.stabilizer_iff_FSG (g : Features.SurfaceGender) (sg : Bool) : stabilizerFor g sg = Stabilizer.cee ↔ g = Features.SurfaceGender.feminine ∧ sg = true

Stabilizer agreement. The cē allomorph appears exactly with feminine-singular focus; everything else takes nē.

theorem Fragments.Hausa.Focus.all_focusConfigs_licensed (c : FocusConfig) : c ∈ focusConfigs → c.Licensed

Every registered focus configuration is licensed. The smart constructors guarantee this; the universal theorem records the invariant for the registry as a whole.

theorem Fragments.Hausa.Focus.exSitu_with_genCmp_not_licensed : ¬exSitu_with_genCmp.Licensed

Ex-situ + General completive is not licensed. The morphological bite of the predicate.

theorem Fragments.Hausa.Focus.exSitu_fem_picks_cee : exSitu_fem_relCmp.stab? = some Stabilizer.cee

The licensed feminine-singular ex-situ example surfaces with cē.

def Fragments.Hausa.Focus.Stabilizer.toneAfter : Stabilizer → (host : Phonology.Autosegmental.RegisterTier.TRN) → Phonology.Autosegmental.RegisterTier.TRN

Surface tone of the stabilizer after a host whose final TBU has the given tone. The stabilizer nē/cē is polar-toned: it surfaces with the opposite tone of the immediately preceding syllable (@cite{newman-2000} §66.1).

Equations

• x✝.toneAfter host = Fragments.Hausa.Tone.polarOf host

theorem Fragments.Hausa.Focus.stabilizer_tone_is_polar (s : Stabilizer) (host : Phonology.Autosegmental.RegisterTier.TRN) : s.toneAfter host = Tone.polarOf host

Stabilizer tone is polarity (cross-fragment). The stabilizer's surface tone is exactly Tone.polarOf applied to the host's final tone — no separate stipulation. This grounds the polar-tone description of nē/cē in the same operator that handles the genitive linker -n, making the two cases instances of one autosegmental operation rather than parallel idiosyncrasies.

theorem Fragments.Hausa.Focus.stabilizer_toneAfter_involutive (s : Stabilizer) (h : Phonology.Autosegmental.RegisterTier.TRN) (hh : h ∈ [Phonology.Autosegmental.RegisterTier.TRN.H, Phonology.Autosegmental.RegisterTier.TRN.L]) : Tone.polarOf (s.toneAfter h) = h

Stabilizer-tone involutivity. Iterating the stabilizer-tone map twice returns to the host tone (on the H/L sublattice). Direct corollary of Tone.polarOf_involutive_on_HL.