CV-Skeletal Templates and Root–Template Association

@cite{mccarthy-1981} @cite{lowenstamm-1996} @cite{faust-2026}

The McCarthy 1981 / Strict-CV (Lowenstamm 1996) representation of nonconcatenative morphology: a template is a sequence of CV slots, optionally specified for [+consonantal]; a root is associated to the template by mapping root segments to slots (left-to-right by default).

Single source of truth

This module provides one Template type, one Association type, and one RootTemplateMatch carrier — used by every templatic-morphology study in the library. The Root α segment type is imported from Core.Lexical, so that the same root data is shared between phonology (this module), morphology (template-satisfaction analyses), and fragments (Hebrew, Amharic, Tarifit).

*Misalignment

Following @cite{faust-2026}, a derived predicate RootTemplateMatch.isMisaligned fires when a nonfinal root segment lands in the final template slot. The predicate distinguishes associations from the root proper (AssocSource.root) from associations from a sister exponent (AssocSource.intruder, e.g. the feminine [t] in Hebrew taQTiL or Amharic gerund and INF). Intruder associations are exempt from *Misalignment because the intruder is not a root segment in the first place — the central analytical move of @cite{faust-2026} §4.

inductive Phonology.Templates.CVSlot : Type

A slot in a CV-skeletal template (@cite{mccarthy-1981}, @cite{lowenstamm-1996}):

• 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 (@cite{faust-2026} (4)).

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

@[implicit_reducible]

instance Phonology.Templates.instDecidableEqCVSlot : DecidableEq CVSlot

Equations

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

@[implicit_reducible]

instance Phonology.Templates.instReprCVSlot : Repr CVSlot

Equations

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

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

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance Phonology.Templates.CVSlot.instDecidablePredIsC : DecidablePred IsC

Equations

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

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

Is this slot a V-slot?

Equations

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

@[implicit_reducible]

instance Phonology.Templates.CVSlot.instDecidablePredIsV : DecidablePred IsV

Equations

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

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

Does this slot require a [+consonantal] segment?

Equations

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

@[implicit_reducible]

instance Phonology.Templates.CVSlot.instDecidablePredRequiresConsonantal : DecidablePred RequiresConsonantal

Equations

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

structure Phonology.Templates.Template : Type

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

• slots : List CVSlot

@[implicit_reducible]

instance Phonology.Templates.instReprTemplate : Repr Template

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phonology.Templates.instDecidableEqTemplate : DecidableEq Template

Equations

• Phonology.Templates.instDecidableEqTemplate = Phonology.Templates.instDecidableEqTemplate.decEq

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

The number of slots in the template.

Equations

• t.length = t.slots.length

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

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

Equations

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

def Phonology.Templates.Template.isFinalSlot (t : Template) (i : ℕ) : Bool

Slot i is the final slot of the template.

Equations

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

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

The slot at position i, if in range.

Equations

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

inductive Phonology.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, @cite{faust-2026} (10)) that satisfy the template without being root segments themselves.

• root : AssocSource
• intruder : AssocSource

@[implicit_reducible]

instance Phonology.Templates.instDecidableEqAssocSource : DecidableEq AssocSource

Equations

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

@[implicit_reducible]

instance Phonology.Templates.instReprAssocSource : Repr AssocSource

Equations

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

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

Equations

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

structure Phonology.Templates.Association : Type

A single root-to-slot association line (@cite{mccarthy-1981}).

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 : ℕ

@[implicit_reducible]

instance Phonology.Templates.instDecidableEqAssociation : DecidableEq Association

Equations

• Phonology.Templates.instDecidableEqAssociation = Phonology.Templates.instDecidableEqAssociation.decEq

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Phonology.Templates.instReprAssociation : Repr Association

Equations

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

structure Phonology.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 : Core.Morphology.Root α
• template : Template
• associations : List Association

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• Phonology.Templates.instDecidableEqRootTemplateMatch = Phonology.Templates.instDecidableEqRootTemplateMatch.decEq

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

Equations

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

def Phonology.Templates.RootTemplateMatch.isRootFinal {α : Type} (m : RootTemplateMatch α) (a : Association) : Bool

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 == Phonology.Templates.AssocSource.root && m.template.isFinalSlot a.slotIndex)

def Phonology.Templates.RootTemplateMatch.isMisaligned {α : Type} (m : RootTemplateMatch α) : Bool

Misalignment (@cite{faust-2026} (2)): the match has a nonfinal root segment associated to the template-final slot. Intruder associations do not count — see AssocSource.

Equations

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

def Phonology.Templates.RootTemplateMatch.allCSlotsFilled {α : Type} (m : RootTemplateMatch α) : Bool

Every C-slot of the template is filled by some association (root or intruder).

Equations

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

def Phonology.Templates.RootTemplateMatch.satisfies {α : Type} (m : RootTemplateMatch α) : Bool

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 @cite{faust-2026} is that for [j]-final biradicals in Hebrew, one cannot satisfy the first without violating the second.

Equations

• m.satisfies = (m.allCSlotsFilled && !m.isMisaligned)

def Phonology.Templates.RootTemplateMatch.inBounds {α : Type} (m : RootTemplateMatch α) : Bool

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

Equations

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

def Phonology.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 (@cite{faust-2026} (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.

def Phonology.Templates.RootTemplateMatch.violatesNCC {α : Type} (m : RootTemplateMatch α) : Bool

The No-Crossing Constraint (@cite{goldsmith-1976}): 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 @cite{faust-2026} (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.

def Phonology.Templates.RootTemplateMatch.hasIntruder {α : Type} (m : RootTemplateMatch α) : Bool

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 = m.associations.any fun (x : Phonology.Templates.Association) => x.source == Phonology.Templates.AssocSource.intruder

def Phonology.Templates.RootTemplateMatch.intrusionLicensed {α : Type} (m : RootTemplateMatch α) (licensed : Bool) : Bool

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 @cite{lowenstamm-2014}), or (b) the match contains no intruder associations.

The licensing predicate is supplied by the morphological theory above — for @cite{faust-2026}'s analysis, it evaluates to true iff the template is realized at an n[+gen] head in @cite{kramer-2020}'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 rather than a MorphologicalLocus enum so that Templates.lean need not depend on Morphology.DM.

Equations

• m.intrusionLicensed licensed = (licensed || !m.hasIntruder)

theorem Phonology.Templates.isMisaligned_empty {α : Type} (r : Core.Morphology.Root α) (t : Template) : { root := r, template := t, associations := [] }.isMisaligned = false

A match with no associations is trivially not misaligned.

theorem Phonology.Templates.isMisaligned_intruder_only {α : Type} (r : Core.Morphology.Root α) (t : Template) (assocs : List Association) (h : (assocs.all fun (a : Association) => a.source == AssocSource.intruder) = true) : { root := r, template := t, associations := assocs }.isMisaligned = false

*Misalignment cannot fire from intruder associations alone.

theorem Phonology.Templates.isMisaligned_iff {α : Type} (m : RootTemplateMatch α) : m.isMisaligned = true ↔ ∃ a ∈ m.associations, a.source = AssocSource.root ∧ m.root.isNonfinal a.rootIndex = true ∧ m.template.isFinalSlot a.slotIndex = true

Structural characterization of isMisaligned: there exists a root association at a nonfinal root position landing at a template-final slot. Lets later proofs reason about misalignment via a witness rather than unfolding List.any.

theorem Phonology.Templates.violatesNCC_iff {α : Type} (m : RootTemplateMatch α) : m.violatesNCC = true ↔ ∃ a ∈ m.associations, a.source = AssocSource.intruder ∧ ∃ b ∈ m.associations, b.source = AssocSource.root ∧ a.slotIndex < b.slotIndex

Structural characterization of violatesNCC: there exist an intruder association and a root association with the intruder strictly to the left of the root association.

theorem Phonology.Templates.satisfies_iff {α : Type} (m : RootTemplateMatch α) : m.satisfies = true ↔ m.allCSlotsFilled = true ∧ m.isMisaligned = false

satisfies decomposes into its two conjuncts: all C-slots filled AND not misaligned. The reading the squib's central argument depends on.

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

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 Phonology.Templates.intrusionLicensed_of_no_intruder {α : Type} (m : RootTemplateMatch α) (h : m.hasIntruder = false) (licensed : Bool) : m.intrusionLicensed licensed = true

Intruder-free matches are licensed in any morphosyntactic context.

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

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

def Phonology.Templates.starMisalign {α : Type} : Core.Constraint.OT.NamedConstraint (RootTemplateMatch α)

The *Misalignment constraint of @cite{faust-2026} (2): a markedness constraint that fires on RootTemplateMatch candidates whose isMisaligned predicate holds. Built via the generic mkAlign constructor from Phonology.Constraints.

Equations

• Phonology.Templates.starMisalign = Phonology.Constraints.mkAlign "*Misalign" fun (m : Phonology.Templates.RootTemplateMatch α) => m.isMisaligned = true

theorem Phonology.Templates.starMisalign_is_markedness {α : Type} : starMisalign.family = Core.Constraint.OT.ConstraintFamily.markedness

*Misalignment is classified as markedness, not faithfulness.

def Phonology.Templates.fill {α : Type} : Core.Constraint.OT.NamedConstraint (RootTemplateMatch α)

The FILL constraint (@cite{prince-smolensky-1993}): a markedness constraint penalizing unfilled C-slots in the template. Used by @cite{faust-2026}'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

• Phonology.Templates.fill = Core.Constraint.OT.mkMark "FILL" fun (m : Phonology.Templates.RootTemplateMatch α) => m.allCSlotsFilled = false

theorem Phonology.Templates.fill_is_markedness {α : Type} : fill.family = Core.Constraint.OT.ConstraintFamily.markedness

FILL is classified as markedness.

def Phonology.Templates.noCross {α : Type} : Core.Constraint.OT.NamedConstraint (RootTemplateMatch α)

NoCross (@cite{goldsmith-1976}): a markedness constraint penalizing candidates whose intruder associations cross root associations.

Equations

• Phonology.Templates.noCross = Core.Constraint.OT.mkMark "NoCross" fun (m : Phonology.Templates.RootTemplateMatch α) => m.violatesNCC = true

theorem Phonology.Templates.noCross_is_markedness {α : Type} : noCross.family = Core.Constraint.OT.ConstraintFamily.markedness

NoCross is classified as markedness.