The Nouns that Say -ni @cite{aitha-2026}

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 @cite{mcfadden-2018}'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 @cite{caha-2009}'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 (@cite{kiparsky-2000}): 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: PrWd-based surface form prediction

inductive Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase : Type

Telugu case values relevant to nominal paradigms.

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqTeluguCase : DecidableEq TeluguCase

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqTeluguCase : BEq TeluguCase

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqTeluguCase = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqTeluguCase.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqTeluguCase.beq : TeluguCase → TeluguCase → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqTeluguCase.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Allomorphy.Studies.Aitha2026.instReprTeluguCase.repr : TeluguCase → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprTeluguCase : Repr TeluguCase

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprTeluguCase = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprTeluguCase.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.toCore : TeluguCase → Core.Case

Map Telugu cases to the core Case type.

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.nom.toCore = Core.Case.nom
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.acc.toCore = Core.Case.acc
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.gen.toCore = Core.Case.gen
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.dat.toCore = Core.Case.dat
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.loc.toCore = Core.Case.loc

def Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.hasACC : TeluguCase → Bool

Does this Telugu case bear the ACC feature (nonnominative)? Under @cite{mcfadden-2018}'s containment analysis, all nonnominative cases include ACC in their representation.

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.nom.hasACC = false
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.acc.hasACC = true
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.gen.hasACC = true
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.dat.hasACC = true
• Phenomena.Allomorphy.Studies.Aitha2026.TeluguCase.loc.hasACC = true

inductive Phenomena.Allomorphy.Studies.Aitha2026.StrongClass : Type

Root class for strongly suppletive nouns. @cite{aitha-2026} 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

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqStrongClass : DecidableEq StrongClass

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongClass.beq : StrongClass → StrongClass → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongClass : BEq StrongClass

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongClass = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongClass.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongClass.repr : StrongClass → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongClass : Repr StrongClass

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongClass = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongClass.repr }

structure Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqStrongParadigm.decEq (x✝ x✝¹ : StrongParadigm) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqStrongParadigm : DecidableEq StrongParadigm

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqStrongParadigm = Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqStrongParadigm.decEq

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongParadigm : BEq StrongParadigm

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongParadigm = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongParadigm.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongParadigm.beq : StrongParadigm → StrongParadigm → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongParadigm.beq { nomForm := a, oblForm := a_1 } { nomForm := b, oblForm := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStrongParadigm.beq x✝¹ x✝ = false

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongParadigm : Repr StrongParadigm

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongParadigm = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongParadigm.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprStrongParadigm.repr : StrongParadigm → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.luTiParadigm : StrongParadigm

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

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.uIParadigm : StrongParadigm

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

Equations

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

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

Surface form of n given a strong paradigm and case.

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.strongSurface p c = if c.hasACC = true then p.oblForm else p.nomForm

inductive Phenomena.Allomorphy.Studies.Aitha2026.WeakStemForm : Type

Stem form in weakly suppletive nouns.

• short : WeakStemForm
• long : WeakStemForm

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqWeakStemForm : DecidableEq WeakStemForm

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqWeakStemForm : BEq WeakStemForm

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqWeakStemForm = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqWeakStemForm.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqWeakStemForm.beq : WeakStemForm → WeakStemForm → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqWeakStemForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Allomorphy.Studies.Aitha2026.instReprWeakStemForm.repr : WeakStemForm → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprWeakStemForm : Repr WeakStemForm

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprWeakStemForm = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprWeakStemForm.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.weakParadigm : TeluguCase → WeakStemForm

The weak noun paradigm for samudram 'ocean'. Data from @cite{krishnamurti-gwynn-1985}.

Equations

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

structure Phenomena.Allomorphy.Studies.Aitha2026.NContext : Type

Morphosyntactic context for VI at the n head in Telugu. A context consists of a root class and case features.

• rootClass : StrongClass
• hasAccFeature : Bool

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqNContext : DecidableEq NContext

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqNContext = Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqNContext.decEq

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

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqNContext : BEq NContext

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqNContext = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqNContext.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqNContext.beq : NContext → NContext → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqNContext.beq { rootClass := a, hasAccFeature := a_1 } { rootClass := b, hasAccFeature := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Allomorphy.Studies.Aitha2026.instBEqNContext.beq x✝¹ x✝ = false

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprNContext : Repr NContext

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprNContext = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprNContext.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprNContext.repr : NContext → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.viLuNom : Morphology.DM.VI.VocabItem NContext Unit

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

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.viLuObl : Morphology.DM.VI.VocabItem NContext Unit

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

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.viUNom : Morphology.DM.VI.VocabItem NContext Unit

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

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.viUObl : Morphology.DM.VI.VocabItem NContext Unit

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

Equations

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

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

All VI rules for strong noun n-exponents.

Equations

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

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

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

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.mkNContext rc c = { rootClass := rc, hasAccFeature := c.hasACC }

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

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

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

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

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

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

theorem Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.Aitha2026.weakAllomorphyPattern : Theories.Morphology.CaseContainment.AllomorphyPattern

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

Equations

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.weak_violates_aba : weakAllomorphyPattern.violatesABA = true

The weak alternation violates @cite{caha-2009}'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 Phenomena.Allomorphy.Studies.Aitha2026.weak_not_contiguous : weakAllomorphyPattern.isContiguous = false

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

def Phenomena.Allomorphy.Studies.Aitha2026.strongAllomorphyPattern : Theories.Morphology.CaseContainment.AllomorphyPattern

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

Equations

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.strong_contiguous : strongAllomorphyPattern.isContiguous = true

def Phenomena.Allomorphy.Studies.Aitha2026.WeakStemForm.toNat : WeakStemForm → ℕ

Helper: encode WeakStemForm as a Nat for AllomorphyPattern comparison.

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.WeakStemForm.short.toNat = 0
• Phenomena.Allomorphy.Studies.Aitha2026.WeakStemForm.long.toNat = 1

theorem Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.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 @cite{aitha-2026}'s full(er) paradigm including agreement:

• ACC -ni: light σ within PrWd → long (samudr-āni-ni)
• DAT -ki: light σ within PrWd → long (samudr-āni-ki)
• 1SG -ni: light σ within PrWd → long (samudr-āni-ni)
• 2SG -vi: light σ within PrWd → 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 PrWd → short (samudr-am-lō)
• P -gurinci: separate PrWd → short (samudr-am-gurinci)
• P -eduru: separate PrWd → short (samudr-am-eduru)

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

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqFollowingContext : DecidableEq FollowingContext

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqFollowingContext.beq : FollowingContext → FollowingContext → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqFollowingContext.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqFollowingContext : BEq FollowingContext

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqFollowingContext = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqFollowingContext.beq }

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprFollowingContext : Repr FollowingContext

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprFollowingContext = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprFollowingContext.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprFollowingContext.repr : FollowingContext → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.weakFormPredicted : FollowingContext → WeakStemForm

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

Equations

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

theorem Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.Aitha2026.no_suffix_triggers_short : weakFormPredicted FollowingContext.noSuffix = WeakStemForm.short

No following suffix → short form.

theorem Phenomena.Allomorphy.Studies.Aitha2026.separate_prwd_triggers_short : weakFormPredicted FollowingContext.separatePrWd = WeakStemForm.short

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

inductive Phenomena.Allomorphy.Studies.Aitha2026.AgrSuffix : Type

Telugu nominal predicative agreement suffixes. Only 1SG and 2SG are overt; 3SG and all plurals are null. Data from @cite{aitha-2026}.

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqAgrSuffix : DecidableEq AgrSuffix

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqAgrSuffix.beq : AgrSuffix → AgrSuffix → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqAgrSuffix.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqAgrSuffix : BEq AgrSuffix

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqAgrSuffix = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqAgrSuffix.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprAgrSuffix.repr : AgrSuffix → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprAgrSuffix : Repr AgrSuffix

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprAgrSuffix = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprAgrSuffix.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.AgrSuffix.toFollowing : AgrSuffix → FollowingContext

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

Equations

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

theorem Phenomena.Allomorphy.Studies.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 PrWd — the conditioning is phonological, not morphosyntactic.

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

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

theorem Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.Aitha2026.WeakUnderlying : Type

The underlying representation of the weak noun stem. @cite{aitha-2026} 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 Phenomena.Allomorphy.Studies.Aitha2026.weakUnderlying : WeakUnderlying

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

Equations

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

inductive Phenomena.Allomorphy.Studies.Aitha2026.LocalityType : Type

The two alternations differ in their sensitivity to locality. @cite{aitha-2026} (§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

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqLocalityType : DecidableEq LocalityType

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqLocalityType.beq : LocalityType → LocalityType → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqLocalityType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqLocalityType : BEq LocalityType

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqLocalityType = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqLocalityType.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprLocalityType.repr : LocalityType → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprLocalityType : Repr LocalityType

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprLocalityType = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprLocalityType.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.strongLocality : LocalityType

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.strongLocality = Phenomena.Allomorphy.Studies.Aitha2026.LocalityType.structural

def Phenomena.Allomorphy.Studies.Aitha2026.weakLocality : LocalityType

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.weakLocality = Phenomena.Allomorphy.Studies.Aitha2026.LocalityType.linear

theorem Phenomena.Allomorphy.Studies.Aitha2026.locality_differs : strongLocality ≠ weakLocality

inductive Phenomena.Allomorphy.Studies.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.

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqStemCandidate : DecidableEq StemCandidate

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqStemCandidate : BEq StemCandidate

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStemCandidate = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqStemCandidate.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqStemCandidate.beq : StemCandidate → StemCandidate → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqStemCandidate.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprStemCandidate : Repr StemCandidate

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprStemCandidate = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprStemCandidate.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprStemCandidate.repr : StemCandidate → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.StemCandidate.toParse : StemCandidate → Theories.Phonology.Syllable.MetricalParse

Map each candidate to its MetricalParse representation.

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.cFtBin : Core.OT.NamedConstraint StemCandidate

FT-BIN(μ): penalizes non-bimoraic feet.

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.cParseSyl : Core.OT.NamedConstraint StemCandidate

PARSE-SYL: penalizes unparsed syllables.

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.cAllFtLeft : Core.OT.NamedConstraint StemCandidate

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

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.stemRanking : List (Core.OT.NamedConstraint 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

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

def Phenomena.Allomorphy.Studies.Aitha2026.stemCandidates : List StemCandidate

Equations

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.stemCandidates_ne : stemCandidates ≠ []

theorem Phenomena.Allomorphy.Studies.Aitha2026.stem_ftbin_violations : List.map cFtBin.eval 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 Phenomena.Allomorphy.Studies.Aitha2026.stem_parsesyl_violations : List.map cParseSyl.eval stemCandidates = [1, 0, 0]

theorem Phenomena.Allomorphy.Studies.Aitha2026.stem_optimal : (Core.OT.buildTableau 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.

def Phenomena.Allomorphy.Studies.Aitha2026.sgNiExponent : Morphology.DM.RichRepresentation.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 PrWd-final and cannot form a binary foot.

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.sgNiExponent = Morphology.DM.RichRepresentation.RichExponent.stressed "ni"

theorem Phenomena.Allomorphy.Studies.Aitha2026.sgNi_is_stressed : sgNiExponent.prosody.inherentStress = some true

inductive Phenomena.Allomorphy.Studies.Aitha2026.WordCandNom : Type

Word-level candidates for the NOM input (ˈsa.mu).(ˌdram).ní. Stressed -ni is PrWd-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.

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqWordCandNom : DecidableEq WordCandNom

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandNom : BEq WordCandNom

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandNom = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandNom.beq }

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandNom.beq : WordCandNom → WordCandNom → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandNom.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandNom.repr : WordCandNom → ℕ → Std.Format

Equations

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

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandNom : Repr WordCandNom

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandNom = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandNom.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.wordNomRanking : List (Core.OT.NamedConstraint 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 Phenomena.Allomorphy.Studies.Aitha2026.wordNomCands : List WordCandNom

Equations

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.wordNomCands_ne : wordNomCands ≠ []

theorem Phenomena.Allomorphy.Studies.Aitha2026.wordNom_optimal : (Core.OT.buildTableau wordNomCands wordNomRanking wordNomCands_ne).optimal = [WordCandNom.deleteNi]

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

inductive Phenomena.Allomorphy.Studies.Aitha2026.WordCandDat : Type

Word-level candidates for the DAT input (ˈsa.mu).(ˌdram).ní.ki. The light suffix -ki is PrWd-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).

instance Phenomena.Allomorphy.Studies.Aitha2026.instDecidableEqWordCandDat : DecidableEq WordCandDat

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandDat.beq : WordCandDat → WordCandDat → Bool

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandDat.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandDat : BEq WordCandDat

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandDat = { beq := Phenomena.Allomorphy.Studies.Aitha2026.instBEqWordCandDat.beq }

instance Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandDat : Repr WordCandDat

Equations

• Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandDat = { reprPrec := Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandDat.repr }

def Phenomena.Allomorphy.Studies.Aitha2026.instReprWordCandDat.repr : WordCandDat → ℕ → Std.Format

Equations

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

def Phenomena.Allomorphy.Studies.Aitha2026.wordDatRanking : List (Core.OT.NamedConstraint 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 Phenomena.Allomorphy.Studies.Aitha2026.wordDatCands : List WordCandDat

Equations

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.wordDatCands_ne : wordDatCands ≠ []

theorem Phenomena.Allomorphy.Studies.Aitha2026.wordDat_optimal : (Core.OT.buildTableau wordDatCands wordDatRanking wordDatCands_ne).optimal = [WordCandDat.compLengthen]

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.word_level_derives_alternation : (Core.OT.buildTableau wordNomCands wordNomRanking wordNomCands_ne).optimal = [WordCandNom.deleteNi] ∧ (Core.OT.buildTableau wordDatCands 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 PrWd.

• NOM (no suffix): -ni is PrWd-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 Phenomena.Allomorphy.Studies.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

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

def Phenomena.Allomorphy.Studies.Aitha2026.WordCandDat.toStemForm : WordCandDat → WeakStemForm

Equations

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.nom_produces_short : WordCandNom.deleteNi.toStemForm = WeakStemForm.short

theorem Phenomena.Allomorphy.Studies.Aitha2026.dat_produces_long : WordCandDat.compLengthen.toStemForm = WeakStemForm.long

def Phenomena.Allomorphy.Studies.Aitha2026.weakSurfaceFromPrWd : Option Theories.Phonology.ProsodicWord.MorphElement → WeakStemForm

Predict the weak stem form from the following morphological element. Uses MorphElement.triggersLongForm from ProsodicWord: the long form surfaces iff the following element is PrWd-internal AND begins with a light syllable.

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Allomorphy.Studies.Aitha2026.weakSurfaceFromPrWd none = Phenomena.Allomorphy.Studies.Aitha2026.WeakStemForm.short

theorem Phenomena.Allomorphy.Studies.Aitha2026.acc_ni_long : weakSurfaceFromPrWd (some { form := "-ni", status := Theories.Phonology.ProsodicWord.MorphStatus.inflectional, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.long

theorem Phenomena.Allomorphy.Studies.Aitha2026.dat_ki_long : weakSurfaceFromPrWd (some { form := "-ki", status := Theories.Phonology.ProsodicWord.MorphStatus.inflectional, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.long

theorem Phenomena.Allomorphy.Studies.Aitha2026.nom_null_short : weakSurfaceFromPrWd none = WeakStemForm.short

theorem Phenomena.Allomorphy.Studies.Aitha2026.gen_null_short : weakSurfaceFromPrWd none = WeakStemForm.short

theorem Phenomena.Allomorphy.Studies.Aitha2026.agr_1sg_ni_long : weakSurfaceFromPrWd (some { form := "-ni", status := Theories.Phonology.ProsodicWord.MorphStatus.agreement, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.long

theorem Phenomena.Allomorphy.Studies.Aitha2026.agr_2sg_vi_long : weakSurfaceFromPrWd (some { form := "-vi", status := Theories.Phonology.ProsodicWord.MorphStatus.agreement, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.long

theorem Phenomena.Allomorphy.Studies.Aitha2026.postp_lo_short : weakSurfaceFromPrWd (some { form := "-lō", status := Theories.Phonology.ProsodicWord.MorphStatus.postposition, initialWeight := Theories.Phonology.Syllable.SyllWeight.heavy }) = WeakStemForm.short

theorem Phenomena.Allomorphy.Studies.Aitha2026.postp_gurinci_short : weakSurfaceFromPrWd (some { form := "-gurinci", status := Theories.Phonology.ProsodicWord.MorphStatus.postposition, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.short

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.prwd_matches_paradigm : weakSurfaceFromPrWd (some { form := "-ni", status := Theories.Phonology.ProsodicWord.MorphStatus.inflectional, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.long ∧ weakSurfaceFromPrWd (some { form := "-ki", status := Theories.Phonology.ProsodicWord.MorphStatus.inflectional, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = WeakStemForm.long ∧ weakSurfaceFromPrWd none = WeakStemForm.short ∧ weakSurfaceFromPrWd none = WeakStemForm.short ∧ weakSurfaceFromPrWd (some { form := "-lō", status := Theories.Phonology.ProsodicWord.MorphStatus.postposition, initialWeight := Theories.Phonology.Syllable.SyllWeight.heavy }) = WeakStemForm.short

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.prwd_agrees_with_paradigm : weakSurfaceFromPrWd (some { form := "-ni", status := Theories.Phonology.ProsodicWord.MorphStatus.inflectional, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = weakParadigm TeluguCase.acc ∧ weakSurfaceFromPrWd (some { form := "-ki", status := Theories.Phonology.ProsodicWord.MorphStatus.inflectional, initialWeight := Theories.Phonology.Syllable.SyllWeight.light }) = weakParadigm TeluguCase.dat ∧ weakSurfaceFromPrWd none = weakParadigm TeluguCase.nom ∧ weakSurfaceFromPrWd none = weakParadigm TeluguCase.gen ∧ weakSurfaceFromPrWd (some { form := "-lō", status := Theories.Phonology.ProsodicWord.MorphStatus.postposition, initialWeight := Theories.Phonology.Syllable.SyllWeight.heavy }) = weakParadigm TeluguCase.loc

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

theorem Phenomena.Allomorphy.Studies.Aitha2026.strong_vs_weak_distinction : strongAllomorphyPattern.isContiguous = true ∧ weakAllomorphyPattern.isContiguous = false

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 PrWd.

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 Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.Aitha2026.hasACC_eq_isNonnom (c : TeluguCase) : c.hasACC = Theories.Morphology.CaseContainment.isNonnom c.toCore

Telugu's hasACC exactly mirrors Core.Case.isNonnom via toCore. This confirms the study's case-feature assignments are consistent with the containment hierarchy infrastructure.

theorem Phenomena.Allomorphy.Studies.Aitha2026.telugu_inventory_valid : Core.validInventory [Core.Case.nom, Core.Case.acc, Core.Case.gen, Core.Case.dat, Core.Case.loc] = true

The Telugu 5-case inventory is contiguous on Blake's typological hierarchy (@cite{blake-1994}).

theorem Phenomena.Allomorphy.Studies.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 Phenomena.Allomorphy.Studies.Aitha2026.central_argument : strongAllomorphyPattern.isContiguous = true ∧ weakAllomorphyPattern.isContiguous = false ∧ 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