Faust (2026) — Intrusion as Template Satisfaction

[Fau26] [McC81] [Bro84] [Low96] [Low14] [Kra20]

Faust, Noam. 2026. Intrusion as template satisfaction and the QaTaT–QaTa problem in Semitic. Linguistic Inquiry 57(2): 427–441. https://doi.org/10.1162/ling_a_00524

Core contribution

A single alignment principle, *Misalignment — "a nonfinal root element must not be template-final" ([Fau26] (2)/(6b)) — jointly resolves three Semitic puzzles:

1. The QaTaT–QaTa gap (Modern Hebrew). Triradical [j]-final roots like √klj roast would be predicted by template satisfaction ([McC81]) to fill the [+c]-specified template-final slot via spreading of the medial radical /l/, yielding *[kalal]. They surface instead as [kala] with an unfilled C-slot ([Fau26] (3c), (4)). *Misalignment derives this: spreading /l/ to template-final would put a nonfinal root element in template-final position. The grammar tolerates an unfilled C-slot rather than violate *Misalignment.

2. Amharic [t]-intrusion ([Bro84]). The [t] in Amharic gerund [fädʤto] and INF forms is reanalyzed not as a default consonant inserted to satisfy the template ([Bro84]), but as the feminine /t/ — the n[+gen] exponent realized as a sister bound root in the sense of [Low14] — which satisfies the template without being a nonfinal root segment, hence not violating *Misalignment. The strategy is unavailable for verbal forms because gender markers are inherent on n, not contextual on Agr ([Fau26] (11) — connects to [Kra20]).

3. Apparent OCP-violating Amharic biradicals are reanalyzed. [Bro84] concluded that Amharic admits OCP-violating √TT roots like √dd for [wäddäd-ä] liked. [Fau26] (page 432) shows: once scorch-type verbs are reanalyzed as triradical (√fdj, not biradical √fd), there is no remaining reason to posit OCP-violating roots. The [wäddäd-ä] form is based on biradical √wd, where /w/ ≠ /d/ — the surface gemination is a template-spreading effect, and *Misalignment is satisfied because the spread /d/ is the final root segment.

Architectural integration

This file consumes and exercises the shared infrastructure:

• Morphology.Root — polymorphic consonantal-root carrier.
• Faust2026.Templates (defined above in this file) — CVSlot, Template, Association, RootTemplateMatch, with derived isMisaligned, allCSlotsFilled, satisfies.
• Faust2026.Templates.starMisalign — the *Misalignment alignment constraint, built via the generic Constraint.binary constructor.
• OptimalityTheory.adjacentIdentical — drives the root-level OCP, used to verify [Fau26]'s OCP-related reanalysis.

Per-derivation decide theorems test all four combinations of isMisaligned ∈ {true, false} × allCSlotsFilled ∈ {true, false}, making the central squib claim — Misalignment-violating candidates are blocked even when they satisfy the template — visible at the type level rather than restated in prose.

inductive Faust2026.Templates.CVSlot : Type

A slot in a CV-skeletal template ([McC81], [Low96]):

• C: a bare consonantal timing slot.
• V: a vowel timing slot.
• Cspec: a C-slot bearing the [+consonantal] feature, blocking association from glides like /j/ — this is the slot type that triggers the QaTaT–QaTa problem when paired with a [j]-final root ([Fau26] (4)).

• C : CVSlot
• V : CVSlot
• Cspec : CVSlot

@[implicit_reducible]

instance Faust2026.Templates.instDecidableEqCVSlot : DecidableEq CVSlot

Equations

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

@[implicit_reducible]

instance Faust2026.Templates.instReprCVSlot : Repr CVSlot

Equations

• Faust2026.Templates.instReprCVSlot = { reprPrec := Faust2026.Templates.instReprCVSlot.repr }

def Faust2026.Templates.instReprCVSlot.repr : CVSlot → ℕ → Std.Format

Equations

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

def Faust2026.Templates.CVSlot.IsC : CVSlot → Prop

Is this slot a C-slot (bare or [+c]-specified)?

Equations

• Faust2026.Templates.CVSlot.C.IsC = True
• Faust2026.Templates.CVSlot.Cspec.IsC = True
• Faust2026.Templates.CVSlot.V.IsC = False

@[implicit_reducible]

instance Faust2026.Templates.CVSlot.instDecidablePredIsC : DecidablePred IsC

Equations

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

def Faust2026.Templates.CVSlot.IsV : CVSlot → Prop

Is this slot a V-slot?

Equations

• Faust2026.Templates.CVSlot.V.IsV = True
• x✝.IsV = False

@[implicit_reducible]

instance Faust2026.Templates.CVSlot.instDecidablePredIsV : DecidablePred IsV

Equations

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

def Faust2026.Templates.CVSlot.RequiresConsonantal : CVSlot → Prop

Does this slot require a [+consonantal] segment?

Equations

• Faust2026.Templates.CVSlot.Cspec.RequiresConsonantal = True
• x✝.RequiresConsonantal = False

@[implicit_reducible]

instance Faust2026.Templates.CVSlot.instDecidablePredRequiresConsonantal : DecidablePred RequiresConsonantal

Equations

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

structure Faust2026.Templates.Template : Type

A CV-skeletal template: an ordered sequence of slots.

• slots : List CVSlot

@[implicit_reducible]

instance Faust2026.Templates.instReprTemplate : Repr Template

Equations

• Faust2026.Templates.instReprTemplate = { reprPrec := Faust2026.Templates.instReprTemplate.repr }

def Faust2026.Templates.instReprTemplate.repr : Template → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Faust2026.Templates.instDecidableEqTemplate : DecidableEq Template

Equations

• Faust2026.Templates.instDecidableEqTemplate = Faust2026.Templates.instDecidableEqTemplate.decEq

def Faust2026.Templates.instDecidableEqTemplate.decEq (x✝ x✝¹ : Template) : Decidable (x✝ = x✝¹)

Equations

• Faust2026.Templates.instDecidableEqTemplate.decEq { slots := a } { slots := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Faust2026.Templates.Template.length (t : Template) : ℕ

The number of slots in the template.

Equations

• t.length = t.slots.length

def Faust2026.Templates.Template.cCount (t : Template) : ℕ

The number of C-slots (consonant timing positions).

Equations

• t.cCount = (List.filter (fun (s : Faust2026.Templates.CVSlot) => decide s.IsC) t.slots).length

@[reducible, inline]

abbrev Faust2026.Templates.Template.isFinalSlot (t : Template) (i : ℕ) : Prop

Slot i is the final slot of the template.

Equations

• t.isFinalSlot i = (i + 1 = t.length)

def Faust2026.Templates.Template.slotAt (t : Template) (i : ℕ) : Option CVSlot

The slot at position i, if in range.

Equations

• t.slotAt i = t.slots[i]?

inductive Faust2026.Templates.AssocSource : Type

The morphological source of an association.

Faust 2026's analysis turns on this distinction: a .root association is subject to *Misalignment, an .intruder association is not. Intruders are sister exponents (e.g. the feminine [t] in Hebrew taQTiL nouns, [Fau26] (10)) that satisfy the template without being root segments themselves.

• root : AssocSource
• intruder : AssocSource

@[implicit_reducible]

instance Faust2026.Templates.instDecidableEqAssocSource : DecidableEq AssocSource

Equations

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

def Faust2026.Templates.instReprAssocSource.repr : AssocSource → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Faust2026.Templates.instReprAssocSource : Repr AssocSource

Equations

• Faust2026.Templates.instReprAssocSource = { reprPrec := Faust2026.Templates.instReprAssocSource.repr }

structure Faust2026.Templates.Association : Type

A single root-to-slot association line ([McC81]).

rootIndex is interpreted relative to the root for .root associations, or as an opaque tag for .intruder associations (intruder identity is handled at the fragment level — this module is segment-agnostic).

Defaults to .root so that "ordinary" associations stay terse.

• source : AssocSource
• rootIndex : ℕ
• slotIndex : ℕ

def Faust2026.Templates.instDecidableEqAssociation.decEq (x✝ x✝¹ : Association) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Faust2026.Templates.instDecidableEqAssociation : DecidableEq Association

Equations

• Faust2026.Templates.instDecidableEqAssociation = Faust2026.Templates.instDecidableEqAssociation.decEq

def Faust2026.Templates.instReprAssociation.repr : Association → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Faust2026.Templates.instReprAssociation : Repr Association

Equations

• Faust2026.Templates.instReprAssociation = { reprPrec := Faust2026.Templates.instReprAssociation.repr }

structure Faust2026.Templates.RootTemplateMatch (α : Type) : Type

A root paired with a template and a list of associations.

Different candidate realizations of the same root × template pair are different RootTemplateMatch values that share root and template but differ in associations. The Faust 2026 analysis compares such candidates via the derived isMisaligned predicate.

• root : Morphology.Root α
• template : Template
• associations : List Association

@[implicit_reducible]

instance Faust2026.Templates.instReprRootTemplateMatch {α✝ : Type} [Repr α✝] : Repr (RootTemplateMatch α✝)

Equations

• Faust2026.Templates.instReprRootTemplateMatch = { reprPrec := Faust2026.Templates.instReprRootTemplateMatch.repr }

def Faust2026.Templates.instReprRootTemplateMatch.repr {α✝ : Type} [Repr α✝] : RootTemplateMatch α✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Faust2026.Templates.instDecidableEqRootTemplateMatch {α✝ : Type} [DecidableEq α✝] : DecidableEq (RootTemplateMatch α✝)

Equations

• Faust2026.Templates.instDecidableEqRootTemplateMatch = Faust2026.Templates.instDecidableEqRootTemplateMatch.decEq

def Faust2026.Templates.instDecidableEqRootTemplateMatch.decEq {α✝ : Type} [DecidableEq α✝] (x✝ x✝¹ : RootTemplateMatch α✝) : Decidable (x✝ = x✝¹)

Equations

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

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.isRootFinal {α : Type} (m : RootTemplateMatch α) (a : Association) : Prop

An association is a root-to-final link iff it comes from the root proper and lands at the template-final slot.

Equations

• m.isRootFinal a = (a.source = Faust2026.Templates.AssocSource.root ∧ m.template.isFinalSlot a.slotIndex)

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.isMisaligned {α : Type} (m : RootTemplateMatch α) : Prop

Misalignment ([Fau26] (2)): the match has a nonfinal root segment associated to the template-final slot. Intruder associations do not count — see AssocSource.

Equations

• m.isMisaligned = ∃ a ∈ m.associations, a.source = Faust2026.Templates.AssocSource.root ∧ m.root.isNonfinal a.rootIndex = true ∧ m.template.isFinalSlot a.slotIndex

def Faust2026.Templates.RootTemplateMatch.unfilledCSlots {α : Type} (m : RootTemplateMatch α) : List ℕ

The list of C-slot indices that are NOT filled by any association. Used by hollow-root analyses ([Fau26] (13)): when the medial radical is non-consonantal, the medial C-slot is unfilled, and the position of the unfilled slot determines whether [t]-intrusion is licensed (final-empty: licit; medial-empty: blocked by the No-Crossing Constraint).

Equations

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

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.allCSlotsFilled {α : Type} (m : RootTemplateMatch α) : Prop

Every C-slot of the template is filled by some association (root or intruder) — equivalently, no C-slot is left unfilled.

Equations

• m.allCSlotsFilled = (m.unfilledCSlots = [])

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.satisfies {α : Type} (m : RootTemplateMatch α) : Prop

The template is satisfied iff all C-slots are filled and the result is not misaligned. The two requirements are independent — the central point of [Fau26] is that for [j]-final biradicals in Hebrew, one cannot satisfy the first without violating the second.

Equations

• m.satisfies = (m.allCSlotsFilled ∧ ¬m.isMisaligned)

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.inBounds {α : Type} (m : RootTemplateMatch α) : Prop

Every association points to an in-range root segment and slot.

Equations

• m.inBounds = ∀ a ∈ m.associations, a.slotIndex < m.template.length ∧ (a.source = Faust2026.Templates.AssocSource.root → a.rootIndex < m.root.arity)

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.violatesNCC {α : Type} (m : RootTemplateMatch α) : Prop

The No-Crossing Constraint ([Gol76]): an intruder association at slot i crosses an existing association at slot j > i. Right-edge intruders (e.g. the feminine /t/ suffix in Hebrew taQTiL and Amharic gerunds) associate inward from the right, so any root segment to the right of the intruder forces line-crossing.

This is the predicate that explains [Fau26] (13b–c): [t]-intrusion does not fill the medial C[+c] of [mäsam]/[mähid] because the final C-slot is already filled by the final root radical, so an intruder at the medial position would have to cross the final root association line.

Equations

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

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.hasIntruder {α : Type} (m : RootTemplateMatch α) : Prop

Does this match contain any intruder associations? Templates without intruders are licit in any morphosyntactic context (verbal or nominal); templates with intruders require external licensing — see intrusionLicensed.

Equations

• m.hasIntruder = ∃ a ∈ m.associations, a.source = Faust2026.Templates.AssocSource.intruder

@[reducible, inline]

abbrev Faust2026.Templates.RootTemplateMatch.intrusionLicensed {α : Type} (m : RootTemplateMatch α) (licensed : Bool) : Prop

A RootTemplateMatch is intrusion-licensed under an external licensing predicate iff either (a) the predicate is true (the morphosyntactic context licenses an intruding sister bound root, à la [Low14]), or (b) the match contains no intruder associations.

The licensing predicate is supplied by the morphological theory above — for [Fau26]'s analysis, it evaluates to true iff the template is realized at an n[+gen] head in [Kra20]'s sense (verbal templates, whose gender lives on a higher Agr head, evaluate to false and so admit no intrusion). The predicate is Bool-valued (an external licensing flag) rather than a MorphologicalLocus enum, keeping the template layer independent of any particular categorizer taxonomy.

Equations

• m.intrusionLicensed licensed = (licensed = true ∨ ¬m.hasIntruder)

theorem Faust2026.Templates.not_isMisaligned_empty {α : Type} (r : Morphology.Root α) (t : Template) : ¬{ root := r, template := t, associations := [] }.isMisaligned

A match with no associations is trivially not misaligned.

theorem Faust2026.Templates.not_isMisaligned_of_all_intruder {α : Type} (r : Morphology.Root α) (t : Template) (assocs : List Association) (h : ∀ a ∈ assocs, a.source = AssocSource.intruder) : ¬{ root := r, template := t, associations := assocs }.isMisaligned

*Misalignment cannot fire from intruder associations alone.

theorem Faust2026.Templates.intrusionLicensed_iff {α : Type} (m : RootTemplateMatch α) (licensed : Bool) : m.intrusionLicensed licensed ↔ licensed = true ∨ ¬m.hasIntruder

The Prop predicates isMisaligned, violatesNCC, and satisfies are now stated directly as the existential / conjunctive characterizations that the squib's argument relies on, so no separate _iff lemmas are needed: satisfies is by definition allCSlotsFilled ∧ ¬ isMisaligned.

Structural characterization of intrusionLicensed: a match passes licensing iff either the external predicate licenses intrusion OR the match is intruder-free. The disjunction is the formal content of the verbal/nominal asymmetry — verbal templates require intruder-free derivations; nominal templates with n[+gen] admit either.

theorem Faust2026.Templates.intrusionLicensed_of_no_intruder {α : Type} (m : RootTemplateMatch α) (h : ¬m.hasIntruder) (licensed : Bool) : m.intrusionLicensed licensed

Intruder-free matches are licensed in any morphosyntactic context.

theorem Faust2026.Templates.intrusionLicensed_with_intruder {α : Type} (m : RootTemplateMatch α) (h : m.hasIntruder) (licensed : Bool) : m.intrusionLicensed licensed ↔ licensed = true

An intruder-bearing match is licensed iff the external predicate is true — the contrapositive that delivers the verbal/nominal split.

def Faust2026.Templates.starMisalign {α : Type} : Constraints.Constraint (RootTemplateMatch α)

The *Misalignment constraint of [Fau26] (2): a markedness constraint that fires on RootTemplateMatch candidates whose isMisaligned predicate holds. Built via the generic Constraint.binary constructor from Constraints.

Equations

• Faust2026.Templates.starMisalign = Constraints.Constraint.binary Faust2026.Templates.RootTemplateMatch.isMisaligned

def Faust2026.Templates.fill {α : Type} : Constraints.Constraint (RootTemplateMatch α)

The FILL constraint ([PS93]): a markedness constraint penalizing unfilled C-slots in the template. Used by [Fau26]'s implicit ranking *Misalign >> FILL: spreading a nonfinal root segment to a final [+c] slot satisfies FILL but violates *Misalign, and the grammar prefers the FILL-violating candidate.

Equations

• Faust2026.Templates.fill = Constraints.Constraint.binary fun (m : Faust2026.Templates.RootTemplateMatch α) => ¬m.allCSlotsFilled

def Faust2026.Templates.noCross {α : Type} : Constraints.Constraint (RootTemplateMatch α)

NoCross ([Gol76]): a markedness constraint penalizing candidates whose intruder associations cross root associations.

Equations

• Faust2026.Templates.noCross = Constraints.Constraint.binary fun (m : Faust2026.Templates.RootTemplateMatch α) => m.violatesNCC

def Faust2026.hebrewPst3msg : Templates.Template

The Hebrew PST.3MSG verbal template CaCaC[+c] ([Fau26] (1), (3a–c), (4)). Five slots; the final C-slot is [+consonantal], blocking association from the glide /j/.

Equations

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

def Faust2026.hebrewPassPrtcpl : Templates.Template

The Hebrew passive-participle template CaCuC ([Fau26] (3c) discussion). Five slots; the final C-slot is not [+c]-specified, so the glide /j/ associates to it freely (yielding [kaluj], [tʃamuj]).

Equations

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

def Faust2026.hebrewTaQTiL : Templates.Template

The Hebrew nominal template taQTiL[+c] ([Fau26] (9)–(10)): six slots C V C C V C[+c]. The first C V (= "ta") is realized by the n[+gen]-internal /t/ exponent and template vocalization; the medial C C hosts the first two root radicals; the final C[+c] is the slot that hosts the intruding feminine /t/ in the feminine-noun reading ([Fau26] (10b–c)).

Equations

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

def Faust2026.amharicPfv3msg : Templates.Template

The Amharic PFV.3MSG verbal template (type-A pattern CäC.CäC[+c], [Fau26] (5), (7)). Six slots C V C C V C[+c]; the medial geminate C C is the position where Amharic spreads its second radical, and the final C-slot is [+c]. The verbal -ä person-marking suffix attaches outside this template.

Equations

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

def Faust2026.amharicGrnd : Templates.Template

The Amharic gerund template CäC.C[+c]-o ([Fau26] (8)). Five slots: the final V hosts the gerund [-o] suffix; the penult C[+c] is where the [t]-intruder lands when the root is [j]-final.

Equations

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

The three-way QaTaT–QaTa contrast ([Fau26] (3))

[Fau26] (3) presents three Modern Hebrew verbs sharing the same CaCaC[+c] template:

• (3a) [kalat] from √klt — full triradical, all radicals surface.
• (3b) [kalal] from √kll — final radical /l/ spreads/associates to template-final; legitimate because the spreading segment IS the final root segment (no *Misalignment violation).
• (3c) [kala] from √klj — analogous spreading would put nonfinal /l/ at template-final; *Misalignment blocks it, so the [+c] slot is left unfilled and the surface form has only two consonants.

The squib's analytical move: (3b) and (3c) look superficially identical — both would (or do) involve the medial radical surfacing in the final position — but *Misalignment discriminates by which root index the template-final segment came from.

def Faust2026.hebrewKlt_kalat : Templates.RootTemplateMatch String

(3a) [kalat] from √klt: full triradical control case. Every root segment associates to a distinct template C-slot; no spreading, no misalignment.

Equations

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

def Faust2026.hebrewKll_kalal : Templates.RootTemplateMatch String

(3b) [kalal] from √kll: the attested QaTaT pattern. The final /l/ at root index 2 associates to template-final C[+c]; this is the final-of-final case and *Misalignment is satisfied.

Equations

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

def Faust2026.hebrewKlj_kalal : Templates.RootTemplateMatch String

Candidate (4) of [Fau26]: the spreading derivation of *[kalal] from √klj + CaCaC[+c]. The medial /l/ at root index 1 is spread to the [+c] template-final slot (template index 4). This is the candidate template satisfaction predicts; [Fau26] (4) shows it is ruled out by *Misalignment.

Equations

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

def Faust2026.hebrewKlj_kala : Templates.RootTemplateMatch String

The actual surface form [kala] ([Fau26] (3c)): only /k/ and /l/ associate; the [+c] template-final slot is left unfilled because /j/ cannot satisfy [+c] and spreading /l/ would violate *Misalignment. The grammar tolerates the unfilled C-slot.

Equations

• Faust2026.hebrewKlj_kala = { root := Hebrew.klj, template := Faust2026.hebrewPst3msg, associations := [{ rootIndex := 0, slotIndex := 0 }, { rootIndex := 1, slotIndex := 2 }] }

def Faust2026.hebrewKlj_kaluj : Templates.RootTemplateMatch String

The passive participle [kaluj] ([Fau26] (3c)): /j/ surfaces because the final C-slot is not [+c]-specified, so direct association succeeds and no spreading is required — *Misalignment trivially satisfied, all C-slots filled.

Equations

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

def Faust2026.hebrewDmj_illicit : Templates.RootTemplateMatch String

The illicit derivation ([Fau26] (10a)): √dmj associated directly to taQTiL[+c]. The prefix /t/ fills C0 (intruder, since it belongs to the template-internal "ta" exponent rather than √dmj), the root /d/ and /m/ fill C2 and C3 respectively, and to fill the [+c] final slot we attempt to spread /m/ — but /m/ is nonfinal in √dmj, so this violates *Misalignment.

Equations

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

def Faust2026.hebrewDmj_tadmit : Templates.RootTemplateMatch String

The licit [tadmit] derivation ([Fau26] (10b–c)): the feminine n[+gen] exponent /t/ is added as a sister bound root, and its /t/ associates from the right to the [+c] final C-slot. Both the prefix /t/ at C0 and the suffix /t/ at C5 are intruder associations (not part of √dmj), so *Misalignment doesn't fire on either; the root /d/ and /m/ occupy nonfinal C-slots.

Equations

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

def Faust2026.amharicFdj_pfv : Templates.RootTemplateMatch String

Amharic [fädʤ-ä] PFV.3MSG: √fdj in CäC.CäC[+c]. Following [Fau26] (7a) with truncation: /f/ → C0, /d/ → C2 (and spreads to C3 for gemination), /j/ has no slot — its palatality merges with the preceding /d/ to yield [dʒ], and the penult V plus final C[+c] are truncated in the surface form. The unfilled final C-slot is precisely what the squib's analysis predicts.

Equations

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

def Faust2026.amharicFdj_grnd : Templates.RootTemplateMatch String

Amharic gerund [fädʤto] ([Fau26] (8)): the feminine /t/ intruder fills the [+c] penult slot, and the final V slot hosts the gerund [-o] suffix. Because /t/ is an intruder (not a root segment), *Misalignment does not block it.

Equations

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

def Faust2026.amharicWd_pfv : Templates.RootTemplateMatch String

Amharic [wäddäd-ä] liked PFV.3MSG: √wd is biradical ([Fau26] page 432). /w/ → C0; /d/ → C2 (and spreads to C3 for gemination, and to C[+c]5 to fill the final slot). The spread of /d/ to template-final is licit under *Misalignment because /d/ is at root index 1, the final root segment of √wd — there is no nonfinal-to-final misalignment. This is the type-level demonstration that the surface contrast between [wäddäd-ä] (biradical, OK) and *[kalal] (triradical, blocked) falls out of *Misalignment alone, with no need for OCP-violating roots.

Equations

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

Hebrew QaTaT–QaTa ([Fau26] (3), (4))

theorem Faust2026.hebrew_kalat_satisfies : hebrewKlt_kalat.satisfies

(3a) [kalat] from √klt: the full-triradical control case satisfies everything — every C-slot filled, no *Misalignment.

theorem Faust2026.hebrew_kll_kalal_satisfies : hebrewKll_kalal.satisfies

(3b) [kalal] from √kll: the attested QaTaT pattern satisfies the template (every C-slot filled) AND respects *Misalignment, because the segment at template-final is /l/ at root index 2 — the final root segment, so no nonfinal-to-final misalignment fires.

theorem Faust2026.hebrew_kalal_misaligned : hebrewKlj_kalal.isMisaligned

(4) The spreading candidate *[kalal] from √klj is misaligned.

theorem Faust2026.hebrew_kala_not_misaligned : ¬hebrewKlj_kala.isMisaligned

(3c) The empty-slot candidate [kala] from √klj is not misaligned.

theorem Faust2026.hebrew_kalal_filled : hebrewKlj_kalal.allCSlotsFilled

Spreading would have satisfied the template — i.e., kalal fills every C-slot — but it violates *Misalignment. The squib's central argument is that this latter violation is decisive.

theorem Faust2026.hebrew_kala_unfilled : ¬hebrewKlj_kala.allCSlotsFilled

The empty-slot [kala] candidate violates the C-slot-filling requirement. The grammar tolerates this because every alternative violates *Misalignment. (See qataT_qata_three_way_contrast for the joint statement of the three-way fate.)

theorem Faust2026.hebrew_kaluj_satisfies : hebrewKlj_kaluj.satisfies

The passive participle [kaluj] is unproblematic on every dimension: final C-slot is not [+c]-specified, /j/ associates directly, no spreading required.

theorem Faust2026.qataT_qata_three_way_contrast : hebrewKlt_kalat.satisfies ∧ hebrewKll_kalal.satisfies ∧ hebrewKlj_kalal.allCSlotsFilled ∧ hebrewKlj_kalal.isMisaligned ∧ ¬hebrewKlj_kala.allCSlotsFilled ∧ ¬hebrewKlj_kala.isMisaligned

The full three-way contrast of [Fau26] (3): three roots, one template, three different fates determined by *Misalignment + [+c]-specification. The decisive feature is which root index sits at template-final:

• √klt: root-index 2 (= final). *Misalignment satisfied. ✓ [kalat]
• √kll: root-index 2 (= final, identical to medial). ✓ [kalal]
• √klj→l: root-index 1 (= nonfinal!). *Misalignment fires. ✗
• √klj→∅: no association at template-final. ✓ but C-slot empty: [kala]

The QaTaT–QaTa "puzzle" dissolves: superficially-identical surface patterns ([kalal] from √kll vs hypothetical [kalal] from √klj) have different root-template alignments, and *Misalignment discriminates by alignment, not by surface form.

Hebrew taQTiL intrusion ([Fau26] (10))

theorem Faust2026.hebrew_dmj_illicit_misaligned : hebrewDmj_illicit.isMisaligned

The illicit spreading derivation ([Fau26] (10a)) is misaligned: nonfinal /m/ landed at the template-final slot.

theorem Faust2026.hebrew_tadmit_not_misaligned : ¬hebrewDmj_tadmit.isMisaligned

The licit [tadmit] derivation ([Fau26] (10b–c)) — feminine /t/ intruder at the final [+c] slot — is not misaligned.

theorem Faust2026.hebrew_tadmit_satisfies : hebrewDmj_tadmit.satisfies

And [tadmit] does satisfy the template (all C-slots filled). This is the squib's central analytical move: intrusion is a template-satisfaction strategy that escapes *Misalignment by not being a root segment in the first place.

Amharic [j]-final verbal vs nominal ([Fau26] (5), (8))

theorem Faust2026.amharic_fdj_pfv_not_misaligned : ¬amharicFdj_pfv.isMisaligned

Amharic [fädʤ-ä] PFV is not misaligned (the final [+c] slot is truncated/unfilled, so no nonfinal root element is there).

theorem Faust2026.amharic_fdj_grnd_satisfies : amharicFdj_grnd.satisfies

Amharic [fädʤto] gerund satisfies the template via [t]-intrusion.

Faust's biradical reanalysis ([Fau26] page 432)

theorem Faust2026.amharic_wd_satisfies : amharicWd_pfv.satisfies

√wd's biradical [wäddäd-ä] satisfies the template — every C-slot filled, no *Misalignment violation (spreading /d/ to template-final is licit because /d/ is the final root segment). The OCP-violating √dd analysis [Bro84] posited is therefore unnecessary.

theorem Faust2026.hebrew_klj_misalign_dominates_fill : hebrewKlj_kalal.allCSlotsFilled ∧ hebrewKlj_kalal.isMisaligned ∧ ¬hebrewKlj_kala.allCSlotsFilled ∧ ¬hebrewKlj_kala.isMisaligned

[Fau26]'s central observation about Hebrew (4): for the same root √klj and template CaCaC[+c], the spreading candidate violates *Misalignment (despite satisfying the template) while the empty-slot candidate satisfies *Misalignment (despite an unfilled C-slot). The grammar's preference for the empty slot is exactly what *Misalignment >> FILL predicts — the squib's OT-implicit ranking.

theorem Faust2026.hebrew_intrusion_strictly_superior_to_spreading : hebrewDmj_illicit.allCSlotsFilled ∧ hebrewDmj_illicit.isMisaligned ∧ hebrewDmj_tadmit.allCSlotsFilled ∧ ¬hebrewDmj_tadmit.isMisaligned ∧ hebrewDmj_tadmit.satisfies

[Fau26]'s analytical move on Hebrew (10): templatic intrusion via the feminine /t/ is licit precisely because the intruder is not a root segment, so *Misalignment doesn't apply to it — and because it's licit, the template can be satisfied without an unfilled C-slot. The intruder strategy is strictly superior to spreading on both dimensions.

theorem Faust2026.biradical_spread_ok_triradical_spread_blocked : ¬amharicWd_pfv.isMisaligned ∧ hebrewKlj_kalal.isMisaligned

[Fau26]'s reanalysis (page 432): biradical vs triradical roots interact with *Misalignment differently. Spreading the final radical of a biradical root to template-final is licit (final-of-final), while spreading the medial radical of a triradical root is not. This is the type-level demonstration that the surface contrast between [wäddäd-ä] (OK) and *[kalal] (blocked) reduces to *Misalignment alone — no OCP-violating biradicals like [Bro84]'s √dd are needed.

theorem Faust2026.misalignment_predicts_all_cases : hebrewKlj_kalal.isMisaligned ∧ hebrewDmj_illicit.isMisaligned ∧ ¬hebrewKlj_kala.isMisaligned ∧ ¬hebrewKlj_kaluj.isMisaligned ∧ ¬hebrewDmj_tadmit.isMisaligned ∧ ¬amharicFdj_pfv.isMisaligned ∧ ¬amharicFdj_grnd.isMisaligned ∧ ¬amharicWd_pfv.isMisaligned

The squib's core analytical claim, in one statement: across both languages and all three phenomena, every form claimed to surface satisfies *Misalignment, while every form claimed to be ruled out violates it.

Connecting to the OCP infrastructure ([McC81])

Faust's biradical reanalysis turns on a substantive empirical claim about the OCP at the root level: once √fdj is recognized as triradical (with /j/ as the third radical, not a default-[t]-inducing biradical √fd), the only remaining "OCP violators" — apparent biradicals like √wd — turn out to have distinct radicals after all (/w/ ≠ /d/), with surface gemination produced by template spreading rather than root identity.

The Root.IsOCPClean predicate (in Morphology) makes this verifiable rather than asserted.

theorem Faust2026.amharic_wd_satisfies_root_ocp : Amharic.wd.IsOCPClean

[Fau26] page 432: √wd has no OCP violation at the root level — even though [wäddäd-ä] surfaces with adjacent identical [d][d], the surface gemination is a template-spreading effect.

theorem Faust2026.amharic_fdj_satisfies_root_ocp : Amharic.fdj.IsOCPClean

[Fau26]'s reanalysis: √fdj (the triradical analysis) has no OCP violation.

theorem Faust2026.hebrew_klj_satisfies_root_ocp : Hebrew.klj.IsOCPClean

And the Hebrew [j]-final root √klj also satisfies the OCP.

theorem Faust2026.hypothetical_dd_violates_root_ocp : ¬{ segments := ["d", "d"] }.IsOCPClean

Sanity: a hypothetical OCP-violating biradical √dd (which [Bro84] would have posited but [Fau26] rejects) really does violate the OCP under our predicate.

[Fau26] (11)'s structural diagnosis — that [t]-intrusion is the exponent of n[+gen] (cf. [Kra20]) and unavailable for verbs because gender lives on a higher Agr head — is formalized cross-paper in §12 below (the verbal/nominal asymmetry). The structural Kramer-2015/2020 background itself is verified in Studies/Kramer2020.lean.

The medial- vs. final-empty asymmetry

[Fau26] (13) presents an asymmetry inside the [t]-intrusion paradigm itself. Three Amharic INF forms are derived from roots whose "hollow" element (a non-consonantal radical merging with vocalization) sits at different positions in the root:

• (13a) [mäsmat] from √sma — non-consonantal final /a/ leaves the template-final C-slot unfilled. Right-edge [t]-intrusion fills that slot; the intruder is at the right edge of the association lines, so no other root association sits to its right. No NCC violation.

• (13b) [mäsam] from √sam — non-consonantal medial /a/ leaves the medial C-slot unfilled, but the final C-slot is filled by the third radical /m/. Right-edge [t]-intrusion would have to land at the medial slot, with /m/ already associated to the final slot — and the intruder line would cross the /m/ line. NCC blocks it.

• (13c) [mähid] from √hid — same structural configuration as (13b), but with /i/ as the non-consonantal medial. Same NCC blocking.

The Strict-CV [Low96] representation makes this asymmetry visible: which C-slot is empty matters because the No-Crossing Constraint [Gol76] discriminates by position relative to the rest of the association lines.

The infrastructure for this analysis lives in the template section defined above in this file: RootTemplateMatch.unfilledCSlots, RootTemplateMatch.violatesNCC, and the noCross constraint.

def Faust2026.amharicInf : Templates.Template

Amharic infinitive template (the five CV-skeletal slots after the [mä-] infinitive prefix). The final slot is [+c]-specified, which is what makes the [t]-intrusion question arise at all.

Equations

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

def Faust2026.amharicSma_inf : Templates.RootTemplateMatch String

(13a) [mäsmat] from √sma hear: the non-consonantal final radical /a/ leaves the template-final C-slot unfilled, and right-edge [t]-intrusion fills it without crossing any other root line.

Equations

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

def Faust2026.amharicSam_inf : Templates.RootTemplateMatch String

(13b) [mäsam] from √sam kiss: the non-consonantal medial radical /a/ leaves the medial C-slot unfilled, while the third radical /m/ fills the final C-slot. The medial position remains empty in the surface form.

Equations

• Faust2026.amharicSam_inf = { root := Amharic.sam, template := Faust2026.amharicInf, associations := [{ rootIndex := 0, slotIndex := 0 }, { rootIndex := 2, slotIndex := 4 }] }

def Faust2026.amharicSam_inf_intrusion : Templates.RootTemplateMatch String

Hypothetical [t]-intrusion candidate for √sam: tries to fill the medial C-slot from the right. The /m/ at C4 forces line-crossing. Demonstrates why intrusion is blocked in (13b).

Equations

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

def Faust2026.amharicHid_inf : Templates.RootTemplateMatch String

(13c) [mähid] from √hid go: structurally identical to (13b) — non-consonantal medial /i/ leaves the medial C-slot unfilled, /d/ fills the final C-slot. Same NCC blocking of [t]-intrusion.

Equations

• Faust2026.amharicHid_inf = { root := Amharic.hid, template := Faust2026.amharicInf, associations := [{ rootIndex := 0, slotIndex := 0 }, { rootIndex := 2, slotIndex := 4 }] }

def Faust2026.amharicHid_inf_intrusion : Templates.RootTemplateMatch String

Hypothetical [t]-intrusion candidate for √hid: same NCC violation as amharicSam_inf_intrusion.

Equations

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

Theorems — final-empty licenses intrusion, medial-empty blocks it

theorem Faust2026.amharic_sma_inf_satisfies : amharicSma_inf.satisfies

(13a): √sma's [t]-intrusion derivation satisfies the template — every C-slot is filled (root + intruder), no *Misalignment fires.

theorem Faust2026.amharic_sma_inf_no_ncc : ¬amharicSma_inf.violatesNCC

(13a): the right-edge intruder in √sma's INF does NOT violate the No-Crossing Constraint — there is no root association sitting to its right to be crossed.

theorem Faust2026.amharic_sam_inf_medial_unfilled : amharicSam_inf.unfilledCSlots = [2]

(13b)/(13c): without intrusion, the medial C-slot of √sam INF is unfilled. Indices into amharicInf = [C, V, C, V, Cspec]: only C2 is unfilled (C0 and C4 have associations, V1 and V3 aren't C-slots).

theorem Faust2026.amharic_hid_inf_medial_unfilled : amharicHid_inf.unfilledCSlots = [2]

(13c): same medial-only unfilled-slot pattern for √hid INF.

theorem Faust2026.amharic_sam_inf_intrusion_violates_ncc : amharicSam_inf_intrusion.violatesNCC

(13b): the hypothetical [t]-intrusion derivation for √sam violates the No-Crossing Constraint — the intruder at C2 would cross the /m/ root association at C4. This is what blocks intrusion in (13b).

theorem Faust2026.amharic_hid_inf_intrusion_violates_ncc : amharicHid_inf_intrusion.violatesNCC

(13c): same NCC violation blocks intrusion in √hid INF.

theorem Faust2026.hollow_root_intrusion_asymmetry : ¬amharicSma_inf.violatesNCC ∧ amharicSma_inf.satisfies ∧ amharicSam_inf_intrusion.violatesNCC ∧ amharicHid_inf_intrusion.violatesNCC ∧ amharicSam_inf.unfilledCSlots = [2] ∧ amharicHid_inf.unfilledCSlots = [2]

The structural asymmetry behind [Fau26] (13) in one statement: among the three hollow-root INFs, the one where the non-consonantal radical is final (√sma, leaving the final C-slot empty) admits [t]-intrusion without violating NCC, while the two where the non-consonantal radical is medial (√sam, √hid, leaving the medial C-slot empty) do not — a hypothetical medial intruder would have to cross the final root association line.

The QaTaT–QaTa choice as an OT optimization, grounded in §3

The squib's analysis is implicitly an OT ranking argument: the grammar chooses the candidate that satisfies *Misalignment over the candidate that satisfies FILL. Sections 7–8 state this ranking via the joint hebrew_klj_misalign_dominates_fill predicate; here we make it explicit by building tableaux directly over the RootTemplateMatch candidates defined in §3, using the starMisalign and fill constraints from the template section above.

This is the "derive, don't stipulate" architecture: the OT verdicts follow from the same isMisaligned and allCSlotsFilled predicates that prove §3–§7, so any change to those predicates would propagate into the tableau predictions automatically.

Two demonstrations:

1. The empirical ranking *Misalign >> FILL selects [kala], the surface form. This is the prediction.
2. The reversed ranking FILL >> *Misalign selects *[kalal], the form that is empirically ruled out. This shows that the ranking is doing real work — without *Misalignment dominating, the spreading candidate would win on template-satisfaction grounds.

def Faust2026.kljCandidates : List (Templates.RootTemplateMatch String)

The √klj candidate set: the spreading attempt and the empty-slot actual surface form. Built as the RootTemplateMatch values from §3 — no enum re-stipulation.

Equations

• Faust2026.kljCandidates = [Faust2026.hebrewKlj_kalal, Faust2026.hebrewKlj_kala]

theorem Faust2026.kljCandidates_ne : kljCandidates ≠ []

theorem Faust2026.kala_wins_under_misalign_over_fill : (OptimalityTheory.Tableau.ofRanking kljCandidates [Templates.starMisalign, Templates.fill] kljCandidates_ne).optimal = {hebrewKlj_kala}

The empirical ranking *Misalign >> FILL selects [kala]: the surface form, with an unfilled template-final C-slot, wins because *Misalignment outranks FILL. The verdict follows from the isMisaligned/allCSlotsFilled computations on the RootTemplateMatch values — no stipulated violation tables.

theorem Faust2026.kalal_predicted_under_reversed_ranking : (OptimalityTheory.Tableau.ofRanking kljCandidates [Templates.fill, Templates.starMisalign] kljCandidates_ne).optimal = {hebrewKlj_kalal}

Reversed ranking FILL >> *Misalign predicts the spreading candidate *[kalal] — the form [Fau26] (4) explicitly argues against. The reversed-ranking demo shows that *Misalignment dominance is doing the empirical work; without it, template satisfaction would force the wrong winner.

theorem Faust2026.klj_factorial_typology_size_two : (OptimalityTheory.factorialOptima kljCandidates [Templates.starMisalign, Templates.fill] kljCandidates_ne).length = 2

Factorial typology over {*Misalign, FILL}: the two rankings yield two distinct optimal sets. This is the OT-typological statement of [Fau26]'s claim — the constraint set predicts exactly two languages, the attested Hebrew/Amharic pattern (kala- type, with empty C-slots tolerated) and a hypothetical mirror (kalal-type, where spreading wins).

The (3) three-way contrast as a tableau

For √klt and √kll, no *Misalignment violation arises in any candidate, so both surface forms (hebrewKlt_kalat, hebrewKll_kalal) are unique winners under any ranking — the QaTaT–QaTa "puzzle" only bites when the third radical is /j/.

theorem Faust2026.kalat_unique_optimum : (OptimalityTheory.Tableau.ofRanking [hebrewKlt_kalat] [Templates.starMisalign, Templates.fill] ⋯).optimal = {hebrewKlt_kalat}

(3a) [kalat] from √klt is the unique optimum because every C-slot is filled and *Misalignment is satisfied — both constraints have zero violations, so it wins under any ranking.

theorem Faust2026.kalal_from_kll_unique_optimum : (OptimalityTheory.Tableau.ofRanking [hebrewKll_kalal] [Templates.starMisalign, Templates.fill] ⋯).optimal = {hebrewKll_kalal}

(3b) [kalal] from √kll likewise wins as the unique optimum: the legitimate final-of-final spreading satisfies *Misalignment AND fills the template. Same logic as (3a), but the empirical interest is that the surface form is identical to the ungrammatical *[kalal] derivation from √klj — only the underlying root index differs, and that's exactly what *Misalignment is sensitive to.

The Hebrew taQTiL intrusion case as a three-candidate tableau

The taQTiL[+c] template admits three derivations for √dmj: the illicit spreading (10a, hebrewDmj_illicit), the licit intrusion (10b–c, hebrewDmj_tadmit), and the empty-slot fallback. We need to construct the empty-slot candidate explicitly to populate the tableau.

def Faust2026.hebrewDmj_empty : Templates.RootTemplateMatch String

Empty-slot candidate for √dmj + taQTiL[+c]: the prefix /t/ plus /d/ and /m/ at C2/C3, with the [+c] final C-slot unfilled. Hypothetical (not the empirical winner) — included to exhibit the full three-way comparison.

Equations

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

def Faust2026.taqtilCandidates : List (Templates.RootTemplateMatch String)

Equations

• Faust2026.taqtilCandidates = [Faust2026.hebrewDmj_illicit, Faust2026.hebrewDmj_empty, Faust2026.hebrewDmj_tadmit]

theorem Faust2026.taqtilCandidates_ne : taqtilCandidates ≠ []

theorem Faust2026.tadmit_wins_under_misalign_over_fill : (OptimalityTheory.Tableau.ofRanking taqtilCandidates [Templates.starMisalign, Templates.fill] taqtilCandidates_ne).optimal = {hebrewDmj_tadmit}

The intrusion candidate [tadmit] is strictly better than both alternatives: it has 0 violations on *Misalign AND 0 violations on FILL. So under any ranking of these two constraints, [tadmit] wins. This is [Fau26]'s core analytical point about (10): intrusion lets the grammar "have it both ways".

theorem Faust2026.tadmit_wins_under_fill_over_misalign : (OptimalityTheory.Tableau.ofRanking taqtilCandidates [Templates.fill, Templates.starMisalign] taqtilCandidates_ne).optimal = {hebrewDmj_tadmit}

And it wins under the reversed ranking too — because intrusion satisfies both constraints, the ranking between them is irrelevant once the intrusion candidate is in the candidate set.

theorem Faust2026.taqtil_factorial_typology_size_one : (OptimalityTheory.factorialOptima taqtilCandidates [Templates.starMisalign, Templates.fill] taqtilCandidates_ne).length = 1

The taQTiL factorial typology collapses to one language: when an intrusion strategy is in the candidate set, both rankings of {*Misalign, FILL} pick the same winner. The OT-typological statement that intrusion is "ranking-invariant" — exactly the sense in which [Fau26] (10b–c) makes intrusion the grammar's optimal escape from the misalignment dilemma.

Cross-paper bridge — n[+gen] licenses intrusion, Agr does not

[Fau26] (11) attributes the nominal-only distribution of [t]-intrusion to a structural fact: the intruding /t/ is the exponent of the n[+gen] head in [Kra20]'s sense — gender is realized inherently on n, exposed as a sister bound root in [Low14]'s sense. In verbal forms the corresponding gender feature lives on a higher Agr head as contextual agreement, not as an inherent root-like exponent on v itself; consequently no intruder is morphosyntactically available to fill the templatic slot.

Sections 1–11 verify the prosodic side of the analysis (intrusion satisfies the template without violating *Misalignment). This section verifies the morphological side by formalizing the Faust claim as a predicate on Kramer's CatHead:

Intrusion is licensed iff the categorizer is n and carries a gender feature.

Once that predicate is in place, the verbal/nominal asymmetry is no longer a docstring stipulation — it falls out by rfl from RootTemplateMatch.intrusionLicensed applied to the per-template CatHead tags, and breaks if either Faust's morphological claim or Kramer's CatHead taxonomy changes.

The morphological-licensing predicate CatHead.licensesIntrusion itself lives in Morphology/DM/Categorizer.lean (alongside the Kramer taxonomy it ranges over), together with its per-canonical- head verification theorems (n_uFem_licenses_intrusion, v_plain_blocks_intrusion, etc.) and the iff characterization Morphology.DM.licensesIntrusion_iff_n_and_gen. The Faust-specific content of §12 is the per-template CatHead tagging and the per-derivation verdicts below.

Per-template CatHead tags

Faust's analysis assigns each templatic morphology slot to a specific categorizer head. These are the morphosyntactic claims; the intrusion-licensing predictions follow mechanically.

def Faust2026.hebrewPst3msg_locus : Morphology.DM.CatHead

Hebrew PST.3MSG CaCaC[+c] is realized at v (verbal categorizer); gender lives on the Agr head outside the template, so v itself has no gender-bearing exponent to intrude.

Equations

• Faust2026.hebrewPst3msg_locus = Morphology.DM.CatHead.v_plain

def Faust2026.hebrewPassPrtcpl_locus : Morphology.DM.CatHead

Hebrew passive participle CaCuC is also v-realized.

Equations

• Faust2026.hebrewPassPrtcpl_locus = Morphology.DM.CatHead.v_plain

def Faust2026.hebrewTaQTiL_locus : Morphology.DM.CatHead

Hebrew taQTiL[+c] is a feminine deverbal noun realized at n[+gen] (the u[+FEM] head in Kramer's Set 1 taxonomy — the source of the intruding /t/).

Equations

• Faust2026.hebrewTaQTiL_locus = Morphology.DM.CatHead.n_uFem

def Faust2026.amharicPfv3msg_locus : Morphology.DM.CatHead

Amharic PFV.3MSG CäC.CäC[+c] is v-realized.

Equations

• Faust2026.amharicPfv3msg_locus = Morphology.DM.CatHead.v_plain

def Faust2026.amharicGrnd_locus : Morphology.DM.CatHead

Amharic gerund CäC.C[+c]-o is a deverbal nominal at n[+gen].

Equations

• Faust2026.amharicGrnd_locus = Morphology.DM.CatHead.n_uFem

def Faust2026.amharicInf_locus : Morphology.DM.CatHead

Amharic infinitive mä-CVCVC[+c] is also a deverbal nominal at n[+gen] — confirmed by the (13a) [t]-intrusion in [mäsmat]. [Fau26]'s analysis treats Amharic infinitives as nominalizations whose template is hosted on n.

Equations

• Faust2026.amharicInf_locus = Morphology.DM.CatHead.n_uFem

Universal licensing structure (Faust + Kramer)

The Faust-CatHead interaction is governed by a single structural fact, derivable by composing intrusionLicensed_iff (the template section above) with licensesIntrusion_iff_n_and_gen (Categorizer.lean). The per-derivation decide theorems below and the end-of-section verbal_nominal_asymmetry_from_kramer bundle are all instances of this universal claim.

theorem Faust2026.intrusion_wellformed_iff_no_intruder_or_n_with_gen (m : Templates.RootTemplateMatch String) (ch : Morphology.DM.CatHead) : m.intrusionLicensed ch.licensesIntrusion ↔ ¬m.hasIntruder ∨ ch.cat = Morphology.DM.Categorizer.n ∧ ch.phi.gender.isSome = true

The Faust+Kramer integration theorem. A RootTemplateMatch passes intrusion-licensing under a CatHead iff either the match is intruder-free OR the head is a gender-bearing nominal (n[+gen], in [Kra20]'s sense).

This is the universal-quantification of [Fau26] (11): every per-derivation verdict in §12 reduces to checking which disjunct holds for the specific (match, head) pair.

theorem Faust2026.v_plain_licenses_iff_no_intruder (m : Templates.RootTemplateMatch String) : m.intrusionLicensed Morphology.DM.CatHead.v_plain.licensesIntrusion ↔ ¬m.hasIntruder

Corollary (verbal half). Under a verbal locus (v_plain, with no gender feature), licensing reduces to intruder-freeness. This is why every verbal Faust derivation in §3–§6 must be intruder-free to be morphologically licensed — the spreading and empty-slot strategies are the only options open to v.

theorem Faust2026.n_uFem_licenses_universally (m : Templates.RootTemplateMatch String) : m.intrusionLicensed Morphology.DM.CatHead.n_uFem.licensesIntrusion

Corollary (nominal half). Under an n_uFem locus (gender- bearing nominal), every match is licensed regardless of intruder status. This is why intrusion is available to nominal templates like Hebrew taQTiL and Amharic gerunds/INFs — the Kramer-2020 structure makes the n[+gen] exponent morphosyntactically present.

Per-derivation licensing theorems

For every match, the predicate RootTemplateMatch.intrusionLicensed applied to the corresponding template's CatHead.licensesIntrusion gives the well-formedness verdict. The proofs are decide — the disjunction reduces by rfl once the predicates evaluate.

Hebrew verbal forms (no intrusion possible)

theorem Faust2026.kalat_licensed_at_v : hebrewKlt_kalat.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion

theorem Faust2026.kalal_kll_licensed_at_v : hebrewKll_kalal.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion

theorem Faust2026.kala_licensed_at_v : hebrewKlj_kala.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion

theorem Faust2026.kalal_klj_licensed_at_v : hebrewKlj_kalal.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion

theorem Faust2026.kaluj_licensed_at_v : hebrewKlj_kaluj.intrusionLicensed hebrewPassPrtcpl_locus.licensesIntrusion

Hebrew nominal taQTiL (intrusion possible)

theorem Faust2026.dmj_illicit_licensed_at_n : hebrewDmj_illicit.intrusionLicensed hebrewTaQTiL_locus.licensesIntrusion

The illicit-spreading derivation also passes intrusion-licensing (its prefix /t/ is an intruder, but n[+gen] licenses it). The derivation is ruled out by *Misalignment, not by the morphological licensing — a useful separation.

theorem Faust2026.tadmit_licensed_at_n : hebrewDmj_tadmit.intrusionLicensed hebrewTaQTiL_locus.licensesIntrusion

Amharic verbal vs nominal

theorem Faust2026.fdj_pfv_licensed_at_v : amharicFdj_pfv.intrusionLicensed amharicPfv3msg_locus.licensesIntrusion

theorem Faust2026.wd_pfv_licensed_at_v : amharicWd_pfv.intrusionLicensed amharicPfv3msg_locus.licensesIntrusion

theorem Faust2026.fdj_grnd_licensed_at_n : amharicFdj_grnd.intrusionLicensed amharicGrnd_locus.licensesIntrusion

theorem Faust2026.sma_inf_licensed_at_n : amharicSma_inf.intrusionLicensed amharicInf_locus.licensesIntrusion

The verbal-intrusion blocking theorem

The empirical content of [Fau26] (11) is negative: a verbal template cannot host an [t]-intruder, even when a phonological analog of intrusion would technically resolve a misalignment problem. Construct a hypothetical verbal candidate that tries to use intrusion — analogous to the licit nominal [tadmit] — and prove it fails morphological licensing.

def Faust2026.hebrewDmj_pst3msg_intrusion : Templates.RootTemplateMatch String

Hypothetical: √dmj realized in the verbal PST.3MSG template CaCaC[+c] with a feminine /t/ intruder occupying the [+c] final slot. Phonologically identical to a nominal intrusion candidate, but Agr-locus precludes the n[+gen] exponent morphosyntactically.

Equations

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

theorem Faust2026.hebrew_pst3msg_intrusion_prosodically_satisfies : hebrewDmj_pst3msg_intrusion.satisfies

The hypothetical verbal-intrusion candidate has all C-slots filled and is not misaligned: it satisfies the prosodic well-formedness conditions [Fau26] states.

theorem Faust2026.hebrew_pst3msg_intrusion_morphologically_blocked : ¬hebrewDmj_pst3msg_intrusion.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion

But under [Fau26]'s morphological-licensing predicate, it fails: v-locus does not license n[+gen]'s /t/ exponent.

The cross-paper integration theorem

theorem Faust2026.verbal_nominal_asymmetry_from_kramer : hebrewDmj_tadmit.intrusionLicensed hebrewTaQTiL_locus.licensesIntrusion ∧ amharicFdj_grnd.intrusionLicensed amharicGrnd_locus.licensesIntrusion ∧ ¬hebrewDmj_pst3msg_intrusion.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion ∧ hebrewDmj_pst3msg_intrusion.satisfies ∧ hebrewKlj_kala.intrusionLicensed hebrewPst3msg_locus.licensesIntrusion ∧ amharicFdj_pfv.intrusionLicensed amharicPfv3msg_locus.licensesIntrusion

The verbal/nominal asymmetry of [Fau26] (11), derived from [Kra20]'s CatHead taxonomy:

1. Intrusion is licensed at n[+gen] (here n_uFem). Both Hebrew taQTiL [tadmit] and the hypothetical verbal-template intrusion hebrewDmj_pst3msg_intrusion would pass intrusion-licensing if the locus were n[+gen]. The first derivation IS at n[+gen]; the second is not.

2. Intrusion is blocked at v. The hypothetical verbal intrusion candidate, despite satisfying the template, fails intrusion-licensing because v doesn't expose a gender exponent.

3. Intruder-free verbal derivations always pass licensing. Every verbal candidate in §3–§6 (kala, kalal, kalat, kaluj, fdj_pfv, wd_pfv) is intruder-free, so it passes vacuously.

The asymmetry is therefore derived — not stipulated — from the composition of two independent claims: Faust's licensing predicate (only n with [+gen]) and Kramer's CatHead structure (n vs. v).