Faust and Lampitelli (2026): Guttural syneresis in Tigrinya and Tigre

In Tigrinya and Tigre a low vowel in an open syllable before a guttural is syncopated, as in [sɨmʕ-i] from /s_mʌʕ-i/, the way /i/ is before /j/. Faust and Lampitelli explain this by Element Theory: gutturals and low vowels share the element |A|, and two adjacent |A|s fuse into one. The analysis runs in Strict CV with the lateral relations of Government Phonology, by fusion, dissociation and epenthesis applied in the order "rules apply" gives, which makes syneresis opaque in several forms. In the feature system the gutturals are no natural class, so the analysis needs the element.

Main statements

• not_isNaturalClass_gutturals: the four gutturals are no natural class of Tigrinya's consonants in the PHOIBLE features.
• rows_derived: every attested form of the paper's paradigms is a realization of the derivation of its underlying form.
• rows_unpredicted: the forms whose retained position the analysis does not predict.

Implementation notes

• The analysis runs over the paper's transcription, and its vowels and gutturals are the paper's; fragment_roots shows that its roots, read as segments, are the Tigrinya and Tigre fragments' roots.
• A form is a list of CV units; templates are positions (radical, geminable radical, fixed segment) with nuclei, instantiated by a fragment root. Gutturals do not geminate (§2.1), so a geminable position holding a guttural is a single unit ((12): -sʌʔɨl).
• The prefixes tɨ- and mɨ- carry empty nuclei realized by epenthesis, as in the paper's underlying forms (t_-, m_-); the causative ʔʌ- is lexical (19c).
• Among the realizations of a run of empty nuclei the analysis takes the Ethiosemitic option C▪C_C▪C (37a): reading left to right, a nucleus after a silent one is realized.
• Trans-guttural harmony "can, but does not have to apply" (§2.1), so realizations lists every option and rows_derived asks that each attested form be among them. Realization does not feed fusion again, the paper's first way out of the loop of (37b–d).
• The postvocalic spirantization of b ([nɨβaħ], (10b)) is outside the analysis; β is read as b.
• Not derived: the |I|-syneresis of (8)–(9) and the ejective asymmetry of fn. 8.

References

• [FL26]
• [KLV85]
• [Bac11]
• [Ang95]
• [Low96]
• [Sch04a]
• [KLV90]
• [Cha91]
• [SS01]
• [Kay92]
• [Bye11]
• [Buc00]

Vowels and gutturals

inductive FaustLampitelli2026.Vowel : Type

The vowels of Tigrinya and Tigre, six full qualities and the weak [ɨ] (p. 5).

• a : Vowel
• aBare : Vowel
• i : Vowel
• u : Vowel
• e : Vowel
• o : Vowel
• weak : Vowel

@[instance_reducible]

instance FaustLampitelli2026.instDecidableEqVowel : DecidableEq Vowel

Equations

• FaustLampitelli2026.instDecidableEqVowel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def FaustLampitelli2026.instReprVowel.repr : Vowel → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FaustLampitelli2026.instReprVowel : Repr Vowel

Equations

• FaustLampitelli2026.instReprVowel = { reprPrec := FaustLampitelli2026.instReprVowel.repr }

@[instance_reducible]

instance FaustLampitelli2026.instFintypeVowel : Fintype Vowel

Equations

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

def FaustLampitelli2026.Vowel.toIPA : Vowel → String

v.toIPA is the IPA symbol of the vowel v.

Equations

• FaustLampitelli2026.Vowel.a.toIPA = "a"
• FaustLampitelli2026.Vowel.aBare.toIPA = "ʌ"
• FaustLampitelli2026.Vowel.i.toIPA = "i"
• FaustLampitelli2026.Vowel.u.toIPA = "u"
• FaustLampitelli2026.Vowel.e.toIPA = "e"
• FaustLampitelli2026.Vowel.o.toIPA = "o"
• FaustLampitelli2026.Vowel.weak.toIPA = "ɨ"

def FaustLampitelli2026.Vowel.segment : Vowel → Phonology.Segment

v.segment is the vowel v in the Tigrinya fragment.

Equations

• FaustLampitelli2026.Vowel.a.segment = Tigrinya.Phonology.a
• FaustLampitelli2026.Vowel.aBare.segment = Tigrinya.Phonology.«ʌ»
• FaustLampitelli2026.Vowel.i.segment = Tigrinya.Phonology.i
• FaustLampitelli2026.Vowel.u.segment = Tigrinya.Phonology.u
• FaustLampitelli2026.Vowel.e.segment = Tigrinya.Phonology.e
• FaustLampitelli2026.Vowel.o.segment = Tigrinya.Phonology.o
• FaustLampitelli2026.Vowel.weak.segment = Tigrinya.Phonology.«ɨ»

def FaustLampitelli2026.Vowel.IsLow : Vowel → Prop

The low vowels are [a] and [ʌ].

Equations

• FaustLampitelli2026.Vowel.a.IsLow = True
• FaustLampitelli2026.Vowel.aBare.IsLow = True
• x✝.IsLow = False

@[instance_reducible]

instance FaustLampitelli2026.instDecidablePredVowelIsLow : DecidablePred Vowel.IsLow

Equations

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

inductive FaustLampitelli2026.Guttural : Type

The four gutturals are the glottals [ʔ, h] and the pharyngeals [ʕ, ħ].

• glottalStop : Guttural
• h : Guttural
• pharyngealVoiced : Guttural
• pharyngealVoiceless : Guttural

@[instance_reducible]

instance FaustLampitelli2026.instDecidableEqGuttural : DecidableEq Guttural

Equations

• FaustLampitelli2026.instDecidableEqGuttural x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FaustLampitelli2026.instReprGuttural : Repr Guttural

Equations

• FaustLampitelli2026.instReprGuttural = { reprPrec := FaustLampitelli2026.instReprGuttural.repr }

def FaustLampitelli2026.instReprGuttural.repr : Guttural → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FaustLampitelli2026.instFintypeGuttural : Fintype Guttural

Equations

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

def FaustLampitelli2026.Guttural.toIPA : Guttural → String

g.toIPA is the IPA symbol of the guttural g.

Equations

• FaustLampitelli2026.Guttural.glottalStop.toIPA = "ʔ"
• FaustLampitelli2026.Guttural.h.toIPA = "h"
• FaustLampitelli2026.Guttural.pharyngealVoiced.toIPA = "ʕ"
• FaustLampitelli2026.Guttural.pharyngealVoiceless.toIPA = "ħ"

def FaustLampitelli2026.Guttural.ofIPA? : String → Option Guttural

Guttural.ofIPA? s is the guttural the IPA symbol s writes, if any.

Equations

• FaustLampitelli2026.Guttural.ofIPA? "ʔ" = some FaustLampitelli2026.Guttural.glottalStop
• FaustLampitelli2026.Guttural.ofIPA? "h" = some FaustLampitelli2026.Guttural.h
• FaustLampitelli2026.Guttural.ofIPA? "ʕ" = some FaustLampitelli2026.Guttural.pharyngealVoiced
• FaustLampitelli2026.Guttural.ofIPA? "ħ" = some FaustLampitelli2026.Guttural.pharyngealVoiceless
• FaustLampitelli2026.Guttural.ofIPA? x✝ = none

theorem FaustLampitelli2026.Guttural.ofIPA?_toIPA (g : Guttural) : ofIPA? g.toIPA = some g

def FaustLampitelli2026.Guttural.segment : Guttural → Phonology.Segment

g.segment is the guttural g in the Tigrinya fragment.

Equations

• FaustLampitelli2026.Guttural.glottalStop.segment = Tigrinya.Phonology.«ʔ»
• FaustLampitelli2026.Guttural.h.segment = Tigrinya.Phonology.h
• FaustLampitelli2026.Guttural.pharyngealVoiced.segment = Tigrinya.Phonology.«ʕ»
• FaustLampitelli2026.Guttural.pharyngealVoiceless.segment = Tigrinya.Phonology.ħ

def FaustLampitelli2026.Guttural.IsPharyngeal : Guttural → Prop

The pharyngeals are [ʕ] and [ħ].

Equations

• FaustLampitelli2026.Guttural.pharyngealVoiced.IsPharyngeal = True
• FaustLampitelli2026.Guttural.pharyngealVoiceless.IsPharyngeal = True
• x✝.IsPharyngeal = False

@[instance_reducible]

instance FaustLampitelli2026.instDecidablePredGutturalIsPharyngeal : DecidablePred Guttural.IsPharyngeal

Equations

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

theorem FaustLampitelli2026.not_isNaturalClass_gutturals : ¬Phonology.IsNaturalClass Tigrinya.Phonology.consonants (Finset.image Guttural.segment Finset.univ)

In the feature system the gutturals are no natural class of Tigrinya's consonants, since what the glottals and the pharyngeals share also describes the dorsal obstruents. Element Theory groups them by their |A| (20).

Element-theoretic representations (20)–(22)

def FaustLampitelli2026.vowelET : Vowel → ElementTheory.MR

vowelET v is the melody of the vowel v (21)–(22). [ʌ] is |A| and [a] headed |A|, the mid vowels combine |A| with |I| or |U|, and the weak vowel is the realization of an empty nucleus.

Equations

• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.a = ElementTheory.MR.headedSimplex ElementTheory.Element.A
• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.aBare = ElementTheory.MR.simplex ElementTheory.Element.A
• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.i = ElementTheory.MR.headedSimplex ElementTheory.Element.I
• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.u = ElementTheory.MR.headedSimplex ElementTheory.Element.U
• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.e = ElementTheory.MR.headedSimplex ElementTheory.Element.I ⊔ ElementTheory.MR.simplex ElementTheory.Element.A
• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.o = ElementTheory.MR.headedSimplex ElementTheory.Element.U ⊔ ElementTheory.MR.simplex ElementTheory.Element.A
• FaustLampitelli2026.vowelET FaustLampitelli2026.Vowel.weak = ⊥

def FaustLampitelli2026.gutturalET : Guttural → ElementTheory.MR

gutturalET g is the melody of the guttural g. Every guttural contains |A|, and the pharyngeals are headed by it (20).

Equations

• One or more equations did not get rendered due to their size.
• FaustLampitelli2026.gutturalET FaustLampitelli2026.Guttural.glottalStop = ElementTheory.MR.headedSimplex ElementTheory.Element.glottal ⊔ ElementTheory.MR.simplex ElementTheory.Element.A
• FaustLampitelli2026.gutturalET FaustLampitelli2026.Guttural.h = ElementTheory.MR.headedSimplex ElementTheory.Element.H ⊔ ElementTheory.MR.simplex ElementTheory.Element.A

theorem FaustLampitelli2026.mem_elements_gutturalET (g : Guttural) : ElementTheory.Element.A ∈ (gutturalET g).elements

theorem FaustLampitelli2026.mem_heads_gutturalET_iff (g : Guttural) : ElementTheory.Element.A ∈ (gutturalET g).heads ↔ g.IsPharyngeal

def FaustLampitelli2026.IsLowA (v : Vowel) : Prop

IsLowA v says that the vowel's melody is |A| alone, as for the low vowels of (21). The mid vowels carry |A| in a complex expression, which blocks fusion (§3.2.2).

Equations

• FaustLampitelli2026.IsLowA v = ((FaustLampitelli2026.vowelET v).elements = {ElementTheory.Element.A})

@[instance_reducible]

instance FaustLampitelli2026.instDecidablePredVowelIsLowA : DecidablePred IsLowA

Equations

• FaustLampitelli2026.instDecidablePredVowelIsLowA x✝ = { decide := decide ((FaustLampitelli2026.vowelET x✝).elements.val = {ElementTheory.Element.A}.val), reflects_decide := ⋯ }

theorem FaustLampitelli2026.isLowA_iff_isLow (v : Vowel) : IsLowA v ↔ v.IsLow

def FaustLampitelli2026.Vowel.ofMR? (m : ElementTheory.MR) : Option Vowel

The vowel with a given melody, if any.

Equations

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

def FaustLampitelli2026.lowered (v : Vowel) : Vowel

The fused |A|, spanning nucleus and consonant, is headed ((21), (27)), so a fused vowel is realized with |A| as its head and [ʌ] lowers to [a].

Equations

• FaustLampitelli2026.lowered v = (FaustLampitelli2026.Vowel.ofMR? (FaustLampitelli2026.vowelET v ⊔ ElementTheory.MR.headedSimplex ElementTheory.Element.A)).getD v

theorem FaustLampitelli2026.lowered_aBare : lowered Vowel.aBare = Vowel.a

Strict CV forms

inductive FaustLampitelli2026.Cons : Type

A consonantal position is a guttural, or any other consonant by its transcription.

• guttural (g : Guttural) : Cons
• plain (s : String) : Cons

def FaustLampitelli2026.instDecidableEqCons.decEq (x✝ x✝¹ : Cons) : Decidable (x✝ = x✝¹)

Equations

• FaustLampitelli2026.instDecidableEqCons.decEq (FaustLampitelli2026.Cons.guttural a) (FaustLampitelli2026.Cons.guttural b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• FaustLampitelli2026.instDecidableEqCons.decEq (FaustLampitelli2026.Cons.guttural g) (FaustLampitelli2026.Cons.plain s) = isFalse ⋯
• FaustLampitelli2026.instDecidableEqCons.decEq (FaustLampitelli2026.Cons.plain s) (FaustLampitelli2026.Cons.guttural g) = isFalse ⋯
• FaustLampitelli2026.instDecidableEqCons.decEq (FaustLampitelli2026.Cons.plain a) (FaustLampitelli2026.Cons.plain b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FaustLampitelli2026.instDecidableEqCons : DecidableEq Cons

Equations

• FaustLampitelli2026.instDecidableEqCons = FaustLampitelli2026.instDecidableEqCons.decEq

def FaustLampitelli2026.instReprCons.repr : Cons → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FaustLampitelli2026.instReprCons : Repr Cons

Equations

• FaustLampitelli2026.instReprCons = { reprPrec := FaustLampitelli2026.instReprCons.repr }

def FaustLampitelli2026.Cons.ofIPA (s : String) : Cons

The consonant written by a root segment.

Equations

• FaustLampitelli2026.Cons.ofIPA s = match FaustLampitelli2026.Guttural.ofIPA? s with | some g => FaustLampitelli2026.Cons.guttural g | none => FaustLampitelli2026.Cons.plain s

def FaustLampitelli2026.Cons.HasA : Cons → Prop

c.HasA says that the consonant's melody contains |A|, which every guttural's does (20). Other consonants carry no representation here, since ejectives also lower but never trigger syneresis (fn. 8).

Equations

• (FaustLampitelli2026.Cons.guttural g).HasA = (ElementTheory.Element.A ∈ (FaustLampitelli2026.gutturalET g).elements)
• (FaustLampitelli2026.Cons.plain s).HasA = False

@[instance_reducible]

instance FaustLampitelli2026.instDecidablePredConsHasA : DecidablePred Cons.HasA

Equations

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

theorem FaustLampitelli2026.hasA_guttural (g : Guttural) : (Cons.guttural g).HasA

def FaustLampitelli2026.Cons.chars : Cons → List Char

The transcription of a consonant.

Equations

• (FaustLampitelli2026.Cons.guttural g).chars = g.toIPA.toList
• (FaustLampitelli2026.Cons.plain s).chars = s.toList

inductive FaustLampitelli2026.Nuc : Type

A nucleus in the course of a derivation (29) is empty, empty but to be realized (▪), or a lexical vowel, shaded when fused with an adjacent guttural.

• empty : Nuc
• mark : Nuc
• vowel (v : Vowel) (fused : Bool) : Nuc

@[instance_reducible]

instance FaustLampitelli2026.instDecidableEqNuc : DecidableEq Nuc

Equations

• FaustLampitelli2026.instDecidableEqNuc = FaustLampitelli2026.instDecidableEqNuc.decEq

def FaustLampitelli2026.instDecidableEqNuc.decEq (x✝ x✝¹ : Nuc) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• FaustLampitelli2026.instDecidableEqNuc.decEq FaustLampitelli2026.Nuc.empty FaustLampitelli2026.Nuc.empty = isTrue ⋯
• FaustLampitelli2026.instDecidableEqNuc.decEq FaustLampitelli2026.Nuc.empty FaustLampitelli2026.Nuc.mark = isFalse FaustLampitelli2026.instDecidableEqNuc.decEq._proof_3
• FaustLampitelli2026.instDecidableEqNuc.decEq FaustLampitelli2026.Nuc.empty (FaustLampitelli2026.Nuc.vowel v fused) = isFalse ⋯
• FaustLampitelli2026.instDecidableEqNuc.decEq FaustLampitelli2026.Nuc.mark FaustLampitelli2026.Nuc.empty = isFalse FaustLampitelli2026.instDecidableEqNuc.decEq._proof_5
• FaustLampitelli2026.instDecidableEqNuc.decEq FaustLampitelli2026.Nuc.mark FaustLampitelli2026.Nuc.mark = isTrue ⋯
• FaustLampitelli2026.instDecidableEqNuc.decEq FaustLampitelli2026.Nuc.mark (FaustLampitelli2026.Nuc.vowel v fused) = isFalse ⋯
• FaustLampitelli2026.instDecidableEqNuc.decEq (FaustLampitelli2026.Nuc.vowel v fused) FaustLampitelli2026.Nuc.empty = isFalse ⋯
• FaustLampitelli2026.instDecidableEqNuc.decEq (FaustLampitelli2026.Nuc.vowel v fused) FaustLampitelli2026.Nuc.mark = isFalse ⋯

def FaustLampitelli2026.instReprNuc.repr : Nuc → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance FaustLampitelli2026.instReprNuc : Repr Nuc

Equations

• FaustLampitelli2026.instReprNuc = { reprPrec := FaustLampitelli2026.instReprNuc.repr }

structure FaustLampitelli2026.CV : Type

A CV unit ([Low96]).

• c : Cons
• v : Nuc

@[instance_reducible]

instance FaustLampitelli2026.instDecidableEqCV : DecidableEq CV

Equations

• FaustLampitelli2026.instDecidableEqCV = FaustLampitelli2026.instDecidableEqCV.decEq

def FaustLampitelli2026.instDecidableEqCV.decEq (x✝ x✝¹ : CV) : Decidable (x✝ = x✝¹)

Equations

• FaustLampitelli2026.instDecidableEqCV.decEq { c := a, v := a_1 } { c := b, v := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance FaustLampitelli2026.instReprCV : Repr CV

Equations

• FaustLampitelli2026.instReprCV = { reprPrec := FaustLampitelli2026.instReprCV.repr }

def FaustLampitelli2026.instReprCV.repr : CV → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev FaustLampitelli2026.Form : Type

A form is a strict iteration of CV units.

Equations

• FaustLampitelli2026.Form = List FaustLampitelli2026.CV

def FaustLampitelli2026.Contentful (f : Form) (i : ℕ) : Prop

The nucleus at i is contentful, so that it properly governs the nucleus before it (23a).

Equations

• FaustLampitelli2026.Contentful f i = match f[i]? with | some { c := c, v := FaustLampitelli2026.Nuc.vowel v fused } => True | x => False

@[instance_reducible]

instance FaustLampitelli2026.instDecidableContentful (f : Form) (i : ℕ) : Decidable (Contentful f i)

Equations

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

def FaustLampitelli2026.HasAAt (f : Form) (i : ℕ) : Prop

The consonant at i contains |A|.

Equations

• FaustLampitelli2026.HasAAt f i = match f[i]? with | some u => u.c.HasA | none => False

@[instance_reducible]

instance FaustLampitelli2026.instDecidableHasAAt (f : Form) (i : ℕ) : Decidable (HasAAt f i)

Equations

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

def FaustLampitelli2026.GeminateInternal (f : Form) (i : ℕ) : Prop

The nucleus at i sits inside a geminate.

Equations

• FaustLampitelli2026.GeminateInternal f i = match f[i]?, f[i + 1]? with | some u, some u' => u.c = u'.c | x, x_1 => False

@[instance_reducible]

instance FaustLampitelli2026.instDecidableGeminateInternal (f : Form) (i : ℕ) : Decidable (GeminateInternal f i)

Equations

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

The operations of (30)

def FaustLampitelli2026.fusion (f : Form) : Form

Fusion ((26b), (27b), (28b)) fuses a low vowel next to an |A| consonant, its own onset or the next, with that consonant and lowers it. Fusion always applies (§3.2.2).

Equations

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

def FaustLampitelli2026.dissociation (f : Form) : Form

Dissociation (26c) empties a fused nucleus iff it is properly governed by a contentful nucleus and is not the licensor of its own fused domain, that is, iff the guttural is the next onset (Av + Ac) rather than its own (Ac + Av, (28)).

Equations

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

def FaustLampitelli2026.epenthesis (f : Form) : Form

Epenthesis (30)–(31) marks the empty nuclei that must be realized. The word-final nucleus and a nucleus inside a geminate stay empty; the initial nucleus (no initial clusters), the nucleus licensing a word-internal guttural (25), a nucleus after a silent empty one (no triconsonantal clusters) and a nucleus before a geminate are realized; every other empty nucleus is governed and silent.

Equations

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

def FaustLampitelli2026.derive (f : Form) : Form

The derivation applies the operations in the order "rules apply" gives (30), since fusion creates the environment of dissociation, which creates that of epenthesis.

Equations

• FaustLampitelli2026.derive f = FaustLampitelli2026.epenthesis (FaustLampitelli2026.dissociation (FaustLampitelli2026.fusion f))

def FaustLampitelli2026.vowelAt (f : Form) (i : ℕ) : Option Vowel

The lexical vowel at i, if any.

Equations

• FaustLampitelli2026.vowelAt f i = match f[i]? with | some { c := c, v := FaustLampitelli2026.Nuc.vowel v fused } => some v | x => none

def FaustLampitelli2026.realizeMark (f : Form) (i : ℕ) : List (List Char)

A nucleus to be realized surfaces as the weak vowel, or, by trans-guttural harmony ((7), (19c)), as a copy of the vowel across an adjacent guttural in either direction.

Equations

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

def FaustLampitelli2026.realizeNuc (f : Form) (i : ℕ) : List (List Char)

The realizations of the nucleus at i.

Equations

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

def FaustLampitelli2026.consAt (f : Form) (i : ℕ) : List Char

The transcription of the consonant at i.

Equations

• FaustLampitelli2026.consAt f i = match f[i]? with | some u => u.c.chars | none => []

def FaustLampitelli2026.realizations (f : Form) : List (List Char)

The surface forms of a form are its consonants and realized nuclei in order, one form per choice of realization.

Equations

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

theorem FaustLampitelli2026.fusion_fuses (f : Form) (i : ℕ) (c : Cons) (v : Vowel) (h : (fusion f)[i]? = some { c := c, v := Nuc.vowel v false }) : ¬(IsLowA v ∧ (c.HasA ∨ HasAAt f (i + 1)))

After fusion no unfused low vowel is adjacent to an |A| consonant, since fusion always applies among two adjacent |A|s (§3.2.2).

theorem FaustLampitelli2026.dissociation_empty_iff (f : Form) (i : ℕ) (u : CV) (h : f[i]? = some u) : (dissociation f)[i]? = some { c := u.c, v := Nuc.empty } ↔ u.v = Nuc.empty ∨ ∃ (v : Vowel), u.v = Nuc.vowel v true ∧ HasAAt f (i + 1) ∧ ¬u.c.HasA ∧ Contentful f (i + 1)

Dissociation empties exactly the fused nuclei that are governed and not self-licensed ((26c), (28)).

Templates and suffixes (§2.1)

inductive FaustLampitelli2026.Pos : Type

A templatic position is a radical, a radical geminated where it can be, since gutturals cannot geminate (§2.1, (12)), or fixed segmental material.

• rad (i : ℕ) : Pos
• gem (i : ℕ) : Pos
• seg (s : String) : Pos

@[reducible, inline]

abbrev FaustLampitelli2026.Template : Type

A template is a list of positions with their nuclei; Q, T, L are the radicals.

Equations

• FaustLampitelli2026.Template = List (FaustLampitelli2026.Pos × FaustLampitelli2026.Nuc)

@[reducible, inline]

abbrev FaustLampitelli2026.V (v : Vowel) : Nuc

A lexical vowel.

Equations

• FaustLampitelli2026.V v = FaustLampitelli2026.Nuc.vowel v false

def FaustLampitelli2026.instantiate (t : Template) (r : Morphology.ConsonantalRoot String) : Option Form

A template instantiated by a root.

Equations

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

structure FaustLampitelli2026.Suffix : Type

A suffix is a vowel filling the stem-final nucleus, then further CV units.

• vowel : Option Vowel
• rest : List (String × Nuc)

def FaustLampitelli2026.attach (f : Form) (s : Suffix) : Form

A stem with a suffix.

Equations

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

def FaustLampitelli2026.prefix2 : Template

The 2nd-person prefix tɨ-, an empty nucleus in the underlying forms of (31)–(39).

Equations

• FaustLampitelli2026.prefix2 = [(FaustLampitelli2026.Pos.seg "t", FaustLampitelli2026.Nuc.empty)]

def FaustLampitelli2026.depPrf : Template

DEP.PRF QʌTʌL (4).

Equations

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

def FaustLampitelli2026.depPrfB : Template

The type B DEP.PRF QʌTTʌL, with medial gemination (18b).

Equations

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

def FaustLampitelli2026.depPrfC : Template

The type C DEP.PRF QaTʌL, with [a] after the first radical (18c).

Equations

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

def FaustLampitelli2026.prf : Template

PRF QʌTiL (4).

Equations

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

def FaustLampitelli2026.imprf : Template

IMPRF QʌTTɨL (4), the Tigre 2-IMP.M with its prefix (12).

Equations

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

def FaustLampitelli2026.imprf2 : Template

2-IMPRF tɨ-QʌTTɨL ((7), (17)).

Equations

• FaustLampitelli2026.imprf2 = FaustLampitelli2026.prefix2 ++ FaustLampitelli2026.imprf

def FaustLampitelli2026.imprf2NoGem : Template

The 2-IMPRF without gemination, tɨ-QʌTɨL, as (7c) [ta-ħadɨm] shows it.

Equations

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

def FaustLampitelli2026.passPrf : Template

PASS-PRF tɨ-QʌTiL (17).

Equations

• FaustLampitelli2026.passPrf = FaustLampitelli2026.prefix2 ++ FaustLampitelli2026.prf

def FaustLampitelli2026.imp : Template

IMP QɨTʌL ((5), (10)).

Equations

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

def FaustLampitelli2026.juss2 : Template

2-JUSS tɨ-QTʌL ((5)–(6), (31)–(32)).

Equations

• FaustLampitelli2026.juss2 = FaustLampitelli2026.prefix2 ++ FaustLampitelli2026.imp

def FaustLampitelli2026.impGem : Template

The Tigre IMP QaTTɨL of (5a).

Equations

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

def FaustLampitelli2026.jussGem2 : Template

The Tigre 2-JUSS tɨ-QaTTɨL of (5a).

Equations

• FaustLampitelli2026.jussGem2 = FaustLampitelli2026.prefix2 ++ FaustLampitelli2026.impGem

def FaustLampitelli2026.gerA : Template

The type A gerund mɨQTaL (13).

Equations

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

def FaustLampitelli2026.gerB : Template

The type B gerund mɨQTTaL (18b).

Equations

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

def FaustLampitelli2026.gerC : Template

The type C gerund mɨQaTaL ((18c), (39b)).

Equations

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

def FaustLampitelli2026.caus : Template

The causative PRF ʔʌQTiL (19c).

Equations

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

def FaustLampitelli2026.prf3 : Template

The Tigre PRF-3MSG stem QaTL- (6).

Equations

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

The paradigms (4)–(19) and the derivations (31)–(39)

inductive FaustLampitelli2026.Lang : Type

The languages of the rows.

• tigrinya : Lang
• tigre : Lang

@[instance_reducible]

instance FaustLampitelli2026.instDecidableEqLang : DecidableEq Lang

Equations

• FaustLampitelli2026.instDecidableEqLang x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance FaustLampitelli2026.instReprLang : Repr Lang

Equations

• FaustLampitelli2026.instReprLang = { reprPrec := FaustLampitelli2026.instReprLang.repr }

def FaustLampitelli2026.instReprLang.repr : Lang → ℕ → Std.Format

Equations

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

structure FaustLampitelli2026.Row : Type

An attested form with the root, template and suffix that build it, and whether the analysis predicts it.

• lang : Lang
• root : Morphology.ConsonantalRoot String
• template : Template
• suffix : Option Suffix
• forms : List (List Char)

  The attested forms, hyphens removed and β read as b.

• predicted : Bool

def FaustLampitelli2026.langTable : List (String × Lang)

Equations

• FaustLampitelli2026.langTable = [("tigr1271", FaustLampitelli2026.Lang.tigrinya), ("tigr1270", FaustLampitelli2026.Lang.tigre)]

def FaustLampitelli2026.tigrinyaRoots : List (String × Morphology.ConsonantalRoot String)

The Tigrinya roots of the rows, in the paper's transcription.

Equations

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

def FaustLampitelli2026.tigreRoots : List (String × Morphology.ConsonantalRoot String)

The Tigre roots of the rows, in the paper's transcription.

Equations

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

def FaustLampitelli2026.segment : Lang → String → Phonology.Segment

segment l x reads a letter of the paper's transcription of a root of language l as a segment of that language's fragment.

Equations

• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "g" = Tigrinya.Phonology.«ɡ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "r" = Tigrinya.Phonology.«ɾ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "f" = Tigrinya.Phonology.f
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "s" = Tigrinya.Phonology.s
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "m" = Tigrinya.Phonology.m
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "ʕ" = Tigrinya.Phonology.«ʕ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "ʔ" = Tigrinya.Phonology.«ʔ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "ħ" = Tigrinya.Phonology.ħ
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "b" = Tigrinya.Phonology.b
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "h" = Tigrinya.Phonology.h
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "d" = Tigrinya.Phonology.d
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "l" = Tigrinya.Phonology.l
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "n" = Tigrinya.Phonology.n
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigrinya "k" = Tigrinya.Phonology.k
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "m" = Tigre.Phonology.m
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "z" = Tigre.Phonology.z
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "n" = Tigre.Phonology.n
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "f" = Tigre.Phonology.f
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "g" = Tigre.Phonology.«ɡ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "r" = Tigre.Phonology.r
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "ħ" = Tigre.Phonology.ħ
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "tˁ" = Tigre.Phonology.«tʼ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "b" = Tigre.Phonology.b
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "h" = Tigre.Phonology.h
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "kˀ" = Tigre.Phonology.«kʼ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "sˁ" = Tigre.Phonology.«tsʼ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "s" = Tigre.Phonology.s
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "ʔ" = Tigre.Phonology.«ʔ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "l" = Tigre.Phonology.l
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "tˀ" = Tigre.Phonology.«tʼ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "ʕ" = Tigre.Phonology.«ʕ»
• FaustLampitelli2026.segment FaustLampitelli2026.Lang.tigre "k" = Tigre.Phonology.k
• FaustLampitelli2026.segment x✝¹ x✝ = ⊥

theorem FaustLampitelli2026.fragment_roots : List.map (fun (x : String × Morphology.ConsonantalRoot String) => Morphology.ConsonantalRoot.map (segment Lang.tigrinya) x.2) tigrinyaRoots = [Tigrinya.Phonology.whip, Tigrinya.Phonology.hear, Tigrinya.Phonology.arrest, Tigrinya.Phonology.pull, Tigrinya.Phonology.teach, Tigrinya.Phonology.slaughter, Tigrinya.Phonology.escape, Tigrinya.Phonology.ask, Tigrinya.Phonology.uncover, Tigrinya.Phonology.bark, Tigrinya.Phonology.hurt, Tigrinya.Phonology.bless, Tigrinya.Phonology.arf] ∧ List.map (fun (x : String × Morphology.ConsonantalRoot String) => Morphology.ConsonantalRoot.map (segment Lang.tigre) x.2) tigreRoots = [Tigre.Phonology.weigh, Tigre.Phonology.leave, Tigre.Phonology.wash, Tigre.Phonology.flee, Tigre.Phonology.getUp, Tigre.Phonology.whip, Tigre.Phonology.ask, Tigre.Phonology.load, Tigre.Phonology.uncover, Tigre.Phonology.pull]

The paper's roots, read as segments, are the fragments' roots.

def FaustLampitelli2026.templateTable : List (String × Template)

Equations

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

def FaustLampitelli2026.suffixTable : List (String × Suffix)

Equations

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

def FaustLampitelli2026.transcribe (s : String) : List Char

transcribe s is a transcription as compared with the realizations, hyphens removed and β read as b.

Equations

• FaustLampitelli2026.transcribe s = List.map (fun (c : Char) => if c = 'β' then 'b' else c) (List.filter (fun (x : Char) => decide (x ≠ '-')) s.toList)

def FaustLampitelli2026.Row.ofDatum (ex : Datum) : Option Row

Equations

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

theorem FaustLampitelli2026.row_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true

def FaustLampitelli2026.rows : List Row

Equations

• FaustLampitelli2026.rows = List.filterMap FaustLampitelli2026.Row.ofDatum FaustLampitelli2026.Examples.all

def FaustLampitelli2026.Row.stem (r : Row) : Option Form

The underlying form of a row is its template instantiated by its root, with its suffix.

Equations

• r.stem = Option.map (fun (f : FaustLampitelli2026.Form) => (Option.map (FaustLampitelli2026.attach f) r.suffix).getD f) (FaustLampitelli2026.instantiate r.template r.root)

def FaustLampitelli2026.Row.realizations (r : Row) : List (List Char)

The surface forms the analysis yields for a row.

Equations

• r.realizations = match r.stem with | some f => FaustLampitelli2026.realizations (FaustLampitelli2026.derive f) | none => []

theorem FaustLampitelli2026.rows_stem_isSome (r : Row) : r ∈ rows → r.stem.isSome = true

theorem FaustLampitelli2026.rows_derived (r : Row) : r ∈ rows → r.predicted = true → ∀ f ∈ r.forms, f ∈ r.realizations

Every attested form of (4)–(19) and (31)–(38) is a realization of the derivation of its underlying form.

theorem FaustLampitelli2026.rows_unpredicted (r : Row) : r ∈ rows → ¬r.predicted = true → ∀ f ∈ r.forms, f ∉ r.realizations

The forms of (17b–d) and (39) realize the position the analysis empties, which it does not predict (§3.3.3).