Faust (2026): Intrusion as template satisfaction and the QaTaT–QaTa problem in Semitic

Faust's *Misalignment principle bars a nonfinal root element from the template-final slot. A root whose final radical cannot take a [+consonantal] C-slot then satisfies the template in one of two ways: it leaves the slot vacant, as in Hebrew [kala], or the consonant of the feminine suffix fills it, as in Hebrew [tadmit] and Amharic [fäʤt-o]. The derivations run McCarthy's association conventions with slot specifications that bar glides and vowels from [+c] slots, and the feminine morph, inherent inflection on n, merges only with a nominal base. That gives the distribution of the intruding [t] across the Amharic paradigms, which Broselow's default consonant left unexplained, and the No-Crossing Constraint keeps it out of the hollow verbs.

Main statements

• klj_spread_misaligned: spreading the final consonant of √klj would misalign the root, so the final slot stays vacant.
• isNonCrossing_melodyLinks_intrude: the intruder's line crosses no root line.
• rows_surface: the derivations reproduce the squib's paradigms.
• intruder_distribution: the intruder occurs exactly in the nominal cells of the roots whose final radical is barred.

Implementation notes

• The derivations run over the squib's transcription. fragment_roots shows that its roots, read as segments, are the Hebrew and Amharic fragments' roots, the alternating stops of √kl and √skt realized as stops by Arad's rule.
• segClass lets a plain C-slot host a glide but no vowel and a [+c] slot only consonants, and merge states the squib's mergers d + j to ʤ, ä + a to a and ä + i to e.
• The medial geminate of the Amharic PFV is prespecified ({C C} in (7)). The suffix consonant associates to the rightmost vacant C-slot only inside its Autosegmental.window, and the morph's vowel does not surface, so the affix carries only t.
• The squib labels (13c) [mähid] where (12e) and its merger give [mähed], and the rows follow (12e). The IPFV and JUSS, whose templates the squib does not draw, and the PFV of √sma are not derived.

References

• [Fau26]
• [McC81]
• [Ara05]
• [Bro84]
• [Gre50]
• [Les95]
• [Low96]
• [Low14]
• [Gol76]

*Misalignment

def Faust2026.Misaligned {α : Type u_1} (m : Morphology.TemplateMatch α) : Prop

Misaligned m holds when some nonfinal root element is associated to the template-final slot, which *Misalignment (2), (6b) bans.

Equations

• Faust2026.Misaligned m = ∃ a ∈ m.associations, a.source = Morphology.AssocSource.root ∧ m.root.IsNonfinal a.melodyIndex ∧ m.template.isFinalSlot a.slotIndex

@[instance_reducible]

instance Faust2026.instDecidableMisaligned {α : Type u_1} (m : Morphology.TemplateMatch α) : Decidable (Misaligned m)

Equations

• Faust2026.instDecidableMisaligned m = Faust2026.instDecidableMisaligned._aux_1 m

theorem Faust2026.misaligned_append {α : Type u_1} (m : Morphology.TemplateMatch α) (l : List Morphology.Association) : Misaligned { root := m.root, vocalism := m.vocalism, affix := m.affix, template := m.template, associations := m.associations ++ l } ↔ Misaligned m ∨ ∃ a ∈ l, a.source = Morphology.AssocSource.root ∧ m.root.IsNonfinal a.melodyIndex ∧ m.template.isFinalSlot a.slotIndex

theorem Faust2026.misaligned_append_affix {α : Type u_1} (m : Morphology.TemplateMatch α) (l : List Morphology.Association) (h : ∀ a ∈ l, a.source = Morphology.AssocSource.affix) : Misaligned { root := m.root, vocalism := m.vocalism, affix := m.affix, template := m.template, associations := m.associations ++ l } ↔ Misaligned m

Lines from the affix tier never misalign the root, since the intruder "is not a radical" ((8), (10)).

Segments, patterns, and association

inductive Faust2026.SegClass : Type

The classes the [+consonantal] specification of a C-slot separates.

• consonant : SegClass
• glide : SegClass
• vowel : SegClass

@[instance_reducible]

instance Faust2026.instDecidableEqSegClass : DecidableEq SegClass

Equations

• Faust2026.instDecidableEqSegClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Faust2026.instReprSegClass.repr : SegClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Faust2026.instReprSegClass.repr Faust2026.SegClass.glide prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.SegClass.glide")).group prec✝
• Faust2026.instReprSegClass.repr Faust2026.SegClass.vowel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.SegClass.vowel")).group prec✝

@[instance_reducible]

instance Faust2026.instReprSegClass : Repr SegClass

Equations

• Faust2026.instReprSegClass = { reprPrec := Faust2026.instReprSegClass.repr }

def Faust2026.segClass : String → SegClass

The glide j and the nonconsonantal radicals a, i of the Amharic hollow roots (12c–e) are barred from [+c] slots; every other segment is a consonant.

Equations

• Faust2026.segClass "j" = Faust2026.SegClass.glide
• Faust2026.segClass "a" = Faust2026.SegClass.vowel
• Faust2026.segClass "i" = Faust2026.SegClass.vowel
• Faust2026.segClass x✝ = Faust2026.SegClass.consonant

def Faust2026.merge : String → String → String

merge states the mergers of two elements sharing a slot that the squib names. A glide joined to the preceding consonant palatalizes it ((7), [fäʤʤ-ä]), and a nonconsonantal radical merges with the vocalization, /a,ä/ yielding [a] and /i,ä/ yielding [e] (13).

Equations

• Faust2026.merge "d" "j" = "ʤ"
• Faust2026.merge "ä" "a" = "a"
• Faust2026.merge "ä" "i" = "e"
• Faust2026.merge x✝¹ x✝ = x✝¹

inductive Faust2026.Category : Type

Category is the category of the base a template builds. Gender markers are inherent inflection on n, so only a nominal base merges with the feminine morph (11).

• noun : Category
• verb : Category
• adjective : Category

@[instance_reducible]

instance Faust2026.instDecidableEqCategory : DecidableEq Category

Equations

• Faust2026.instDecidableEqCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Faust2026.instReprCategory.repr : Category → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Faust2026.instReprCategory.repr Faust2026.Category.noun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Category.noun")).group prec✝
• Faust2026.instReprCategory.repr Faust2026.Category.verb prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Category.verb")).group prec✝

@[instance_reducible]

instance Faust2026.instReprCategory : Repr Category

Equations

• Faust2026.instReprCategory = { reprPrec := Faust2026.instReprCategory.repr }

structure Faust2026.Pattern : Type

A pattern is a template with its lexical shape, namely its skeleton, category, vocalization and lines, segmental material outside the skeleton, and the parameters of the squib's derivations.

• template : Morphology.CVTemplate

  The skeleton.

• category : Category

  The category of the base.

• vocalism : List String

  The vocalization and its association lines.

• vocLines : List Morphology.Association
• pre : List String

  Segmental material preceding and following the skeleton.

• post : List String
• geminate : Option ℕ

  A slot prespecified as geminate ({C C} in (7)).

• joinsGlide : Bool

  A barred glide joins the consonant on its left (Amharic (7)) rather than floating (Hebrew (4)).

• truncates : Bool

  An unsatisfied final syllable is deleted (7a).

def Faust2026.lines (p : Pattern) (r : Morphology.ConsonantalRoot String) : Morphology.TemplateMatch String

The root associated with the C-slots by the conventions, one to one from left to right with the final radical spreading onto leftover slots, plus the pattern's vocalization lines.

Equations

• Faust2026.lines p r = ({ root := r, vocalism := p.vocalism, template := p.template, associations := [] }.associate Morphology.AssocSource.root).link p.vocLines

def Faust2026.Admits (m : Morphology.TemplateMatch String) (a : Morphology.Association) : Prop

m.Admits a says that the slot's specification admits the segment. A [+c] slot hosts consonants only ((4), (7), (13)), and a plain C-slot anything but a vowel.

Equations

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

@[instance_reducible]

instance Faust2026.instDecidableAdmits (m : Morphology.TemplateMatch String) (a : Morphology.Association) : Decidable (Admits m a)

Equations

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

def Faust2026.flankingV (m : Morphology.TemplateMatch String) (i : ℕ) : List ℕ

The V-slots flanking slot i.

Equations

• Faust2026.flankingV m i = List.filter (fun (s : ℕ) => decide (m.template.slotAt s = some Morphology.CVSlot.V)) [i - 1, i + 1]

def Faust2026.vocAt (m : Morphology.TemplateMatch String) (s : ℕ) : Option Morphology.Association

The vocalization line at slot s.

Equations

• Faust2026.vocAt m s = List.find? (fun (a : Morphology.Association) => a.source == Morphology.AssocSource.vocalism && a.slotIndex == s) m.associations

def Faust2026.join (p : Pattern) (m : Morphology.TemplateMatch String) (a : Morphology.Association) : Morphology.TemplateMatch String

join places a barred root element. A glide joins the slot of the consonant on its left where the pattern's language does that, Amharic and not Hebrew (7). A nonconsonantal radical merges with the vocalization on the V-slots flanking its slot, the vocalization element spreading to a flanking V-slot it did not occupy, so that the merger "occupies the two vocalic positions around the C position" (13b–c).

Equations

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

def Faust2026.associate (p : Pattern) (r : Morphology.ConsonantalRoot String) : Morphology.TemplateMatch String

Association under the slot specifications removes the rejected lines and joins or merges their elements as the pattern's language allows.

Equations

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

Intrusion

def Faust2026.melodyLinks (m : Morphology.TemplateMatch String) : Finset (ℕ × ℕ)

The consonantal melody of a base merged with a suffix, root elements then the suffix's, in the coordinates of Autosegmental.IsNonCrossing.

Equations

• Faust2026.melodyLinks m = m.links Morphology.AssocSource.root ∪ Finset.image (fun (p : ℕ × ℕ) => (p.1 + m.root.arity, p.2)) (m.links Morphology.AssocSource.affix)

def Faust2026.intrudeAt (m : Morphology.TemplateMatch String) (s : ℕ) : Morphology.TemplateMatch String

The feminine morph √(a)t merged with the base, its consonant associated to slot s.

Equations

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

theorem Faust2026.melodyLinks_intrudeAt (m : Morphology.TemplateMatch String) (s : ℕ) : melodyLinks (intrudeAt m s) = insert (m.root.arity, s) (melodyLinks m)

def Faust2026.intrude (m : Morphology.TemplateMatch String) : Morphology.TemplateMatch String

Intrusion (10b–c) associates the morph's consonant from right to left to the rightmost vacant C-slot, provided that slot lies in its window, so that its line crosses none of the root's; otherwise the consonant floats (13b–c).

Equations

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

theorem Faust2026.misaligned_intrudeAt (m : Morphology.TemplateMatch String) (s : ℕ) : Misaligned (intrudeAt m s) ↔ Misaligned m

theorem Faust2026.misaligned_intrude (m : Morphology.TemplateMatch String) : Misaligned (intrude m) ↔ Misaligned m

Intrusion is template satisfaction without misalignment, since the intruder never misaligns the root ((8), (10)).

theorem Faust2026.isNonCrossing_melodyLinks_intrude (m : Morphology.TemplateMatch String) (h : Autosegmental.IsNonCrossing (melodyLinks m)) : Autosegmental.IsNonCrossing (melodyLinks (intrude m))

The intruder's line never crosses a root line, so intrusion keeps the merged melody non-crossing.

def Faust2026.derive (p : Pattern) (r : Morphology.ConsonantalRoot String) : Morphology.TemplateMatch String

The derivation of a root in a pattern is association under the slot specifications followed, for a nominal base whose template is unsatisfied, by merger of the feminine morph ((10b), (11)).

Equations

• Faust2026.derive p r = if p.category = Faust2026.Category.noun ∧ ¬(Faust2026.associate p r).allCSlotsFilled then Faust2026.intrude (Faust2026.associate p r) else Faust2026.associate p r

theorem Faust2026.derive_of_category_ne_noun (p : Pattern) (r : Morphology.ConsonantalRoot String) (h : p.category ≠ Category.noun) : derive p r = associate p r

Only a nominal base merges with the feminine morph (11), so a verbal or adjectival base is realized as associated.

Realization

def Faust2026.hosted (m : Morphology.TemplateMatch String) (s : ℕ) : List String

hosted m s lists the segments slot s hosts, vocalization first, then root, then affix lines.

Equations

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

def Faust2026.realizeSlot (m : Morphology.TemplateMatch String) (s : ℕ) : Option String

realizeSlot m s merges the segments slot s hosts onto the first.

Equations

• Faust2026.realizeSlot m s = match Faust2026.hosted m s with | [] => none | x :: xs => some (List.foldl Faust2026.merge x xs)

def Faust2026.collapses (x : String) : List (Morphology.CVSlot × Option String) → Bool

collapses x l says that the V-slot realized x is followed by a vacant C-slot and a V-slot realized the same.

Equations

• Faust2026.collapses x ((c, none) :: (Morphology.CVSlot.V, some y) :: tail) = (decide c.IsC && x == y)
• Faust2026.collapses x x✝ = false

def Faust2026.collapse : Bool → List (Morphology.CVSlot × Option String) → List String

collapse lists the realized slots in order, V-slots around a vacant C-slot with the same realization surfacing once, since "the phonological length of these vowels is not translated to phonetic length" (13). The flag records that the vowel has already been realized.

Equations

• Faust2026.collapse x✝ [] = []
• Faust2026.collapse x✝ ((fst, none) :: tl) = Faust2026.collapse x✝ tl
• Faust2026.collapse true ((Morphology.CVSlot.V, some val) :: tl) = Faust2026.collapse false tl
• Faust2026.collapse x✝ ((s, some x_3) :: tl) = x_3 :: Faust2026.collapse (s == Morphology.CVSlot.V && Faust2026.collapses x_3 tl) tl

def Faust2026.truncate (p : Pattern) (m : Morphology.TemplateMatch String) : Morphology.CVTemplate

Truncation (7a) deletes the final syllable, the final C-slot and the V-slot before it, when the pattern truncates and that slot is vacant.

Equations

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

def Faust2026.realize (p : Pattern) (m : Morphology.TemplateMatch String) : List String

The surface segments of a match in a pattern are the realized slots, a filled prespecified geminate slot counting twice ({C C} in (7)), between the pattern's outer material.

Equations

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

def Faust2026.surface (p : Pattern) (r : Morphology.ConsonantalRoot String) : List String

The surface segments of a root in a pattern.

Equations

• Faust2026.surface p r = Faust2026.realize p (Faust2026.derive p r)

def Faust2026.surfaceChars (p : Pattern) (r : Morphology.ConsonantalRoot String) : List Char

The surface form as characters, for comparison with a transcription.

Equations

• Faust2026.surfaceChars p r = List.flatMap String.toList (Faust2026.surface p r)

The roots, in the squib's transcription

def Faust2026.klt : Morphology.ConsonantalRoot String

The root √klt of kalat 'received'.

Equations

• Faust2026.klt = { segments := ["k", "l", "t"] }

def Faust2026.kl : Morphology.ConsonantalRoot String

The root the biradical √kl of kalal 'included'.

Equations

• Faust2026.kl = { segments := ["k", "l"] }

def Faust2026.klj : Morphology.ConsonantalRoot String

The root √klj of kala 'roasted'.

Equations

• Faust2026.klj = { segments := ["k", "l", "j"] }

def Faust2026.dmj : Morphology.ConsonantalRoot String

The root √dmj of tadmit.

Equations

• Faust2026.dmj = { segments := ["d", "m", "j"] }

def Faust2026.glj : Morphology.ConsonantalRoot String

The root √glj of taglit.

Equations

• Faust2026.glj = { segments := ["g", "l", "j"] }

def Faust2026.rmj : Morphology.ConsonantalRoot String

The root √rmj of tarmit.

Equations

• Faust2026.rmj = { segments := ["r", "m", "j"] }

def Faust2026.skt : Morphology.ConsonantalRoot String

The root the t-final √skt of taskit.

Equations

• Faust2026.skt = { segments := ["s", "k", "t"] }

def Faust2026.sbr : Morphology.ConsonantalRoot String

The root Amharic √sbr 'break'.

Equations

• Faust2026.sbr = { segments := ["s", "b", "r"] }

def Faust2026.wd : Morphology.ConsonantalRoot String

The root Amharic √wd 'like'.

Equations

• Faust2026.wd = { segments := ["w", "d"] }

def Faust2026.fdj : Morphology.ConsonantalRoot String

The root Amharic √fdj 'scorch'.

Equations

• Faust2026.fdj = { segments := ["f", "d", "j"] }

def Faust2026.sma : Morphology.ConsonantalRoot String

The root Amharic √sma 'hear'.

Equations

• Faust2026.sma = { segments := ["s", "m", "a"] }

def Faust2026.sam : Morphology.ConsonantalRoot String

The root Amharic √sam 'kiss'.

Equations

• Faust2026.sam = { segments := ["s", "a", "m"] }

def Faust2026.hid : Morphology.ConsonantalRoot String

The root Amharic √hid 'go'.

Equations

• Faust2026.hid = { segments := ["h", "i", "d"] }

Modern Hebrew: the QaTaT–QaTa problem (3)–(4) and taQTiL (9)–(10)

def Faust2026.hebrewPst : Pattern

The PST.3MSG template CaCaC[+c] ((3)–(4)), vocalization a,a.

Equations

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

def Faust2026.hebrewQtila : Pattern

The action-noun template QTiLa (3).

Equations

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

def Faust2026.hebrewQatul : Pattern

The passive-participle template QaTuL (3).

Equations

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

def Faust2026.hebrewTaqtil : Pattern

The resultative nominal template taQTiL[+c] ((9)–(10)) has its fixed ta before the skeleton.

Equations

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

theorem Faust2026.klt_kl_satisfy : (derive hebrewPst klt).allCSlotsFilled ∧ ¬Misaligned (derive hebrewPst klt) ∧ (derive hebrewPst kl).allCSlotsFilled ∧ ¬Misaligned (derive hebrewPst kl) ∧ { melodyIndex := 1, slotIndex := 4 } ∈ (derive hebrewPst kl).associations

√klt fills CaCaC[+c] radical by radical, and the biradical √kl satisfies it by spreading its final l, QaTaT and never QaQaT, with no misalignment ((3a–b), (1)).

theorem Faust2026.klj_spread_misaligned : (derive hebrewPst klj).unfilledCSlots = [4] ∧ ¬Misaligned (derive hebrewPst klj) ∧ Misaligned ((derive hebrewPst klj).spread Morphology.AssocSource.root) ∧ realize hebrewPst ((derive hebrewPst klj).spread Morphology.AssocSource.root) = ["k", "a", "l", "a", "l"]

For √klj the [+c] final slot stays vacant; template satisfaction by spreading would yield [kalal] with the nonfinal l template-final, which *Misalignment rules out ((4), (6)).

theorem Faust2026.klj_qtila_qatul : (derive hebrewQtila klj).allCSlotsFilled ∧ (derive hebrewQatul klj).allCSlotsFilled

The final slots of QTiLa and QaTuL are unspecified, so j associates and surfaces (3c).

theorem Faust2026.dmj_taqtil : (associate hebrewTaqtil dmj).unfilledCSlots = [3] ∧ Misaligned ((associate hebrewTaqtil dmj).spread Morphology.AssocSource.root) ∧ { source := Morphology.AssocSource.affix, melodyIndex := 0, slotIndex := 3 } ∈ (derive hebrewTaqtil dmj).associations ∧ (derive hebrewTaqtil dmj).allCSlotsFilled ∧ ¬Misaligned (derive hebrewTaqtil dmj)

√dmj leaves the [+c] final slot of taQTiL vacant and spreading would misalign; merged with the feminine morph, whose t associates from the right, the template is satisfied without misalignment (10).

Amharic: (5), (7)–(8), (12)–(13)

def Faust2026.amharicPfv : Pattern

The type A PFV.3MSG stem CäCCäC[+c] ((5), (7)) has its medial C prespecified geminate, its final slot [+c] and the person suffix -ä outside; a barred glide joins the consonant on its left, and an unsatisfied final syllable is truncated (7a).

Equations

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

def Faust2026.amharicGrnd : Pattern

The GRND stem CäCC[+c] with the subject suffix -o ((5), (8)).

Equations

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

def Faust2026.amharicInf : Pattern

The INF has the prefix mä- and, in Strict CV terms (13), the skeleton CVC[+c]VC[+c] with ä on the second V-slot.

Equations

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

theorem Faust2026.fdj_pfv : { melodyIndex := 2, slotIndex := 2 } ∈ (derive amharicPfv fdj).associations ∧ (derive amharicPfv fdj).unfilledCSlots = [4] ∧ ¬Misaligned (derive amharicPfv fdj) ∧ Misaligned ((derive amharicPfv fdj).spread Morphology.AssocSource.root)

In the PFV the barred j of √fdj joins d at the geminate slot and the final slot stays vacant, with no misalignment; spreading d there would misalign (7).

theorem Faust2026.wd_pfv : (derive amharicPfv wd).allCSlotsFilled ∧ ¬Misaligned (derive amharicPfv wd) ∧ wd.IsOCPClean ∧ ¬{ segments := ["w", "d", "d"] }.IsOCPClean

The biradical √wd satisfies the PFV template by spreading its final d without misalignment and is OCP-clean, while [Bro84]'s √wdd is not (5b).

theorem Faust2026.fdj_grnd : { source := Morphology.AssocSource.affix, melodyIndex := 0, slotIndex := 3 } ∈ (derive amharicGrnd fdj).associations ∧ (derive amharicGrnd fdj).allCSlotsFilled ∧ ¬Misaligned (derive amharicGrnd fdj) ∧ Autosegmental.IsNonCrossing (melodyLinks (derive amharicGrnd fdj))

In the GRND the intruder fills the vacant final slot, satisfying the template without misalignment (8).

theorem Faust2026.inf_intrusion : (associate amharicInf sma).unfilledCSlots = [4] ∧ (associate amharicInf sam).unfilledCSlots = [2] ∧ (associate amharicInf hid).unfilledCSlots = [2] ∧ { source := Morphology.AssocSource.affix, melodyIndex := 0, slotIndex := 4 } ∈ (derive amharicInf sma).associations ∧ 2 ∉ Autosegmental.window (melodyLinks (associate amharicInf sam)) sam.arity ∧ 2 ∉ Autosegmental.window (melodyLinks (associate amharicInf hid)) hid.arity ∧ (derive amharicInf sam).unfilledCSlots = [2] ∧ (derive amharicInf hid).unfilledCSlots = [2] ∧ ¬Misaligned (derive amharicInf sam) ∧ ¬Misaligned (derive amharicInf hid)

All three INF derivations leave a C-slot vacant, but the intruder associates only in (13a), where the vacancy is final; in (13b–c) its line to the medial vacancy would cross the final radical's, so it floats, and no representation is misaligned.

The paradigms (3), (5), (12) and the nouns (9)

inductive Faust2026.Lang : Type

The languages of the rows.

• hebrew : Lang
• amharic : Lang

@[instance_reducible]

instance Faust2026.instDecidableEqLang : DecidableEq Lang

Equations

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

@[instance_reducible]

instance Faust2026.instReprLang : Repr Lang

Equations

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

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

Equations

• Faust2026.instReprLang.repr Faust2026.Lang.hebrew prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Lang.hebrew")).group prec✝
• Faust2026.instReprLang.repr Faust2026.Lang.amharic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Lang.amharic")).group prec✝

inductive Faust2026.Cell : Type

The paradigm cells of (3), (5), (12).

• pst3msg : Cell
• actionNoun : Cell
• passPrtc : Cell
• pfv : Cell
• ipfv : Cell
• juss : Cell
• grnd : Cell
• inf : Cell

@[instance_reducible]

instance Faust2026.instDecidableEqCell : DecidableEq Cell

Equations

• Faust2026.instDecidableEqCell x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Faust2026.instReprCell.repr : Cell → ℕ → Std.Format

Equations

• Faust2026.instReprCell.repr Faust2026.Cell.pst3msg prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.pst3msg")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.actionNoun prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.actionNoun")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.passPrtc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.passPrtc")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.pfv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.pfv")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.ipfv prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.ipfv")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.juss prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.juss")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.grnd prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.grnd")).group prec✝
• Faust2026.instReprCell.repr Faust2026.Cell.inf prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Faust2026.Cell.inf")).group prec✝

@[instance_reducible]

instance Faust2026.instReprCell : Repr Cell

Equations

• Faust2026.instReprCell = { reprPrec := Faust2026.instReprCell.repr }

def Faust2026.Cell.pattern? : Cell → Option Pattern

The pattern of a cell, for the cells the squib draws.

Equations

• Faust2026.Cell.pst3msg.pattern? = some Faust2026.hebrewPst
• Faust2026.Cell.actionNoun.pattern? = some Faust2026.hebrewQtila
• Faust2026.Cell.passPrtc.pattern? = some Faust2026.hebrewQatul
• Faust2026.Cell.pfv.pattern? = some Faust2026.amharicPfv
• Faust2026.Cell.grnd.pattern? = some Faust2026.amharicGrnd
• Faust2026.Cell.inf.pattern? = some Faust2026.amharicInf
• Faust2026.Cell.ipfv.pattern? = none
• Faust2026.Cell.juss.pattern? = none

def Faust2026.Cell.IsNominal (c : Cell) : Prop

The cells with a nominal base are the Amharic GRND and INF, whose subjects are marked as possessors (§4.2), and the Hebrew action noun.

Equations

• c.IsNominal = (Option.map Faust2026.Pattern.category c.pattern? = some Faust2026.Category.noun)

@[instance_reducible]

instance Faust2026.instDecidableIsNominal (c : Cell) : Decidable c.IsNominal

Equations

• Faust2026.instDecidableIsNominal c = Faust2026.instDecidableIsNominal._aux_1 c

structure Faust2026.Row : Type

A paradigm cell of a root.

• lang : Lang
• root : Morphology.ConsonantalRoot String
• cell : Cell
• form : String

def Faust2026.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Faust2026.instDecidableEqRow : DecidableEq Row

Equations

• Faust2026.instDecidableEqRow = Faust2026.instDecidableEqRow.decEq

def Faust2026.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Faust2026.instReprRow : Repr Row

Equations

• Faust2026.instReprRow = { reprPrec := Faust2026.instReprRow.repr }

structure Faust2026.NounRow : Type

A taQTiL noun (9), with its root where the squib identifies it.

• form : String
• gender : Gender
• root : Option (Morphology.ConsonantalRoot String)

@[instance_reducible]

instance Faust2026.instDecidableEqNounRow : DecidableEq NounRow

Equations

• Faust2026.instDecidableEqNounRow = Faust2026.instDecidableEqNounRow.decEq

def Faust2026.instDecidableEqNounRow.decEq (x✝ x✝¹ : NounRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Faust2026.instReprNounRow : Repr NounRow

Equations

• Faust2026.instReprNounRow = { reprPrec := Faust2026.instReprNounRow.repr }

def Faust2026.instReprNounRow.repr : NounRow → ℕ → Std.Format

Equations

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

def Faust2026.langTable : List (String × Lang)

Equations

• Faust2026.langTable = [("hebr1245", Faust2026.Lang.hebrew), ("amha1245", Faust2026.Lang.amharic)]

def Faust2026.rootTable : List (String × Morphology.ConsonantalRoot String)

Equations

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

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

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

Equations

• Faust2026.segment Faust2026.Lang.hebrew "k" = Hebrew.Phonology.k
• Faust2026.segment Faust2026.Lang.hebrew "l" = Hebrew.Phonology.l
• Faust2026.segment Faust2026.Lang.hebrew "t" = Hebrew.Phonology.t
• Faust2026.segment Faust2026.Lang.hebrew "j" = Hebrew.Phonology.j
• Faust2026.segment Faust2026.Lang.hebrew "d" = Hebrew.Phonology.d
• Faust2026.segment Faust2026.Lang.hebrew "m" = Hebrew.Phonology.m
• Faust2026.segment Faust2026.Lang.hebrew "g" = Hebrew.Phonology.«ɡ»
• Faust2026.segment Faust2026.Lang.hebrew "r" = Hebrew.Phonology.«ʁ»
• Faust2026.segment Faust2026.Lang.hebrew "s" = Hebrew.Phonology.s
• Faust2026.segment Faust2026.Lang.amharic "s" = Amharic.Phonology.s
• Faust2026.segment Faust2026.Lang.amharic "b" = Amharic.Phonology.b
• Faust2026.segment Faust2026.Lang.amharic "r" = Amharic.Phonology.«ɾ»
• Faust2026.segment Faust2026.Lang.amharic "w" = Amharic.Phonology.w
• Faust2026.segment Faust2026.Lang.amharic "d" = Amharic.Phonology.d
• Faust2026.segment Faust2026.Lang.amharic "f" = Amharic.Phonology.f
• Faust2026.segment Faust2026.Lang.amharic "j" = Amharic.Phonology.j
• Faust2026.segment Faust2026.Lang.amharic "m" = Amharic.Phonology.m
• Faust2026.segment Faust2026.Lang.amharic "a" = Amharic.Phonology.a
• Faust2026.segment Faust2026.Lang.amharic "h" = Amharic.Phonology.h
• Faust2026.segment Faust2026.Lang.amharic "i" = Amharic.Phonology.i
• Faust2026.segment x✝¹ x✝ = ⊥

theorem Faust2026.fragment_roots : List.map (fun (x : Morphology.ConsonantalRoot Phonology.Segment) => Morphology.ConsonantalRoot.map (Arad2005.fillContinuant false) x) [Hebrew.klt, Hebrew.kl, Hebrew.klj, Hebrew.dmj, Hebrew.glj, Hebrew.rmj, Hebrew.skt] = List.map (fun (x : Morphology.ConsonantalRoot String) => Morphology.ConsonantalRoot.map (segment Lang.hebrew) x) [klt, kl, klj, dmj, glj, rmj, skt] ∧ [Amharic.sbr, Amharic.wd, Amharic.fdj, Amharic.sma, Amharic.sam, Amharic.hid] = List.map (fun (x : Morphology.ConsonantalRoot String) => Morphology.ConsonantalRoot.map (segment Lang.amharic) x) [sbr, wd, fdj, sma, sam, hid]

The squib's roots, read as segments, are the fragments' roots, the Hebrew alternating stops of √kl and √skt realized as the stops the squib writes.

def Faust2026.cellTable : List (String × Cell)

Equations

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

def Faust2026.genderTable : List (String × Gender)

Equations

• Faust2026.genderTable = [("masculine", Gender.masculine), ("feminine", Gender.feminine)]

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

Equations

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

def Faust2026.NounRow.ofDatum (ex : Datum) : Option NounRow

Equations

• Faust2026.NounRow.ofDatum ex = do let gender ← ex.parse? "gender" Faust2026.genderTable pure { form := ex.primaryText, gender := gender, root := ex.parse? "root" Faust2026.rootTable }

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

def Faust2026.rows : List Row

Equations

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

def Faust2026.nounRows : List NounRow

Equations

• Faust2026.nounRows = List.filterMap Faust2026.NounRow.ofDatum Faust2026.Examples.all

def Faust2026.Row.surface? (r : Row) : Option (List Char)

The surface form the pipeline derives for a row, where its cell has a pattern.

Equations

• r.surface? = Option.map (fun (x : Faust2026.Pattern) => Faust2026.surfaceChars x r.root) r.cell.pattern?

theorem Faust2026.rows_surface (r : Row) : r ∈ rows → r.cell.pattern?.isSome = true → (r.root, r.cell) ≠ (sma, Cell.pfv) → r.surface? = some r.form.toList

The pipeline reproduces every cell of (3), (5), (12) that has a pattern, except the PFV of √sma, where the final radical merges with the suffix vowel.

theorem Faust2026.j_surfaces (r : Row) : r ∈ rows → r.lang = Lang.hebrew → ('j' ∈ r.form.toList ↔ r.root = klj ∧ r.cell ≠ Cell.pst3msg)

The final j of √klj surfaces in the action noun and the passive participle and not in the PST.3MSG (3).

def Faust2026.BarredFinal (r : Morphology.ConsonantalRoot String) : Prop

A root's final radical is barred from a [+c] slot when it is a glide, as in √klj and √fdj, or a vowel, as in √sma.

Equations

• Faust2026.BarredFinal r = match r.finalSegment with | some x => Faust2026.segClass x ≠ Faust2026.SegClass.consonant | none => False

@[instance_reducible]

instance Faust2026.instDecidableBarredFinal (r : Morphology.ConsonantalRoot String) : Decidable (BarredFinal r)

Equations

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

theorem Faust2026.intruder_distribution (r : Row) : r ∈ rows → r.lang = Lang.amharic → ('t' ∈ r.form.toList ∧ "t" ∉ r.root.segments ↔ r.cell.IsNominal ∧ BarredFinal r.root)

Across the Amharic paradigms (5) and (12), a nonradical [t] occurs exactly in the nominal cells of the roots whose final radical is barred — the distribution [Bro84]'s default consonant leaves unexplained (§2.2) and the suffix analysis derives (§4.2).

theorem Faust2026.masculine_of_not_t_final (r : NounRow) : r ∈ nounRows → r.form.toList.getLast? ≠ some 't' → r.gender = Gender.masculine

A taQTiL noun whose last consonant is not [t] is masculine (9).

def Faust2026.NounRow.Derived (r : NounRow) : Prop

The taQTiL derivation of a noun's root reproduces the noun, and the noun is feminine iff the derivation merged the feminine morph, so [taskit] from t-final √skt is masculine and the nouns from j-final roots feminine (9b).

Equations

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

@[instance_reducible]

instance Faust2026.instDecidableDerived (r : NounRow) : Decidable r.Derived

Equations

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

theorem Faust2026.nounRows_derived (r : NounRow) : r ∈ nounRows → r.Derived