The Nouns that Say -ni [Ait26]

Aitha, A. (2026). The nouns that say -ni: Morpheme-specific phonology in Telugu. Natural Language & Linguistic Theory 44:16.

Overview

Telugu nouns exhibit two stem alternation patterns:

1. Strong alternation: NOM il-lu vs oblique in-ṭi ('house'). Genuine case-conditioned contextual allomorphy, analyzed via DM Vocabulary Insertion with [McF18]'s case containment hierarchy. The NOM-vs-oblique split follows from the Elsewhere Condition: a rule conditioned on [ACC] is more specific than an unconditioned default.

2. Weak alternation: NOM samudr-am vs ACC samudr-āni ('ocean'). Surface pattern looks like case-conditioned allomorphy but is phonological. Three diagnostics show it cannot be case allomorphy: (a) the ABAB paradigm shape violates [Cah09]'s *ABA constraint; (b) noncase agreement suffixes trigger the alternation; (c) the conditioning requires strict linear adjacency (phonological, not structural locality).

   The alternation is derived in Stratal OT ([Kip00]): both surface forms derive from a single underlying -am-ni, where -ni is a singular suffix with prespecified stress. The interaction of stress faithfulness with foot binarity constraints across three phonological strata (Stem, Word, Phrase) produces the alternation.

Formalization

• §1: Telugu case system and paradigm data
• §2: Strong alternation — VI rules and Elsewhere Condition
• §3: Weak alternation — *ABA violation and syllable-weight conditioning
• §4: Stem-level metrical parsing (OT tableau)
• §5: Word-level phonology — NOM and DAT tableaux (Stratal OT)
• §6: Word-based surface form prediction

inductive Aitha2026.TeluguCase : Type

Telugu case values relevant to nominal paradigms.

• nom : TeluguCase
• acc : TeluguCase
• gen : TeluguCase
• dat : TeluguCase
• loc : TeluguCase

@[implicit_reducible]

instance Aitha2026.instDecidableEqTeluguCase : DecidableEq TeluguCase

Equations

• Aitha2026.instDecidableEqTeluguCase x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instReprTeluguCase : Repr TeluguCase

Equations

• Aitha2026.instReprTeluguCase = { reprPrec := Aitha2026.instReprTeluguCase.repr }

def Aitha2026.instReprTeluguCase.repr : TeluguCase → ℕ → Std.Format

Equations

• Aitha2026.instReprTeluguCase.repr Aitha2026.TeluguCase.nom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.TeluguCase.nom")).group prec✝
• Aitha2026.instReprTeluguCase.repr Aitha2026.TeluguCase.acc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.TeluguCase.acc")).group prec✝
• Aitha2026.instReprTeluguCase.repr Aitha2026.TeluguCase.gen prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.TeluguCase.gen")).group prec✝
• Aitha2026.instReprTeluguCase.repr Aitha2026.TeluguCase.dat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.TeluguCase.dat")).group prec✝
• Aitha2026.instReprTeluguCase.repr Aitha2026.TeluguCase.loc prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.TeluguCase.loc")).group prec✝

def Aitha2026.TeluguCase.toCore : TeluguCase → Case

Map Telugu cases to the core Case type.

Equations

• Aitha2026.TeluguCase.nom.toCore = Case.nom
• Aitha2026.TeluguCase.acc.toCore = Case.acc
• Aitha2026.TeluguCase.gen.toCore = Case.gen
• Aitha2026.TeluguCase.dat.toCore = Case.dat
• Aitha2026.TeluguCase.loc.toCore = Case.loc

def Aitha2026.TeluguCase.IsNonnom (c : TeluguCase) : Prop

Is this Telugu case nonnominative? Derived from Case.IsNonnominative, which is (.acc : Case) ≤ c under the [Cah09]/[McF18] containment ordering. The full containment hierarchy lives at Syntax.Case.Order (containmentRank, cahaLE); Aitha's n-head VI rules condition on this binary projection of the hierarchy down to a NOM-vs-oblique contrast at the n head — the layered hierarchy is the substrate, the binary split is the Telugu-n-specific reduction.

Equations

• c.IsNonnom = c.toCore.IsNonnominative

@[implicit_reducible]

instance Aitha2026.instDecidableIsNonnom (c : TeluguCase) : Decidable c.IsNonnom

Equations

• Aitha2026.instDecidableIsNonnom c = Aitha2026.instDecidableIsNonnom._aux_1 c

inductive Aitha2026.StrongClass : Type

Root class for strongly suppletive nouns. [Ait26] lists 7 subclasses, all sharing the NOM-vs-oblique split. Multiple NOM subclasses share a single OBL form (-ṭi for all but the -u∼-i class), a prediction of the Elsewhere Condition: the more specific (OBL) rule can generalize across root sets. We formalize two representative classes; the analysis extends to all.

• luTi : StrongClass
• uI : StrongClass

@[implicit_reducible]

instance Aitha2026.instDecidableEqStrongClass : DecidableEq StrongClass

Equations

• Aitha2026.instDecidableEqStrongClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprStrongClass.repr : StrongClass → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Aitha2026.instReprStrongClass.repr Aitha2026.StrongClass.uI prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.StrongClass.uI")).group prec✝

@[implicit_reducible]

instance Aitha2026.instReprStrongClass : Repr StrongClass

Equations

• Aitha2026.instReprStrongClass = { reprPrec := Aitha2026.instReprStrongClass.repr }

structure Aitha2026.StrongParadigm : Type

Strong noun paradigm: the n-exponent for each case. All strong nouns share the NOM-vs-oblique split regardless of the actual surface shape of n.

• nomForm : String
• oblForm : String

def Aitha2026.instDecidableEqStrongParadigm.decEq (x✝ x✝¹ : StrongParadigm) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Aitha2026.instDecidableEqStrongParadigm : DecidableEq StrongParadigm

Equations

• Aitha2026.instDecidableEqStrongParadigm = Aitha2026.instDecidableEqStrongParadigm.decEq

@[implicit_reducible]

instance Aitha2026.instReprStrongParadigm : Repr StrongParadigm

Equations

• Aitha2026.instReprStrongParadigm = { reprPrec := Aitha2026.instReprStrongParadigm.repr }

def Aitha2026.instReprStrongParadigm.repr : StrongParadigm → ℕ → Std.Format

Equations

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

def Aitha2026.luTiParadigm : StrongParadigm

The n-exponent for the -lu∼-ṭi class.

Equations

• Aitha2026.luTiParadigm = { nomForm := "lu", oblForm := "ṭi" }

def Aitha2026.uIParadigm : StrongParadigm

The n-exponent for the -u∼-i class.

Equations

• Aitha2026.uIParadigm = { nomForm := "u", oblForm := "i" }

def Aitha2026.strongSurface (p : StrongParadigm) (c : TeluguCase) : String

Surface form of n given a strong paradigm and case.

Equations

• Aitha2026.strongSurface p c = if c.IsNonnom then p.oblForm else p.nomForm

inductive Aitha2026.WeakStemForm : Type

Stem form in weakly suppletive nouns.

• short : WeakStemForm
• long : WeakStemForm

@[implicit_reducible]

instance Aitha2026.instDecidableEqWeakStemForm : DecidableEq WeakStemForm

Equations

• Aitha2026.instDecidableEqWeakStemForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprWeakStemForm.repr : WeakStemForm → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aitha2026.instReprWeakStemForm : Repr WeakStemForm

Equations

• Aitha2026.instReprWeakStemForm = { reprPrec := Aitha2026.instReprWeakStemForm.repr }

def Aitha2026.weakParadigm : TeluguCase → WeakStemForm

The weak noun paradigm for samudram 'ocean'. Data from [KG85].

Equations

• Aitha2026.weakParadigm Aitha2026.TeluguCase.nom = Aitha2026.WeakStemForm.short
• Aitha2026.weakParadigm Aitha2026.TeluguCase.acc = Aitha2026.WeakStemForm.long
• Aitha2026.weakParadigm Aitha2026.TeluguCase.gen = Aitha2026.WeakStemForm.short
• Aitha2026.weakParadigm Aitha2026.TeluguCase.dat = Aitha2026.WeakStemForm.long
• Aitha2026.weakParadigm Aitha2026.TeluguCase.loc = Aitha2026.WeakStemForm.short

structure Aitha2026.NContext : Type

Morphosyntactic context for VI at the n head in Telugu. Carries the root class and the Telugu case directly; nonnominativity is derived from case.IsNonnom rather than stored as a Bool — so the McFadden 2018 / Caha 2009 containment substrate is the source of truth at every VI use site.

• rootClass : StrongClass
• case : TeluguCase

def Aitha2026.instDecidableEqNContext.decEq (x✝ x✝¹ : NContext) : Decidable (x✝ = x✝¹)

Equations

• Aitha2026.instDecidableEqNContext.decEq { rootClass := a, case := a_1 } { rootClass := b, case := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instDecidableEqNContext : DecidableEq NContext

Equations

• Aitha2026.instDecidableEqNContext = Aitha2026.instDecidableEqNContext.decEq

@[implicit_reducible]

instance Aitha2026.instReprNContext : Repr NContext

Equations

• Aitha2026.instReprNContext = { reprPrec := Aitha2026.instReprNContext.repr }

def Aitha2026.instReprNContext.repr : NContext → ℕ → Std.Format

Equations

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

def Aitha2026.viLuNom : Morphology.DM.VI.VocabItem NContext Unit

VI rule for NOM n of the -lu∼-ṭi class. No nonnominative requirement → this is the elsewhere/default rule.

Equations

• Aitha2026.viLuNom = { exponent := "lu", contextMatch := fun (ctx : Aitha2026.NContext) => ctx.rootClass == Aitha2026.StrongClass.luTi, specificity := 1 }

def Aitha2026.viLuObl : Morphology.DM.VI.VocabItem NContext Unit

VI rule for oblique n of the -lu∼-ṭi class. Requires case.IsNonnom → more specific, wins over viLuNom in non-NOM.

Equations

• Aitha2026.viLuObl = { exponent := "ṭi", contextMatch := fun (ctx : Aitha2026.NContext) => ctx.rootClass == Aitha2026.StrongClass.luTi && decide ctx.case.IsNonnom, specificity := 2 }

def Aitha2026.viUNom : Morphology.DM.VI.VocabItem NContext Unit

VI rule for NOM n of the -u∼-i class.

Equations

• Aitha2026.viUNom = { exponent := "u", contextMatch := fun (ctx : Aitha2026.NContext) => ctx.rootClass == Aitha2026.StrongClass.uI, specificity := 1 }

def Aitha2026.viUObl : Morphology.DM.VI.VocabItem NContext Unit

VI rule for oblique n of the -u∼-i class.

Equations

• Aitha2026.viUObl = { exponent := "i", contextMatch := fun (ctx : Aitha2026.NContext) => ctx.rootClass == Aitha2026.StrongClass.uI && decide ctx.case.IsNonnom, specificity := 2 }

def Aitha2026.strongVIRules : List (Morphology.DM.VI.VocabItem NContext Unit)

All VI rules for strong noun n-exponents.

Equations

• Aitha2026.strongVIRules = [Aitha2026.viLuNom, Aitha2026.viLuObl, Aitha2026.viUNom, Aitha2026.viUObl]

def Aitha2026.mkNContext (rc : StrongClass) (c : TeluguCase) : NContext

Build the morphosyntactic context for VI from Telugu case + root class.

Equations

• Aitha2026.mkNContext rc c = { rootClass := rc, case := c }

theorem Aitha2026.vi_luTi_nom : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.luTi TeluguCase.nom) = some "lu"

theorem Aitha2026.vi_luTi_acc : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.luTi TeluguCase.acc) = some "ṭi"

theorem Aitha2026.vi_luTi_gen : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.luTi TeluguCase.gen) = some "ṭi"

theorem Aitha2026.vi_luTi_dat : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.luTi TeluguCase.dat) = some "ṭi"

theorem Aitha2026.vi_uI_nom : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.uI TeluguCase.nom) = some "u"

theorem Aitha2026.vi_uI_acc : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.uI TeluguCase.acc) = some "i"

theorem Aitha2026.vi_matches_strong_luTi (c : TeluguCase) : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.luTi c) = some (strongSurface luTiParadigm c)

VI produces the correct strong paradigm for -lu∼-ṭi nouns.

theorem Aitha2026.vi_matches_strong_uI (c : TeluguCase) : Morphology.DM.VI.vocabularyInsertSimple strongVIRules (mkNContext StrongClass.uI c) = some (strongSurface uIParadigm c)

VI produces the correct strong paradigm for -u∼-i nouns.

def Aitha2026.weakAllomorphyPattern : Morphology.Case.Allomorphy.AllomorphyPattern

The weak alternation's surface paradigm as an AllomorphyPattern. Short form = 0, long form = 1.

Equations

• Aitha2026.weakAllomorphyPattern = { nom := 0, acc := 1, gen := 0, dat := 1 }

theorem Aitha2026.weak_violates_aba : weakAllomorphyPattern.ViolatesABA

The weak alternation violates [Cah09]'s *ABA constraint. The ABAB pattern contains the subsequence A–B–A at NOM–ACC–GEN: NOM and GEN share the short form, but intervening ACC has the long form. Since GEN's representation contains ACC's on the containment hierarchy, this cannot arise from case-conditioned VI.

theorem Aitha2026.weak_not_contiguous : ¬weakAllomorphyPattern.IsContiguous

Therefore the weak alternation is not contiguous on the case containment hierarchy.

def Aitha2026.strongAllomorphyPattern : Morphology.Case.Allomorphy.AllomorphyPattern

In contrast, the strong alternation (ABB = NOM vs oblique) is contiguous — consistent with case-conditioned VI.

Equations

• Aitha2026.strongAllomorphyPattern = { nom := 0, acc := 1, gen := 1, dat := 1 }

theorem Aitha2026.strong_contiguous : strongAllomorphyPattern.IsContiguous

def Aitha2026.WeakStemForm.toNat : WeakStemForm → ℕ

Helper: encode WeakStemForm as a Nat for AllomorphyPattern comparison.

Equations

• Aitha2026.WeakStemForm.short.toNat = 0
• Aitha2026.WeakStemForm.long.toNat = 1

theorem Aitha2026.weak_pattern_from_paradigm : weakAllomorphyPattern = { nom := (weakParadigm TeluguCase.nom).toNat, acc := (weakParadigm TeluguCase.acc).toNat, gen := (weakParadigm TeluguCase.gen).toNat, dat := (weakParadigm TeluguCase.dat).toNat }

The weakAllomorphyPattern is not a separate stipulation — it is derived from weakParadigm. This theorem closes the gap between the paradigm data and the *ABA check.

inductive Aitha2026.FollowingContext : Type

Environments that trigger the long form in weak nouns. The long form surfaces when followed by a light syllable within the prosodic word — regardless of whether that syllable realizes a case suffix or an agreement suffix.

Data from [Ait26]'s full(er) paradigm including agreement:

• ACC -ni: light σ within Word → long (samudr-āni-ni)
• DAT -ki: light σ within Word → long (samudr-āni-ki)
• 1SG -ni: light σ within Word → long (samudr-āni-ni)
• 2SG -vi: light σ within Word → long (samudr-āni-vi)
• NOM -∅: no following σ → short (samudr-am-∅)
• GEN -∅: no following σ → short (samudr-am-∅)
• 3SG -∅: no following σ → short (samudr-am-∅)
• P -lō: separate Word → short (samudr-am-lō)
• P -gurinci: separate Word → short (samudr-am-gurinci)
• P -eduru: separate Word → short (samudr-am-eduru)

Note: -gurinci and -eduru begin with light syllables, yet still trigger the short form. The conditioning factor is Word membership, not syllable weight of the following element per se.

• noSuffix : FollowingContext
• lightWithinPrWd : FollowingContext
• separatePrWd : FollowingContext

@[implicit_reducible]

instance Aitha2026.instDecidableEqFollowingContext : DecidableEq FollowingContext

Equations

• Aitha2026.instDecidableEqFollowingContext x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instReprFollowingContext : Repr FollowingContext

Equations

• Aitha2026.instReprFollowingContext = { reprPrec := Aitha2026.instReprFollowingContext.repr }

def Aitha2026.instReprFollowingContext.repr : FollowingContext → ℕ → Std.Format

Equations

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

def Aitha2026.weakFormPredicted : FollowingContext → WeakStemForm

The phonological conditioning: long form iff followed by a light syllable within the same prosodic word.

Equations

• Aitha2026.weakFormPredicted Aitha2026.FollowingContext.lightWithinPrWd = Aitha2026.WeakStemForm.long
• Aitha2026.weakFormPredicted Aitha2026.FollowingContext.noSuffix = Aitha2026.WeakStemForm.short
• Aitha2026.weakFormPredicted Aitha2026.FollowingContext.separatePrWd = Aitha2026.WeakStemForm.short

theorem Aitha2026.light_suffix_triggers_long : weakFormPredicted FollowingContext.lightWithinPrWd = WeakStemForm.long

Both ACC -ni (case) and 1SG -ni (agreement) trigger the long form — the conditioning is phonological, not morphosyntactic.

theorem Aitha2026.no_suffix_triggers_short : weakFormPredicted FollowingContext.noSuffix = WeakStemForm.short

No following suffix → short form.

theorem Aitha2026.separate_prwd_triggers_short : weakFormPredicted FollowingContext.separatePrWd = WeakStemForm.short

Postposition in a separate Word → short form (regardless of whether the postposition starts with a light or heavy syllable).

inductive Aitha2026.AgrSuffix : Type

Telugu nominal predicative agreement suffixes. Only 1SG and 2SG are overt; 3SG and all plurals are null. Data from [Ait26].

• sg1 : AgrSuffix
• sg2 : AgrSuffix
• sg3 : AgrSuffix

@[implicit_reducible]

instance Aitha2026.instDecidableEqAgrSuffix : DecidableEq AgrSuffix

Equations

• Aitha2026.instDecidableEqAgrSuffix x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprAgrSuffix.repr : AgrSuffix → ℕ → Std.Format

Equations

• Aitha2026.instReprAgrSuffix.repr Aitha2026.AgrSuffix.sg1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.AgrSuffix.sg1")).group prec✝
• Aitha2026.instReprAgrSuffix.repr Aitha2026.AgrSuffix.sg2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.AgrSuffix.sg2")).group prec✝
• Aitha2026.instReprAgrSuffix.repr Aitha2026.AgrSuffix.sg3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.AgrSuffix.sg3")).group prec✝

@[implicit_reducible]

instance Aitha2026.instReprAgrSuffix : Repr AgrSuffix

Equations

• Aitha2026.instReprAgrSuffix = { reprPrec := Aitha2026.instReprAgrSuffix.repr }

def Aitha2026.AgrSuffix.toFollowing : AgrSuffix → FollowingContext

Classify agreement suffixes by their phonological context: overt light suffixes pattern identically to overt light case suffixes.

Equations

• Aitha2026.AgrSuffix.sg1.toFollowing = Aitha2026.FollowingContext.lightWithinPrWd
• Aitha2026.AgrSuffix.sg2.toFollowing = Aitha2026.FollowingContext.lightWithinPrWd
• Aitha2026.AgrSuffix.sg3.toFollowing = Aitha2026.FollowingContext.noSuffix

theorem Aitha2026.agr_1sg_triggers_long : weakFormPredicted AgrSuffix.sg1.toFollowing = WeakStemForm.long

1SG -ni triggers the long form, just like ACC -ni. Both are light syllables within Word — the conditioning is phonological, not morphosyntactic.

theorem Aitha2026.agr_3sg_triggers_short : weakFormPredicted AgrSuffix.sg3.toFollowing = WeakStemForm.short

3SG -∅ triggers the short form, just like NOM -∅.

theorem Aitha2026.case_agr_identity : AgrSuffix.sg1.toFollowing = FollowingContext.lightWithinPrWd ∧ weakFormPredicted AgrSuffix.sg1.toFollowing = weakFormPredicted FollowingContext.lightWithinPrWd

The decisive argument: case and agreement suffixes with identical phonological shape produce identical stem forms. ACC -ni and 1SG -ni both map to lightWithinPrWd, so both trigger the long form. If the alternation were case-conditioned, agreement suffixes (which bear no case features) could not trigger it.

structure Aitha2026.WeakUnderlying : Type

The underlying representation of the weak noun stem. [Ait26] argues (§4.2) that the surface alternants -am and -āni derive from a single underlying form: the concatenation of -am (exponent of n) + -ni (singular suffix, exponent of Num).

The surface forms result from TWO independent phonological processes:

1. The -am ~ -ā alternation: compensatory lengthening after deletion of the coda nasal (Stem-level vowel hiatus resolution)
2. The -ni ~ -∅ alternation: deletion of stressed light syllables that cannot form a binary foot (Word-level phonology)

This unified underlying form means the "stem alternation" is not a single alternation at all, but the combined effect of two regular phonological processes acting on the same input.

• nExponent : String
• sgSuffix : String

def Aitha2026.weakUnderlying : WeakUnderlying

All weak nouns share the same underlying -am-ni.

Equations

• Aitha2026.weakUnderlying = { nExponent := "am", sgSuffix := "ni" }

inductive Aitha2026.LocalityType : Type

The two alternations differ in their sensitivity to locality. [Ait26] (§4.1) shows this via Q-postposing constructions:

• Strong: oblique can be triggered across an intervening quantifier (structural locality — the case head c-commands n)
• Weak: the alternation is determined by the linearly adjacent syllable, not by structural position

This difference supports the claim that the strong alternation is morphosyntactic (structural, can skip intervening material) while the weak alternation is phonological (linear adjacency required).

• structural : LocalityType
• linear : LocalityType

@[implicit_reducible]

instance Aitha2026.instDecidableEqLocalityType : DecidableEq LocalityType

Equations

• Aitha2026.instDecidableEqLocalityType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instReprLocalityType : Repr LocalityType

Equations

• Aitha2026.instReprLocalityType = { reprPrec := Aitha2026.instReprLocalityType.repr }

def Aitha2026.instReprLocalityType.repr : LocalityType → ℕ → Std.Format

Equations

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

def Aitha2026.strongLocality : LocalityType

Equations

• Aitha2026.strongLocality = Aitha2026.LocalityType.structural

def Aitha2026.weakLocality : LocalityType

Equations

• Aitha2026.weakLocality = Aitha2026.LocalityType.linear

theorem Aitha2026.locality_differs : strongLocality ≠ weakLocality

inductive Aitha2026.StemCandidate : Type

Candidates for the Stem-level metrical parse of samudr-am 'ocean-n' (underlying syllable weights: CV.CV.CVC = L.L.H).

• llU_H : StemCandidate

  (ˈsa.mu).dram — one bimoraic foot, final H unparsed.

• l_l_H : StemCandidate

  (ˈsa).(ˌmu).(ˌdram) — two degenerate feet + one bimoraic.

• ll_H : StemCandidate

  (ˈsa.mu).(ˌdram) — two bimoraic feet. Optimal.

@[implicit_reducible]

instance Aitha2026.instDecidableEqStemCandidate : DecidableEq StemCandidate

Equations

• Aitha2026.instDecidableEqStemCandidate x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprStemCandidate.repr : StemCandidate → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aitha2026.instReprStemCandidate : Repr StemCandidate

Equations

• Aitha2026.instReprStemCandidate = { reprPrec := Aitha2026.instReprStemCandidate.repr }

def Aitha2026.StemCandidate.toFooting : StemCandidate → Prosody.Footing Prosody.Syllable.Weight

Map each candidate to its canonical Prosody.Footing over weighted σ (feet are Prosody.Foots; an unfooted σ is a bare weight).

Equations

• One or more equations did not get rendered due to their size.
• Aitha2026.StemCandidate.llU_H.toFooting = [Sum.inl { syllables := [Prosody.Syllable.Weight.light, Prosody.Syllable.Weight.light], head := 0 }, Sum.inr Prosody.Syllable.Weight.heavy]

def Aitha2026.allFtLeftOf (fc : Prosody.Footing Prosody.Syllable.Weight) : ℕ

ALL-FT-LEFT: per foot, the σ intervening from the left edge of the domain.

Equations

• Aitha2026.allFtLeftOf fc = Aitha2026.allFtLeftOf.go fc 0

def Aitha2026.allFtLeftOf.go : Prosody.Footing Prosody.Syllable.Weight → ℕ → ℕ

Equations

• Aitha2026.allFtLeftOf.go [] a✝ = 0
• Aitha2026.allFtLeftOf.go (Sum.inl f :: rest) a✝ = a✝ + Aitha2026.allFtLeftOf.go rest (a✝ + f.syllables.length)
• Aitha2026.allFtLeftOf.go (Sum.inr val :: rest) a✝ = Aitha2026.allFtLeftOf.go rest (a✝ + 1)

def Aitha2026.cFtBin : Constraints.Constraint StemCandidate

FT-BIN(μ): penalizes non-bimoraic feet (a foot whose morae ≠ 2).

Equations

• Aitha2026.cFtBin c = (List.filter (fun (f : Prosody.Foot ℕ) => decide (Prosody.Foot.moraCount id f ≠ 2)) c.toFooting.feet).length

def Aitha2026.cParseSyl : Constraints.Constraint StemCandidate

PARSE-SYL: penalizes unparsed (stray) syllables.

Equations

• Aitha2026.cParseSyl c = c.toFooting.strays.length

def Aitha2026.cAllFtLeft : Constraints.Constraint StemCandidate

ALL-FT-LEFT: penalizes feet distant from the left edge.

Equations

• Aitha2026.cAllFtLeft c = Aitha2026.allFtLeftOf c.toFooting

def Aitha2026.stemRanking : List (Constraints.Constraint StemCandidate)

Stem-level constraint ranking: FT-BIN ≫ PARSE-SYL ≫ ALL-FT-LEFT.

FT-BIN dominates PARSE-SYL: it is better to leave a syllable unparsed than to create a degenerate (monomoraic) foot.

Equations

• Aitha2026.stemRanking = [Aitha2026.cFtBin, Aitha2026.cParseSyl, Aitha2026.cAllFtLeft]

def Aitha2026.stemCandidates : List StemCandidate

Equations

• Aitha2026.stemCandidates = [Aitha2026.StemCandidate.llU_H, Aitha2026.StemCandidate.l_l_H, Aitha2026.StemCandidate.ll_H]

theorem Aitha2026.stemCandidates_ne : stemCandidates ≠ []

theorem Aitha2026.stem_ftbin_violations : List.map cFtBin stemCandidates = [0, 2, 0]

Violation profiles for Stem-level candidates:

Candidate	FT-BIN	PARSE-SYL	ALL-FT-LEFT
(ˈsa.mu).dram	0	1*	0
(ˈsa).(ˌmu).(ˌdram)	2*	0	0+1+2
☞ (ˈsa.mu).(ˌdram)	0	0	0+2

theorem Aitha2026.stem_parsesyl_violations : List.map cParseSyl stemCandidates = [1, 0, 0]

theorem Aitha2026.stem_optimal : (OptimalityTheory.Tableau.ofRanking stemCandidates stemRanking stemCandidates_ne).optimal = {StemCandidate.ll_H}

The optimal Stem-level parse is (ˈsa.mu).(ˌdram): two well-formed moraic trochees, (LL)(H), with no unparsed syllables.

structure Aitha2026.ProsodicPrespec : Type

Prosodic prespecification for a morphological exponent. none means the property is unspecified (determined by the phonological grammar alone).

• inherentStress : Option Bool

def Aitha2026.instDecidableEqProsodicPrespec.decEq (x✝ x✝¹ : ProsodicPrespec) : Decidable (x✝ = x✝¹)

Equations

• Aitha2026.instDecidableEqProsodicPrespec.decEq { inherentStress := a } { inherentStress := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instDecidableEqProsodicPrespec : DecidableEq ProsodicPrespec

Equations

• Aitha2026.instDecidableEqProsodicPrespec = Aitha2026.instDecidableEqProsodicPrespec.decEq

@[implicit_reducible]

instance Aitha2026.instReprProsodicPrespec : Repr ProsodicPrespec

Equations

• Aitha2026.instReprProsodicPrespec = { reprPrec := Aitha2026.instReprProsodicPrespec.repr }

def Aitha2026.instReprProsodicPrespec.repr : ProsodicPrespec → ℕ → Std.Format

Equations

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

structure Aitha2026.RichExponent : Type

A rich exponent: segmental content plus optional prosodic prespecification. Used here for Telugu singular -ni's lexically prespecified stress ([Ait26] §5; precedent [Ald99] on English stress-shifting suffixes).

• segments : String
• prosody : ProsodicPrespec

def Aitha2026.instDecidableEqRichExponent.decEq (x✝ x✝¹ : RichExponent) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Aitha2026.instDecidableEqRichExponent : DecidableEq RichExponent

Equations

• Aitha2026.instDecidableEqRichExponent = Aitha2026.instDecidableEqRichExponent.decEq

@[implicit_reducible]

instance Aitha2026.instReprRichExponent : Repr RichExponent

Equations

• Aitha2026.instReprRichExponent = { reprPrec := Aitha2026.instReprRichExponent.repr }

def Aitha2026.instReprRichExponent.repr : RichExponent → ℕ → Std.Format

Equations

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

def Aitha2026.RichExponent.stressed (s : String) : RichExponent

Create a stressed exponent.

Equations

• Aitha2026.RichExponent.stressed s = { segments := s, prosody := { inherentStress := some true } }

def Aitha2026.sgNiExponent : RichExponent

The singular suffix -ni carries prespecified stress. This prespecification, interacting with FT-BIN(μ) and IDENT-STRESS at the Word level, drives deletion of -ni when it is Word-final and cannot form a binary foot.

Equations

• Aitha2026.sgNiExponent = Aitha2026.RichExponent.stressed "ni"

theorem Aitha2026.sgNi_is_stressed : sgNiExponent.prosody.inherentStress = some true

inductive Aitha2026.WordCandNom : Type

Word-level candidates for the NOM input (ˈsa.mu).(ˌdram).ní. Stressed -ni is Word-final: no following suffix to pair with.

• destress : WordCandNom

  (ˈsa.mu).(ˌdram).ni — stress on -ni removed.

• degenerateFoot : WordCandNom

  (ˈsa.mu).(ˌdram).(ˌní) — -ni as degenerate (monomoraic) foot.

• deleteI_coda : WordCandNom

  (ˈsa.mu).(ˌdramn) — nucleic /i/ deleted, /n/ joins coda → complex.

• deleteIM : WordCandNom

  (ˈsa.mu).(ˌdran) — /i/ and /m/ deleted, Stem edge misaligned.

• deleteNi : WordCandNom

  ☞ (ˈsa.mu).(ˌdram) — /ni/ fully deleted.

@[implicit_reducible]

instance Aitha2026.instDecidableEqWordCandNom : DecidableEq WordCandNom

Equations

• Aitha2026.instDecidableEqWordCandNom x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprWordCandNom.repr : WordCandNom → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aitha2026.instReprWordCandNom : Repr WordCandNom

Equations

• Aitha2026.instReprWordCandNom = { reprPrec := Aitha2026.instReprWordCandNom.repr }

def Aitha2026.wordNomRanking : List (Constraints.Constraint WordCandNom)

Word-level ranking for NOM.

Candidate	ID-STR	FT-BIN	*CxCODA	AL-R	MAX(μ)	MAX
destress	1*
degenerateFoot		1*
deleteI_coda			1*		1	1
deleteIM				1*	2	2
☞ deleteNi					1	2

Equations

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

def Aitha2026.wordNomCands : List WordCandNom

Equations

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

theorem Aitha2026.wordNomCands_ne : wordNomCands ≠ []

theorem Aitha2026.wordNom_optimal : (OptimalityTheory.Tableau.ofRanking wordNomCands wordNomRanking wordNomCands_ne).optimal = {WordCandNom.deleteNi}

Word level, NOM: Word-final stressed -ni is deleted. Surface: samudr-am (short form).

inductive Aitha2026.WordCandDat : Type

Word-level candidates for the DAT input (ˈsa.mu).(ˌdram).ní.ki. The light suffix -ki is Word-internal, so -ni can form a bimoraic foot (ˌní.ki) — but the /mn/ boundary violates *DIST-0.

• faithful : WordCandDat

  (ˈsa.mu).(ˌdram).(ˌní.ki) — faithful. /mn/ boundary retained.

• resyllabify : WordCandDat

  (ˈsa.mu).(ˌdra).(ˌmí.ki) — /m/ resyllabified as onset.

• deleteNi : WordCandDat

  (ˈsa.mu).(ˌdram).ki — /ni/ deleted, -ki degenerate.

• compLengthen : WordCandDat

  ☞ (ˈsa.mu).(ˌdrā).(ˌní.ki) — /m/ deleted, /a/→/ā/ (CL).

@[implicit_reducible]

instance Aitha2026.instDecidableEqWordCandDat : DecidableEq WordCandDat

Equations

• Aitha2026.instDecidableEqWordCandDat x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instReprWordCandDat : Repr WordCandDat

Equations

• Aitha2026.instReprWordCandDat = { reprPrec := Aitha2026.instReprWordCandDat.repr }

def Aitha2026.instReprWordCandDat.repr : WordCandDat → ℕ → Std.Format

Equations

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

inductive Aitha2026.Con : Type

The constraint inventory of [Ait26], as a label type: cross-stratum identity is by label, not by candidate type (the strata have different candidate types). The paper's tables abbreviate stress faithfulness as both ID-STR and IDENT-STRESS; both spellings are preserved as distinct labels.

• distZero : Con
• alignR : Con
• idStress : Con
• ftBin : Con
• maxMora : Con
• max : Con
• identStress : Con

@[implicit_reducible]

instance Aitha2026.instDecidableEqCon : DecidableEq Con

Equations

• Aitha2026.instDecidableEqCon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprCon.repr : Con → ℕ → Std.Format

Equations

• Aitha2026.instReprCon.repr Aitha2026.Con.distZero prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.distZero")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.alignR prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.alignR")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.idStress prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.idStress")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.ftBin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.ftBin")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.maxMora prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.maxMora")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.max prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.max")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.identStress prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.identStress")).group prec✝

@[implicit_reducible]

instance Aitha2026.instReprCon : Repr Con

Equations

• Aitha2026.instReprCon = { reprPrec := Aitha2026.instReprCon.repr }

def Aitha2026.wordDatRanking : List (Con × Constraints.Constraint WordCandDat)

Word-level ranking for DAT. Same constraint set as NOM, with *DIST-0 additionally relevant (eliminates faithful candidate).

Candidate	*DIST-0	AL-R	ID-STR	FT-BIN	MAX(μ)	MAX
faithful	1*
resyllabify		1*
deleteNi				1*	1	2
☞ compLengthen					1	1

Equations

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

def Aitha2026.wordDatCands : List WordCandDat

Equations

• Aitha2026.wordDatCands = [Aitha2026.WordCandDat.faithful, Aitha2026.WordCandDat.resyllabify, Aitha2026.WordCandDat.deleteNi, Aitha2026.WordCandDat.compLengthen]

theorem Aitha2026.wordDatCands_ne : wordDatCands ≠ []

theorem Aitha2026.wordDat_optimal : (OptimalityTheory.Tableau.ofRanking wordDatCands (List.map (fun (x : Con × Constraints.Constraint WordCandDat) => x.2) wordDatRanking) wordDatCands_ne).optimal = {WordCandDat.compLengthen}

Word level, DAT: /mn/ boundary repaired by compensatory lengthening. Surface: samudr-āni-ki (long form).

theorem Aitha2026.word_level_derives_alternation : (OptimalityTheory.Tableau.ofRanking wordNomCands wordNomRanking wordNomCands_ne).optimal = {WordCandNom.deleteNi} ∧ (OptimalityTheory.Tableau.ofRanking wordDatCands (List.map (fun (x : Con × Constraints.Constraint WordCandDat) => x.2) wordDatRanking) wordDatCands_ne).optimal = {WordCandDat.compLengthen}

The same constraint system derives both surface forms from the same underlying -am-ni. The difference is purely phonological: whether a light suffix follows within the Word.

• NOM (no suffix): -ni is Word-final → deleted → short
• DAT (-ki follows): -ni pairs with -ki → /mn/ repaired → long

This completes the derivation that the weakFormPredicted function (§3) stipulates: the alternation is now DERIVED from OT constraint interaction, not encoded by fiat.

def Aitha2026.WordCandNom.toStemForm : WordCandNom → WeakStemForm

Map Word-level optimal outputs to WeakStemForm. NOM deleteNi = short (the -ni is gone, surface is -am). DAT compLengthen = long (the -am becomes -ā, -ni survives as -āni).

Equations

• Aitha2026.WordCandNom.deleteNi.toStemForm = Aitha2026.WeakStemForm.short
• x✝.toStemForm = Aitha2026.WeakStemForm.long

def Aitha2026.WordCandDat.toStemForm : WordCandDat → WeakStemForm

Equations

• Aitha2026.WordCandDat.compLengthen.toStemForm = Aitha2026.WeakStemForm.long
• x✝.toStemForm = Aitha2026.WeakStemForm.short

theorem Aitha2026.nom_produces_short : WordCandNom.deleteNi.toStemForm = WeakStemForm.short

theorem Aitha2026.dat_produces_long : WordCandDat.compLengthen.toStemForm = WeakStemForm.long

Paper §5.3 develops the Phrase-level stratum, where constraint ranking is reranked relative to the Word level. This is the empirical core of the "Stratal" claim: the same constraint inventory (*DIST-0, MAX, IDENT-STRESS, ...) is demoted or promoted across the Word→Phrase boundary, producing different optimal outputs for the same segmental configuration.

Key reranking from paper §5.3: *DIST-0 is demoted from above MAX at the Word level (deriving m-deletion before singular -ni) to below MAX at the Phrase level (tolerating m-n contact across postposition boundary). This subsection encodes paper tableau (66) for samudram nunci 'from ocean': the Phrase-level grammar tolerates the m-n contact across the postposition boundary that the Word-level grammar would have repaired by compensatory lengthening.

inductive Aitha2026.PhraseCandPostp : Type

Phrase-level candidates for the postpositional input ('sa.mu).('dram).('nun).('ci) ('ocean-from'), the Word-level output of the NOM stratum concatenated with the postposition -nunci 'from'.

• compLengthen : PhraseCandPostp

  (ˈsa.mu).(ˌdrā).(ˌnun).(ˌci) — /m/ deleted, /a/ → /ā/ via CL.

• deleteM : PhraseCandPostp

  (ˈsa.mu).(ˌdra).(ˌnun).(ˌci) — /m/ deleted, no CL.

• deleteN : PhraseCandPostp

  (ˈsa.mu).(ˌdram).(ˌun).(ˌci) — /n/ of postposition deleted.

• faithful : PhraseCandPostp

  ☞ (ˈsa.mu).(ˌdram).(ˌnun).(ˌci) — faithful; m-n contact retained.

@[implicit_reducible]

instance Aitha2026.instDecidableEqPhraseCandPostp : DecidableEq PhraseCandPostp

Equations

• Aitha2026.instDecidableEqPhraseCandPostp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Aitha2026.instReprPhraseCandPostp.repr : PhraseCandPostp → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Aitha2026.instReprPhraseCandPostp : Repr PhraseCandPostp

Equations

• Aitha2026.instReprPhraseCandPostp = { reprPrec := Aitha2026.instReprPhraseCandPostp.repr }

def Aitha2026.phrasePostpRanking : List (Con × Constraints.Constraint PhraseCandPostp)

Phrase-level ranking for postposition contexts.

Crucially, *DIST-0 is now below MAX — the reverse of the Word stratum (file:584). This is the headline cross-stratum reranking of paper §5.3.

Candidate	IDENT-STRESS	MAX	*DIST-0	AL-R
compLengthen		1*		1
deleteM		1		1
deleteN		1
☞ faithful			1

Equations

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

def Aitha2026.phrasePostpCands : List PhraseCandPostp

Equations

• Aitha2026.phrasePostpCands = [Aitha2026.PhraseCandPostp.compLengthen, Aitha2026.PhraseCandPostp.deleteM, Aitha2026.PhraseCandPostp.deleteN, Aitha2026.PhraseCandPostp.faithful]

theorem Aitha2026.phrasePostpCands_ne : phrasePostpCands ≠ []

theorem Aitha2026.phrasePostp_optimal : (OptimalityTheory.Tableau.ofRanking phrasePostpCands (List.map (fun (x : Con × Constraints.Constraint PhraseCandPostp) => x.2) phrasePostpRanking) phrasePostpCands_ne).optimal = {PhraseCandPostp.faithful}

Phrase level: postposition nunci 'from'. The faithful output wins — *DIST-0 is demoted below MAX at Phrase level, so m-n contact is tolerated rather than repaired. Surface: samudram nunci.

Wires the existing per-stratum tableaux into StratalDerivation records — making the file's "Stratal OT" claim explicit at the type level. Each derivation records the optimal output at each cycle; the candidate types differ across strata because GEN produces different representations at each level.

def Aitha2026.nomDerivation : OptimalityTheory.Stratal.StratalDerivation StemCandidate WordCandNom WordCandNom

The Stratal-OT derivation of NOM samudram 'ocean-NOM'.

• Stem: input /samudr-am/, optimal parse (ˈsa.mu).(ˌdram) (= .ll_H).
• Word: stem output combined with prosodified -ni singular suffix and a null NOM exponent; Word-final stressed -ni is deleted; output samudram (= .deleteNi).
• Phrase: no overt postposition follows, so no Phrase-level repairs are required. Surface = Word output.

Equations

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

def Aitha2026.datDerivation : OptimalityTheory.Stratal.StratalDerivation StemCandidate WordCandDat WordCandDat

DAT derivation samudrāniki — Word-level CL produces the long form via m-deletion + /a/ → /ā/.

Equations

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

def Aitha2026.postpDerivation : OptimalityTheory.Stratal.StratalDerivation StemCandidate WordCandNom PhraseCandPostp

Postpositional derivation samudram nunci — Phrase-level reranking blocks the Word-level CL repair. Same input segmental shape as DAT at the m-n contact, different output because *DIST-0 is demoted at Phrase.

Equations

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

theorem Aitha2026.derivations_share_stem : nomDerivation.stemOutput = datDerivation.stemOutput ∧ nomDerivation.stemOutput = postpDerivation.stemOutput

The three derivations agree at the stem stratum (same input shape) but diverge at later strata depending on what follows the noun.

Paper §5.3 (p. 31) makes the headline Stratal-OT claim that *DIST-0 is demoted going from the Word stratum to the Phrase stratum. The substrate's IsPromotedAcross / IsDemotedAcross operate on constraint labels — necessary here because wordDatRanking and phrasePostpRanking have different candidate types (WordCandDat vs PhraseCandPostp), so the same-C isPromoted/isDemoted would not typecheck.

theorem Aitha2026.dist0_demoted_phrase_relative_to_word : OptimalityTheory.Stratal.IsDemotedAcross Con.distZero phrasePostpRanking wordDatRanking

*DIST-0 is at the highest rank in the Word DAT ranking (wordDatRanking, position 0) and at a lower rank in the Phrase postpositional ranking (phrasePostpRanking, position 2). This is the demotion across the Word→Phrase boundary that the paper's §5.3 central reranking claim makes — and it is precisely what derives m-retention at phrase boundaries vs m-deletion + CL inside the prosodic word.

theorem Aitha2026.max_promoted_phrase_relative_to_word : OptimalityTheory.Stratal.IsPromotedAcross Con.max phrasePostpRanking wordDatRanking

Conversely, MAX is promoted going Word → Phrase. Dual aspect of the same reranking.

inductive Aitha2026.WordMembership : Type

Prosodic-word membership of a following element: parsed inside the host ω (stem, derivational/inflectional/agreement suffixes) or forming its own ω (postpositions). The conditioning dimension is prosodic, not morphosyntactic ([Ait26] §3.2).

• internal : WordMembership
• external : WordMembership

@[implicit_reducible]

instance Aitha2026.instDecidableEqWordMembership : DecidableEq WordMembership

Equations

• Aitha2026.instDecidableEqWordMembership x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Aitha2026.instReprWordMembership : Repr WordMembership

Equations

• Aitha2026.instReprWordMembership = { reprPrec := Aitha2026.instReprWordMembership.repr }

def Aitha2026.instReprWordMembership.repr : WordMembership → ℕ → Std.Format

Equations

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

structure Aitha2026.MorphElement : Type

A following morphological element: its ω-membership and the weight of its initial syllable — the Telugu weak-noun long-form conditioning.

• membership : WordMembership
• initialWeight : Prosody.Syllable.Weight

def Aitha2026.instDecidableEqMorphElement.decEq (x✝ x✝¹ : MorphElement) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Aitha2026.instDecidableEqMorphElement : DecidableEq MorphElement

Equations

• Aitha2026.instDecidableEqMorphElement = Aitha2026.instDecidableEqMorphElement.decEq

@[implicit_reducible]

instance Aitha2026.instReprMorphElement : Repr MorphElement

Equations

• Aitha2026.instReprMorphElement = { reprPrec := Aitha2026.instReprMorphElement.repr }

def Aitha2026.instReprMorphElement.repr : MorphElement → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Aitha2026.MorphElement.triggersLongForm (m : MorphElement) : Prop

The long stem form surfaces iff the following element is ω-internal and begins with a light syllable; ω-external postpositions never trigger it, even with a light initial syllable.

Equations

• m.triggersLongForm = (m.membership = Aitha2026.WordMembership.internal ∧ m.initialWeight = Prosody.Syllable.Weight.light)

def Aitha2026.weakSurfaceFromPrWd : Option MorphElement → WeakStemForm

Predict the weak stem form from the following morphological element: the long form surfaces iff the following element is ω-internal AND begins with a light syllable.

Equations

• Aitha2026.weakSurfaceFromPrWd (some m) = if m.triggersLongForm then Aitha2026.WeakStemForm.long else Aitha2026.WeakStemForm.short
• Aitha2026.weakSurfaceFromPrWd none = Aitha2026.WeakStemForm.short

theorem Aitha2026.acc_ni_long : weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.long

theorem Aitha2026.dat_ki_long : weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.long

theorem Aitha2026.nom_null_short : weakSurfaceFromPrWd none = WeakStemForm.short

theorem Aitha2026.gen_null_short : weakSurfaceFromPrWd none = WeakStemForm.short

theorem Aitha2026.agr_1sg_ni_long : weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.long

theorem Aitha2026.agr_2sg_vi_long : weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.long

theorem Aitha2026.postp_lo_short : weakSurfaceFromPrWd (some { membership := WordMembership.external, initialWeight := Prosody.Syllable.Weight.heavy }) = WeakStemForm.short

theorem Aitha2026.postp_gurinci_short : weakSurfaceFromPrWd (some { membership := WordMembership.external, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.short

Postposition -gurinci 'about' begins with a light syllable, yet triggers the short form — because it is Word-external. This is the key evidence that the conditioning is Word membership, not syllable weight alone.

theorem Aitha2026.prwd_matches_paradigm : weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.long ∧ weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = WeakStemForm.long ∧ weakSurfaceFromPrWd none = WeakStemForm.short ∧ weakSurfaceFromPrWd none = WeakStemForm.short ∧ weakSurfaceFromPrWd (some { membership := WordMembership.external, initialWeight := Prosody.Syllable.Weight.heavy }) = WeakStemForm.short

The Word-based prediction matches the original paradigm data for all five cases in the canonical weak paradigm.

theorem Aitha2026.prwd_agrees_with_paradigm : weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = weakParadigm TeluguCase.acc ∧ weakSurfaceFromPrWd (some { membership := WordMembership.internal, initialWeight := Prosody.Syllable.Weight.light }) = weakParadigm TeluguCase.dat ∧ weakSurfaceFromPrWd none = weakParadigm TeluguCase.nom ∧ weakSurfaceFromPrWd none = weakParadigm TeluguCase.gen ∧ weakSurfaceFromPrWd (some { membership := WordMembership.external, initialWeight := Prosody.Syllable.Weight.heavy }) = weakParadigm TeluguCase.loc

The Word-based prediction agrees with the original weakParadigm for all five cases. This closes the gap between the phonological derivation (OT + Word) and the empirical data (paradigm).

theorem Aitha2026.strong_vs_weak_distinction : strongAllomorphyPattern.IsContiguous ∧ ¬weakAllomorphyPattern.IsContiguous

The two alternation patterns have fundamentally different analyses:

1. Strong alternation: ABB pattern (contiguous on containment hierarchy) → case-conditioned contextual allomorphy (VI).
2. Weak alternation: ABAB pattern (violates *ABA) → phonological alternation conditioned by syllable weight within Word.

The strong alternation depends on structural position (Elsewhere Condition + ACC feature); the weak alternation depends on linear adjacency to a light syllable (phonological locality).

theorem Aitha2026.weak_is_outward_sensitive : Morphology.DM.VI.isOutwardSensitive 2 1 = true

The outward sensitivity of the weak alternation: the form of n (closer to root) depends on material further from the root (case and agreement suffixes). Under root-out VI, this is impossible — suffixes are not yet inserted when n receives its exponent.

theorem Aitha2026.vi_derives_strong_pattern : (if (strongSurface luTiParadigm TeluguCase.nom == strongSurface luTiParadigm TeluguCase.nom) = true then 0 else 1, if (strongSurface luTiParadigm TeluguCase.acc == strongSurface luTiParadigm TeluguCase.nom) = true then 0 else 1, if (strongSurface luTiParadigm TeluguCase.gen == strongSurface luTiParadigm TeluguCase.nom) = true then 0 else 1, if (strongSurface luTiParadigm TeluguCase.dat == strongSurface luTiParadigm TeluguCase.nom) = true then 0 else 1) = (0, 1, 1, 1)

The strong alternation pattern derived from VI output matches the strongAllomorphyPattern used for the *ABA check. This is the end-to-end chain: VI rules → surface forms → ABB pattern → contiguous.

The proof constructs the pattern from strongSurface by checking whether each case gets the NOM form (= 0) or the OBL form (= 1).

theorem Aitha2026.central_argument : strongAllomorphyPattern.IsContiguous ∧ ¬weakAllomorphyPattern.IsContiguous ∧ Morphology.DM.VI.isOutwardSensitive 2 1 = true

End-to-end argumentation chain:

1. Strong alternation: VI derives ABB → contiguous → valid case allomorphy
2. Weak alternation: ABAB pattern → non-contiguous → cannot be case allomorphy
3. Weak alternation: outward-sensitive → incompatible with root-out VI
4. THEREFORE: weak alternation is phonological, not morphological

def Aitha2026.teluguWBP : Bool

Telugu has Weight by Position: coda consonants bear morae, making CVC syllables heavy. This is assumed by the Stem-level parse, where dram (CVC) is treated as heavy (2μ).

Equations

• Aitha2026.teluguWBP = true

theorem Aitha2026.telugu_coda_deletion_strands_mora (o n c : Phonology.Segment) : ((Prosody.Syllable.ofCV [o] [n] [c] teluguWBP ⋯).strand 1).strandedCount = 1

In a WBP language like Telugu, deleting a coda consonant strands one mora — this is [Hay89]'s classical CL.

This grounds the DAT compLengthen candidate: /m/ deletion from /dram/ strands a mora, which spreads left to yield /drā/. The CL repair is not a stipulated candidate — it is available precisely because Telugu has WBP.

theorem Aitha2026.telugu_cl_conservation (o n c : Phonology.Segment) : have σ := Prosody.Syllable.ofCV [o] [n] [c] teluguWBP ⋯; σ.moraCount = (σ.strand 1).relicense.moraCount

Moraic conservation ([Hay89]): the mora stranded by /m/ deletion is absorbed by leftward spreading to /a/, yielding /ā/ (2μ). Total mora count is unchanged.

All three Telugu OT tableaux lift to generic ConstraintSystems via tableauSystem. The Stratal-OT derivation of the weak alternation becomes a probability-1 claim per stratum.

noncomputable def Aitha2026.stemSystem : Core.Optimization.ConstraintSystem StemCandidate (Core.Optimization.LexProfile ℕ 3)

Stem-level metrical parse tableau as a generic ConstraintSystem.

Equations

• Aitha2026.stemSystem = OptimalityTheory.tableauSystem (OptimalityTheory.Tableau.ofRanking Aitha2026.stemCandidates Aitha2026.stemRanking Aitha2026.stemCandidates_ne)

theorem Aitha2026.stemSystem_predict_ll_H : stemSystem.predict StemCandidate.ll_H = 1

Probability 1 on (LL)(H): two well-formed moraic trochees.

noncomputable def Aitha2026.wordNomSystem : Core.Optimization.ConstraintSystem WordCandNom (Core.Optimization.LexProfile ℕ 6)

Word-level NOM tableau as a generic ConstraintSystem.

Equations

• Aitha2026.wordNomSystem = OptimalityTheory.tableauSystem (OptimalityTheory.Tableau.ofRanking Aitha2026.wordNomCands Aitha2026.wordNomRanking Aitha2026.wordNomCands_ne)

theorem Aitha2026.wordNomSystem_predict_deleteNi : wordNomSystem.predict WordCandNom.deleteNi = 1

Probability 1 on deleteNi: Word-final stressed -ni is deleted.

noncomputable def Aitha2026.wordDatSystem : Core.Optimization.ConstraintSystem WordCandDat (Core.Optimization.LexProfile ℕ 6)

Word-level DAT tableau as a generic ConstraintSystem.

Equations

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

theorem Aitha2026.wordDatSystem_predict_compLengthen : wordDatSystem.predict WordCandDat.compLengthen = 1

Probability 1 on compLengthen: /m/ deletion + CL yields -āni.