@cite{cacchioli-2025} — Empirical Data @cite{cacchioli-2025}

Pure empirical data from @cite{cacchioli-2025} "The Syntax of Clausal Prefixes in Tigrinya." No theory imports — this file contains only observed patterns, grammaticality judgments, and co-occurrence restrictions.

Key observations

1. Four prefixes: zɨ-, kɨ-, kəmzi-, ʔay-...-n
2. Complementary distribution: No two prefixes co-occur
3. Verb class selection: The matrix verb determines which prefix appears
4. Fixed linear order: Prefix always precedes the verbal complex
5. Agreement asymmetry: kɨ- and ʔay-...-n take agreement; zɨ- and kəmzi- don't

inductive Phenomena.Complementation.Cacchioli2025.TigrinyaPrefix : Type

The four clausal prefixes attested in Tigrinya.

• zi : TigrinyaPrefix
• ki : TigrinyaPrefix
• kemzi : TigrinyaPrefix
• ay_n : TigrinyaPrefix

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instDecidableEqTigrinyaPrefix : DecidableEq TigrinyaPrefix

Equations

• Phenomena.Complementation.Cacchioli2025.instDecidableEqTigrinyaPrefix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Complementation.Cacchioli2025.instReprTigrinyaPrefix.repr : TigrinyaPrefix → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instReprTigrinyaPrefix : Repr TigrinyaPrefix

Equations

• Phenomena.Complementation.Cacchioli2025.instReprTigrinyaPrefix = { reprPrec := Phenomena.Complementation.Cacchioli2025.instReprTigrinyaPrefix.repr }

structure Phenomena.Complementation.Cacchioli2025.CooccurrenceJudgment : Type

A grammaticality judgment for a prefix combination. true = grammatical, false = ungrammatical.

• prefix1 : TigrinyaPrefix
• prefix2 : TigrinyaPrefix
• grammatical : Bool
• example_ : String

def Phenomena.Complementation.Cacchioli2025.instReprCooccurrenceJudgment.repr : CooccurrenceJudgment → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instReprCooccurrenceJudgment : Repr CooccurrenceJudgment

Equations

• Phenomena.Complementation.Cacchioli2025.instReprCooccurrenceJudgment = { reprPrec := Phenomena.Complementation.Cacchioli2025.instReprCooccurrenceJudgment.repr }

def Phenomena.Complementation.Cacchioli2025.instBEqCooccurrenceJudgment.beq : CooccurrenceJudgment → CooccurrenceJudgment → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Complementation.Cacchioli2025.instBEqCooccurrenceJudgment.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instBEqCooccurrenceJudgment : BEq CooccurrenceJudgment

Equations

• Phenomena.Complementation.Cacchioli2025.instBEqCooccurrenceJudgment = { beq := Phenomena.Complementation.Cacchioli2025.instBEqCooccurrenceJudgment.beq }

def Phenomena.Complementation.Cacchioli2025.cooccurrenceData : List CooccurrenceJudgment

No two prefixes can co-occur (complementary distribution).

Equations

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

theorem Phenomena.Complementation.Cacchioli2025.all_cooccurrences_ungrammatical : (cooccurrenceData.all fun (x : CooccurrenceJudgment) => x.grammatical == false) = true

All prefix combinations are ungrammatical (complementary distribution).

structure Phenomena.Complementation.Cacchioli2025.SelectionDatum : Type

A selection datum: a matrix verb selects a particular prefix.

• verb : String
• verbGloss : String
• verbClass : String
• selectedPrefix : TigrinyaPrefix
• example_ : String
• grammatical : Bool

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instReprSelectionDatum : Repr SelectionDatum

Equations

• Phenomena.Complementation.Cacchioli2025.instReprSelectionDatum = { reprPrec := Phenomena.Complementation.Cacchioli2025.instReprSelectionDatum.repr }

def Phenomena.Complementation.Cacchioli2025.instReprSelectionDatum.repr : SelectionDatum → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instBEqSelectionDatum : BEq SelectionDatum

Equations

• Phenomena.Complementation.Cacchioli2025.instBEqSelectionDatum = { beq := Phenomena.Complementation.Cacchioli2025.instBEqSelectionDatum.beq }

def Phenomena.Complementation.Cacchioli2025.instBEqSelectionDatum.beq : SelectionDatum → SelectionDatum → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Complementation.Cacchioli2025.instBEqSelectionDatum.beq x✝¹ x✝ = false

def Phenomena.Complementation.Cacchioli2025.selectionData : List SelectionDatum

Verb class selection data from @cite{cacchioli-2025}.

Equations

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

structure Phenomena.Complementation.Cacchioli2025.AgreementDatum : Type

Agreement data: which prefixes take agreement suffixes.

• prefix_ : TigrinyaPrefix
• takesAgreement : Bool

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instReprAgreementDatum : Repr AgreementDatum

Equations

• Phenomena.Complementation.Cacchioli2025.instReprAgreementDatum = { reprPrec := Phenomena.Complementation.Cacchioli2025.instReprAgreementDatum.repr }

def Phenomena.Complementation.Cacchioli2025.instReprAgreementDatum.repr : AgreementDatum → ℕ → Std.Format

Equations

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

def Phenomena.Complementation.Cacchioli2025.instBEqAgreementDatum.beq : AgreementDatum → AgreementDatum → Bool

Equations

• Phenomena.Complementation.Cacchioli2025.instBEqAgreementDatum.beq { prefix_ := a, takesAgreement := a_1 } { prefix_ := b, takesAgreement := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Complementation.Cacchioli2025.instBEqAgreementDatum.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Phenomena.Complementation.Cacchioli2025.instBEqAgreementDatum : BEq AgreementDatum

Equations

• Phenomena.Complementation.Cacchioli2025.instBEqAgreementDatum = { beq := Phenomena.Complementation.Cacchioli2025.instBEqAgreementDatum.beq }

def Phenomena.Complementation.Cacchioli2025.agreementData : List AgreementDatum

Equations

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

def Phenomena.Complementation.Cacchioli2025.ctpToFiniteness : Typology.Complementation.CTPClass → Option Bool

Map CTP reality status to [±finite] selection.

Realis CTPs (utterance, knowledge, commentative,...) select [+finite] complements — indicative/realis clauses whose Fin head bears [+finite].

Irrealis CTPs (desiderative, manipulative, modal,...) select [-finite] complements — subjunctive/irrealis clauses whose Fin head bears [-finite].

Some classes are variable (perception can take both finite and non-finite complements), so they return none.

Equations

• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.utterance = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.knowledge = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.commentative = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.propAttitude = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.desiderative = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.manipulative = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.modal = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.phasal = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.achievement = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.negative = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.perception = none
• Phenomena.Complementation.Cacchioli2025.ctpToFiniteness Typology.Complementation.CTPClass.pretence = none

def Phenomena.Complementation.Cacchioli2025.ctpToFactivity : Typology.Complementation.CTPClass → Option Bool

Map CTP class to [±factive] selection.

Factive CTPs presuppose the truth of their complement; their Force/C head bears [+factive]. Non-factive CTPs don't, bearing [-factive].

Equations

• Phenomena.Complementation.Cacchioli2025.ctpToFactivity Typology.Complementation.CTPClass.knowledge = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFactivity Typology.Complementation.CTPClass.commentative = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFactivity Typology.Complementation.CTPClass.perception = some true
• Phenomena.Complementation.Cacchioli2025.ctpToFactivity Typology.Complementation.CTPClass.utterance = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFactivity Typology.Complementation.CTPClass.propAttitude = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFactivity Typology.Complementation.CTPClass.desiderative = some false
• Phenomena.Complementation.Cacchioli2025.ctpToFactivity x✝ = none

theorem Phenomena.Complementation.Cacchioli2025.knowledge_selects_finite : ctpToFiniteness Typology.Complementation.CTPClass.knowledge = some true

Knowledge verbs select [+finite] (indicative) complements.

theorem Phenomena.Complementation.Cacchioli2025.desiderative_selects_nonfinite : ctpToFiniteness Typology.Complementation.CTPClass.desiderative = some false

Desiderative verbs select [-finite] (subjunctive/irrealis) complements.

theorem Phenomena.Complementation.Cacchioli2025.knowledge_is_factive : ctpToFactivity Typology.Complementation.CTPClass.knowledge = some true

Knowledge verbs select [+factive] complements.

theorem Phenomena.Complementation.Cacchioli2025.utterance_not_factive : ctpToFactivity Typology.Complementation.CTPClass.utterance = some false

Utterance verbs select [-factive] complements.

theorem Phenomena.Complementation.Cacchioli2025.realis_implies_finite : ctpToFiniteness Typology.Complementation.CTPClass.utterance = some true ∧ ctpToFiniteness Typology.Complementation.CTPClass.knowledge = some true ∧ ctpToFiniteness Typology.Complementation.CTPClass.commentative = some true ∧ ctpToFiniteness Typology.Complementation.CTPClass.propAttitude = some true

Realis CTP classes map to [+finite].

theorem Phenomena.Complementation.Cacchioli2025.irrealis_implies_nonfinite : ctpToFiniteness Typology.Complementation.CTPClass.desiderative = some false ∧ ctpToFiniteness Typology.Complementation.CTPClass.manipulative = some false ∧ ctpToFiniteness Typology.Complementation.CTPClass.modal = some false ∧ ctpToFiniteness Typology.Complementation.CTPClass.phasal = some false

Irrealis CTP classes map to [-finite].

theorem Phenomena.Complementation.Cacchioli2025.irrealis_always_nonfinite (c : Typology.Complementation.CTPClass) (b : Bool) (h : ctpToFiniteness c = some b) (hr : Typology.Complementation.ctpRealityStatus c = Typology.Complementation.RealityStatus.irrealis) : b = false

Irrealis CTP classes always map to [-finite] when they have a value. The converse (realis → [+finite]) does not hold universally: phasal verbs are realis but take non-finite complements.

theorem Phenomena.Complementation.Cacchioli2025.phasal_violates_realis_finite_correspondence : Typology.Complementation.ctpRealityStatus Typology.Complementation.CTPClass.phasal = Typology.Complementation.RealityStatus.realis ∧ ctpToFiniteness Typology.Complementation.CTPClass.phasal = some false

Cross-paper divergence theorem: phasal CTPs witness the failure of the realis ↔ finite correspondence. @cite{noonan-2007} §3.1.1 puts phasal complements in DTR, but the substrate's ctpRealityStatus classifies them as realis (event is asserted as actual). Cacchioli's feature-based analysis classifies the same complements as [-finite] (reduced). The contradiction makes visible a real Noonan- internal tension between the realis-as-asserted-fact criterion and the DTR → irrealis groupings of Table 2.3.

The witness: phasal is realis AND takes non-finite (irrealis-aligned) complements. Any unification forcing realis ↔ +finite would have to reclassify either Noonan's reality status of phasal or Cacchioli's finiteness assignment.

theorem Phenomena.Complementation.Cacchioli2025.zi_fvalue_topic_field : Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.zi.headCat = Minimalist.fValue Minimalist.Cat.Top

zɨ- (Rel) is at the same fValue level as Top (topic field, F5).

theorem Phenomena.Complementation.Cacchioli2025.ki_fvalue_boundary : Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.ki.headCat = 3

kɨ- (Fin) is at the IP/CP boundary (F3).

theorem Phenomena.Complementation.Cacchioli2025.kemzi_fvalue_clause_typing : Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.kemzi.headCat = 6

kəmzi- (Force) is at the clause-typing level (F6).

theorem Phenomena.Complementation.Cacchioli2025.ay_fvalue_inflectional : Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.ay_n.headCat = 2

ʔay-...-n (Neg) is in the inflectional domain (F2).

theorem Phenomena.Complementation.Cacchioli2025.prefixes_distinct_flevels : Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.ay_n.headCat < Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.ki.headCat ∧ Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.ki.headCat < Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.zi.headCat ∧ Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.zi.headCat < Minimalist.fValue Fragments.Tigrinya.ClausePrefixes.kemzi.headCat

The four prefixes target four distinct F-levels: Neg(2) < Fin(3) < Rel(5) < Force(6).

theorem Phenomena.Complementation.Cacchioli2025.agreement_matches_data_bridge : Fragments.Tigrinya.ClausePrefixes.zi.takesAgreementSuffix = false ∧ Fragments.Tigrinya.ClausePrefixes.ki.takesAgreementSuffix = true ∧ Fragments.Tigrinya.ClausePrefixes.kemzi.takesAgreementSuffix = false ∧ Fragments.Tigrinya.ClausePrefixes.ay_n.takesAgreementSuffix = true

Fragment agreement field matches empirical data for each prefix.

theorem Phenomena.Complementation.Cacchioli2025.only_neg_discontinuous : Fragments.Tigrinya.ClausePrefixes.zi.isDiscontinuous = false ∧ Fragments.Tigrinya.ClausePrefixes.ki.isDiscontinuous = false ∧ Fragments.Tigrinya.ClausePrefixes.kemzi.isDiscontinuous = false ∧ Fragments.Tigrinya.ClausePrefixes.ay_n.isDiscontinuous = true

Only ʔay-...-n is discontinuous.

theorem Phenomena.Complementation.Cacchioli2025.knowledge_selects_kemzi : ctpToFiniteness Typology.Complementation.CTPClass.knowledge = some true

Knowledge verbs select [+finite] → predicts kəmzi- (factive).

theorem Phenomena.Complementation.Cacchioli2025.desiderative_selects_ki : ctpToFiniteness Typology.Complementation.CTPClass.desiderative = some false

Desiderative verbs select [-finite] → predicts kɨ- (subjunctive).

theorem Phenomena.Complementation.Cacchioli2025.commentative_selects_kemzi : ctpToFiniteness Typology.Complementation.CTPClass.commentative = some true

Commentative verbs select [+finite] → predicts kəmzi- (factive).

theorem Phenomena.Complementation.Cacchioli2025.manipulative_selects_ki : ctpToFiniteness Typology.Complementation.CTPClass.manipulative = some false

Manipulative verbs select [-finite] → predicts kɨ- (subjunctive).

theorem Phenomena.Complementation.Cacchioli2025.neg_circumfix_realize : (Fragments.Tigrinya.ClausePrefixes.negCircumfix "mäs'ə").realize = "ʔay-mäs'ə-n"

The negative circumfix surfaces correctly for a sample verb.

theorem Phenomena.Complementation.Cacchioli2025.neg_circumfix_from_neg : (Fragments.Tigrinya.ClausePrefixes.negCircumfix "mäs'ə").gloss = Fragments.Tigrinya.ClausePrefixes.ay_n.gloss

The negative circumfix gloss is derived from the fragment entry.

theorem Phenomena.Complementation.Cacchioli2025.all_prefixes_verbal : Minimalist.catFamily Fragments.Tigrinya.ClausePrefixes.zi.headCat = Minimalist.CatFamily.verbal ∧ Minimalist.catFamily Fragments.Tigrinya.ClausePrefixes.ki.headCat = Minimalist.CatFamily.verbal ∧ Minimalist.catFamily Fragments.Tigrinya.ClausePrefixes.kemzi.headCat = Minimalist.CatFamily.verbal ∧ Minimalist.catFamily Fragments.Tigrinya.ClausePrefixes.ay_n.headCat = Minimalist.CatFamily.verbal

All four prefix heads are in the verbal extended projection.