The nouns that say -ni

[Ait26] separates two stem alternations in Telugu nouns. The strong alternation (il-lu in-ṭi 'house') is contextual allomorphy of the nominalizer n conditioned by [ACC], the feature every nonnominative case contains under [Cah09]'s containment hierarchy ([McF18]). The weak alternation (samudr-am samudr-āni 'ocean') only looks like case allomorphy: it violates *ABA, is triggered by agreement suffixes in nominative contexts, and reads the weight of the next syllable inside the prosodic word. It is instead the phonology of a single underlying -am-ni, derived in Stratal OT ([Kip00]) from prespecified stress on the singular suffix -ni.

Main definitions

• strongItems, strongN: the Vocabulary Items of (4) over root lists and [ACC], and the n exponent they insert.
• Following, weakN: what follows n and the long/short generalization of §3.2 — long iff the next syllable is light and inside the prosodic word.
• numItems: the singular suffix -ni as an exponent of Num conditioned by the preceding -am ((40)).
• stemRanking, wordNomRanking, wordDatRanking, phraseRanking: the tableaux of (49), (62), (59), and (66).

Main results

• strong_rows, weak_rows: the items and the generalization reproduce every paradigm cell of the data pool.
• weak_not_case_function: no assignment of exponents to cases fits the weak rows — the nominative carries both forms ((8), (16)).
• weak_violates_aba, strong_contiguous: the paradigm shapes against containment.
• wordNom_optimal, wordDat_optimal: Word-level phonology deletes word-final stressed -ni and repairs /mn/ by compensatory lengthening.
• distZero_demoted, alignR_demoted: the Word-to-Phrase rerankings of (68).

Implementation notes

The Stem-level sandhi of the -em and -ām subclasses ((52), (55)) and the quantifier-postposing tableaux ((63), (67)) are not formalized. Tableau violation marks follow the paper's prose where the tableau images are not in the text layer.

Case

inductive Aitha2026.TeluguCase : Type

The Telugu cases of the paradigms, with the postpositions as P.

• nom : TeluguCase
• acc : TeluguCase
• gen : TeluguCase
• dat : TeluguCase
• p : TeluguCase

@[instance_reducible]

instance Aitha2026.instDecidableEqTeluguCase : DecidableEq TeluguCase

Equations

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

@[instance_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.p prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.TeluguCase.p")).group prec✝

@[instance_reducible]

instance Aitha2026.instFintypeTeluguCase : Fintype TeluguCase

Equations

• Aitha2026.instFintypeTeluguCase = { elems := { val := ↑Aitha2026.TeluguCase.enumList, nodup := Aitha2026.TeluguCase.enumList_nodup }, complete := Aitha2026.instFintypeTeluguCase._proof_1 }

def Aitha2026.TeluguCase.toCore : TeluguCase → Case

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.p.toCore = Case.loc

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

A nonnominative case contains [ACC] ((3), [Cah09]): the natural class of the oblique.

Equations

• c.IsNonnom = c.toCore.IsNonnominative

@[instance_reducible]

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

Equations

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

def Aitha2026.TeluguCase.ofString : String → Option TeluguCase

Equations

• Aitha2026.TeluguCase.ofString "nom" = some Aitha2026.TeluguCase.nom
• Aitha2026.TeluguCase.ofString "acc" = some Aitha2026.TeluguCase.acc
• Aitha2026.TeluguCase.ofString "gen" = some Aitha2026.TeluguCase.gen
• Aitha2026.TeluguCase.ofString "dat" = some Aitha2026.TeluguCase.dat
• Aitha2026.TeluguCase.ofString "p" = some Aitha2026.TeluguCase.p
• Aitha2026.TeluguCase.ofString x✝ = none

The strong alternation (§2)

inductive Aitha2026.Root : Type

The strong roots of (2), by gloss.

• house : Root
• bow : Root
• eye : Root
• tooth : Root
• nest : Root
• stream : Root
• mouth : Root
• plough : Root
• ghee : Root
• well : Root
• town : Root
• husband : Root

@[instance_reducible]

instance Aitha2026.instDecidableEqRoot : DecidableEq Root

Equations

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

@[instance_reducible]

instance Aitha2026.instReprRoot : Repr Root

Equations

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

def Aitha2026.instReprRoot.repr : Root → ℕ → Std.Format

Equations

• Aitha2026.instReprRoot.repr Aitha2026.Root.house prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.house")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.bow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.bow")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.eye prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.eye")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.tooth prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.tooth")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.nest prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.nest")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.stream prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.stream")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.mouth prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.mouth")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.plough prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.plough")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.ghee prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.ghee")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.well prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.well")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.town prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.town")).group prec✝
• Aitha2026.instReprRoot.repr Aitha2026.Root.husband prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Root.husband")).group prec✝

@[instance_reducible]

instance Aitha2026.instFintypeRoot : Fintype Root

Equations

• Aitha2026.instFintypeRoot = { elems := { val := ↑Aitha2026.Root.enumList, nodup := Aitha2026.Root.enumList_nodup }, complete := Aitha2026.instFintypeRoot._proof_1 }

def Aitha2026.Root.ofString : String → Option Root

Equations

• Aitha2026.Root.ofString "house" = some Aitha2026.Root.house
• Aitha2026.Root.ofString "bow" = some Aitha2026.Root.bow
• Aitha2026.Root.ofString "eye" = some Aitha2026.Root.eye
• Aitha2026.Root.ofString "tooth" = some Aitha2026.Root.tooth
• Aitha2026.Root.ofString "nest" = some Aitha2026.Root.nest
• Aitha2026.Root.ofString "stream" = some Aitha2026.Root.stream
• Aitha2026.Root.ofString "mouth" = some Aitha2026.Root.mouth
• Aitha2026.Root.ofString "plough" = some Aitha2026.Root.plough
• Aitha2026.Root.ofString "ghee" = some Aitha2026.Root.ghee
• Aitha2026.Root.ofString "well" = some Aitha2026.Root.well
• Aitha2026.Root.ofString "town" = some Aitha2026.Root.town
• Aitha2026.Root.ofString "husband" = some Aitha2026.Root.husband
• Aitha2026.Root.ofString x✝ = none

inductive Aitha2026.Feature : Type

Features at the n head: the root it attaches to and, in every nonnominative case, [ACC].

• root (r : Root) : Feature
• acc : Feature

@[instance_reducible]

instance Aitha2026.instDecidableEqFeature : DecidableEq Feature

Equations

• Aitha2026.instDecidableEqFeature = Aitha2026.instDecidableEqFeature.decEq

def Aitha2026.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• Aitha2026.instDecidableEqFeature.decEq (Aitha2026.Feature.root a) (Aitha2026.Feature.root b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Aitha2026.instDecidableEqFeature.decEq (Aitha2026.Feature.root r) Aitha2026.Feature.acc = isFalse ⋯
• Aitha2026.instDecidableEqFeature.decEq Aitha2026.Feature.acc (Aitha2026.Feature.root r) = isFalse ⋯
• Aitha2026.instDecidableEqFeature.decEq Aitha2026.Feature.acc Aitha2026.Feature.acc = isTrue ⋯

def Aitha2026.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aitha2026.instReprFeature : Repr Feature

Equations

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

def Aitha2026.site (r : Root) (c : TeluguCase) : List Feature

The n head's bundle for root r in case c.

Equations

• Aitha2026.site r c = Aitha2026.Feature.root r :: if c.IsNonnom then [Aitha2026.Feature.acc] else []

def Aitha2026.forRoots (roots : List Root) (e : String) (acc : Bool := false) : List (DistributedMorphology.VocabularyItem Feature String)

The items of one exponent: e next to each listed root, in the context of [ACC] when acc.

Equations

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

def Aitha2026.strongItems : List (DistributedMorphology.VocabularyItem Feature String)

The Vocabulary Items of (4) for the roots of (2): the nominative exponents next to their roots, and the oblique exponents next to the same roots and [ACC] — one -ṭi entry spanning the -ru, -lu, -nu, -ḍu, and -li classes, -ti for the -yi class, -i for the -u class.

Equations

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

def Aitha2026.strongN (r : Root) (c : TeluguCase) : Option String

The exponent of n for root r in case c.

Equations

• Aitha2026.strongN r c = DistributedMorphology.subsetPrinciple Aitha2026.strongItems (DistributedMorphology.Neighborhood.ofBundle (Aitha2026.site r c))

theorem Aitha2026.strongN_nonnom (r : Root) (c : TeluguCase) : c.IsNonnom → strongN r c = strongN r TeluguCase.acc

The nominative–nonnominative cut: every nonnominative case takes the accusative's exponent, by the Elsewhere Condition over [ACC].

The weak alternation (§3)

structure Aitha2026.Following : Type

What follows the n exponent: its membership in the noun's prosodic word and the weight of its initial syllable (§3.2).

• internal : Bool
• weight : Prosody.Syllable.Weight

def Aitha2026.instDecidableEqFollowing.decEq (x✝ x✝¹ : Following) : Decidable (x✝ = x✝¹)

Equations

• Aitha2026.instDecidableEqFollowing.decEq { internal := a, weight := a_1 } { internal := b, weight := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Aitha2026.instDecidableEqFollowing : DecidableEq Following

Equations

• Aitha2026.instDecidableEqFollowing = Aitha2026.instDecidableEqFollowing.decEq

def Aitha2026.instReprFollowing.repr : Following → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aitha2026.instReprFollowing : Repr Following

Equations

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

def Aitha2026.TriggersLong (f : Option Following) : Prop

The long form is triggered iff the next syllable is light and inside the prosodic word; postpositions with light initial syllables ((18)) and the heavy-initial postposed quantifier ((17)) do not trigger it.

Equations

• Aitha2026.TriggersLong f = ∃ m ∈ f, m.internal = true ∧ m.weight = Prosody.Syllable.Weight.light

@[instance_reducible]

instance Aitha2026.instDecidableTriggersLong (f : Option Following) : Decidable (TriggersLong f)

Equations

• Aitha2026.instDecidableTriggersLong f = id inferInstance

def Aitha2026.weakN (f : Option Following) : String

The weak n exponent: -āni before a word-internal light syllable, -am otherwise.

Equations

• Aitha2026.weakN f = if Aitha2026.TriggersLong f then "āni" else "am"

The data pool

structure Aitha2026.Cell : Type

A paradigm cell of the pool: the root class, the case if any, what follows n, and the n exponent.

• noun : String
• strongRoot : Option Root
• plural : Bool
• case : Option TeluguCase
• following : Option Following
• n : String

@[instance_reducible]

instance Aitha2026.instDecidableEqCell : DecidableEq Cell

Equations

• Aitha2026.instDecidableEqCell = Aitha2026.instDecidableEqCell.decEq

def Aitha2026.instDecidableEqCell.decEq (x✝ x✝¹ : Cell) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Aitha2026.instReprCell : Repr Cell

Equations

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

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

Equations

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

def Aitha2026.Cell.ofExample (ex : Data.Examples.LinguisticExample) : Option Cell

The cell an example records, from its paperFeatures.

Equations

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

theorem Aitha2026.cell_ofExample_isSome (ex : Data.Examples.LinguisticExample) : ex ∈ Examples.all → (Cell.ofExample ex).isSome = true

def Aitha2026.cells : List Cell

The cells of the pool.

Equations

• Aitha2026.cells = List.filterMap Aitha2026.Cell.ofExample Aitha2026.Examples.all

def Aitha2026.strongCells : List (Root × TeluguCase × String)

The strong cells, with their roots.

Equations

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

def Aitha2026.weakCells : List Cell

The singular weak cells.

Equations

• Aitha2026.weakCells = List.filter (fun (c : Aitha2026.Cell) => decide (c.strongRoot = none ∧ ¬c.plural = true)) Aitha2026.cells

theorem Aitha2026.strong_rows (x : Root × TeluguCase × String) : x ∈ strongCells → strongN x.1 x.2.1 = some x.2.2

The strong paradigm: (4) inserts the attested exponent in every strong cell of (1), (2), and fn. 6 — the agreement suffix, bearing no [ACC], leaves the nominative form.

theorem Aitha2026.weak_rows (c : Cell) : c ∈ weakCells → weakN c.following = c.n

The weak generalization: the long form in every singular weak cell of (8), (13)–(18) is predicted by the following syllable alone.

def Aitha2026.oceanNom : Cell

The nominative short form of (8).

Equations

• Aitha2026.oceanNom = { noun := "samudram", strongRoot := none, plural := false, case := some Aitha2026.TeluguCase.nom, following := none, n := "am" }

def Aitha2026.ocean1sg : Cell

The long form under the 1SG agreement suffix, in a nominative predicate nominal ((13)).

Equations

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

theorem Aitha2026.weak_not_case_function : ¬∃ (f : Option TeluguCase → String), ∀ c ∈ weakCells, f c.case = c.n

Not case allomorphy: no assignment of an n exponent to each case fits the weak cells, since the nominative carries both -am and -āni ((8) with (13)–(16)).

Paradigm shapes against containment (§3.1)

def Aitha2026.caseSuffix : TeluguCase → Option Following

The suffix shapes of the case paradigms (1) and (8): null nominative and genitive, light -ni/-ki, and the heavy postposition -lō.

Equations

• Aitha2026.caseSuffix Aitha2026.TeluguCase.nom = none
• Aitha2026.caseSuffix Aitha2026.TeluguCase.acc = some { internal := true, weight := Prosody.Syllable.Weight.light }
• Aitha2026.caseSuffix Aitha2026.TeluguCase.gen = none
• Aitha2026.caseSuffix Aitha2026.TeluguCase.dat = some { internal := true, weight := Prosody.Syllable.Weight.light }
• Aitha2026.caseSuffix Aitha2026.TeluguCase.p = some { internal := false, weight := Prosody.Syllable.Weight.heavy }

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

The weak paradigm as an allomorphy pattern, short 0 and long 1.

Equations

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

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

The strong paradigm of illu as an allomorphy pattern, nominative 0 and oblique 1.

Equations

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

theorem Aitha2026.weak_violates_aba : weakPattern.ViolatesABA

The weak ABAB paradigm violates *ABA: the nominative form resurfaces in the genitive, which contains [ACC] ([Cah09]).

theorem Aitha2026.strong_contiguous : strongPattern.IsContiguous

The strong ABB paradigm is contiguous on the containment hierarchy.

The singular suffix (§4.2)

inductive Aitha2026.NumContext : Type

The context of Num: the preceding n exponent is -am.

• afterAm : NumContext

@[instance_reducible]

instance Aitha2026.instDecidableEqNumContext : DecidableEq NumContext

Equations

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

@[instance_reducible]

instance Aitha2026.instReprNumContext : Repr NumContext

Equations

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

def Aitha2026.instReprNumContext.repr : NumContext → ℕ → Std.Format

Equations

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

def Aitha2026.numItems : List (DistributedMorphology.VocabularyItem NumContext String)

The Vocabulary Items of Num in the singular ((40)): -ni after -am, null elsewhere — conditioned inward, as root-out insertion allows.

Equations

• Aitha2026.numItems = [DistributedMorphology.VocabularyItem.ofFeatures [Aitha2026.NumContext.afterAm] "ni", DistributedMorphology.VocabularyItem.ofFeatures [] "ø"]

def Aitha2026.numSg (nExponent : String) : Option String

The singular exponent of Num after an n exponent.

Equations

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

theorem Aitha2026.numSg_am : numSg "am" = some "ni" ∧ numSg "lu" = some "ø"

Weak nouns take -ni, strong nouns the null singular: the underlying weak singular is samudr-am-ni-K ((41)).

Stem-level phonology (§5.1)

inductive Aitha2026.StemCandidate : Type

The metrical parses of samudr-am in (49): final heavy syllable unparsed, three degenerate feet, or two bimoraic trochees.

• unparsedFinal : StemCandidate
• degenerate : StemCandidate
• trochees : StemCandidate

@[instance_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.

@[instance_reducible]

instance Aitha2026.instReprStemCandidate : Repr StemCandidate

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• Aitha2026.StemCandidate.unparsedFinal.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 ((48)): per foot, the syllables between the left edge of the domain and the foot.

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.ftBin : Constraints.Constraint StemCandidate

FT-BIN(μ) ((46)).

Equations

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

def Aitha2026.parseSyl : Constraints.Constraint StemCandidate

PARSE-SYL ((47)).

Equations

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

def Aitha2026.allFtLeft : Constraints.Constraint StemCandidate

Equations

• Aitha2026.allFtLeft c = Aitha2026.allFtLeftOf c.toFooting

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

FT-BIN ≫ PARSE-SYL ≫ ALL-FT-LEFT.

Equations

• Aitha2026.stemRanking = [Aitha2026.ftBin, Aitha2026.parseSyl, Aitha2026.allFtLeft]

def Aitha2026.stemCandidates : List StemCandidate

Equations

• Aitha2026.stemCandidates = [Aitha2026.StemCandidate.unparsedFinal, Aitha2026.StemCandidate.degenerate, Aitha2026.StemCandidate.trochees]

theorem Aitha2026.stemCandidates_ne : stemCandidates ≠ []

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

(49): the Stem parses as two moraic trochees, (ˈsa.mu)(ˌdram).

Word-level phonology (§5.2)

inductive Aitha2026.Con : Type

The constraints of §5.2–5.3, as labels shared across strata.

• distZero : Con
• alignR : Con
• identStress : Con
• ftBin : Con
• maxMora : Con
• max : Con
• identLength : Con
• complexCoda : Con

@[instance_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.identStress prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.identStress")).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.identLength prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.identLength")).group prec✝
• Aitha2026.instReprCon.repr Aitha2026.Con.complexCoda prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.complexCoda")).group prec✝

@[instance_reducible]

instance Aitha2026.instReprCon : Repr Con

Equations

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

inductive Aitha2026.WordCandNom : Type

The Word-level candidates for nominative samudr-am-ní ((62)): destress -ni; foot it alone; delete /i/ into a coda cluster; delete /i/ and /m/; or delete /ni/.

• destress : WordCandNom
• degenerateFoot : WordCandNom
• deleteI : WordCandNom
• deleteIM : WordCandNom
• deleteNi : WordCandNom

@[instance_reducible]

instance Aitha2026.instDecidableEqWordCandNom : DecidableEq WordCandNom

Equations

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

@[instance_reducible]

instance Aitha2026.instReprWordCandNom : Repr WordCandNom

Equations

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

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

Equations

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

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

(62): IDENT-STRESS, FT-BIN, *COMPLEXCODA, ALIGN-R ≫ MAX-μ, MAX.

Equations

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

def Aitha2026.wordNomCands : List WordCandNom

Equations

• Aitha2026.wordNomCands = [Aitha2026.WordCandNom.destress, Aitha2026.WordCandNom.degenerateFoot, Aitha2026.WordCandNom.deleteI, Aitha2026.WordCandNom.deleteIM, Aitha2026.WordCandNom.deleteNi]

theorem Aitha2026.wordNomCands_ne : wordNomCands ≠ []

theorem Aitha2026.wordNom_optimal : (OptimalityTheory.Tableau.ofRanking wordNomCands (List.map (fun (x : Con × Constraints.Constraint WordCandNom) => x.2) wordNomRanking) wordNomCands_ne).optimal = {WordCandNom.deleteNi}

(62): word-final stressed -ni, unable to head a binary foot, is deleted — the short form samudram.

inductive Aitha2026.WordCandDat : Type

The Word-level candidates for dative samudr-am-ní-ki ((59)): keep /mn/; delete /n/ or /m/ with the mora; delete /m/ or /n/ with compensatory lengthening.

• faithful : WordCandDat
• deleteN : WordCandDat
• deleteM : WordCandDat
• deleteMLengthen : WordCandDat
• deleteNLengthen : WordCandDat

@[instance_reducible]

instance Aitha2026.instDecidableEqWordCandDat : DecidableEq WordCandDat

Equations

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

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

Equations

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

@[instance_reducible]

instance Aitha2026.instReprWordCandDat : Repr WordCandDat

Equations

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

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

(59): *DIST-0, MAX-μ ≫ ALIGN-R ≫ MAX, IDENT-LENGTH.

Equations

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

def Aitha2026.wordDatCands : List WordCandDat

Equations

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

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.deleteMLengthen}

(59): the /mn/ contact is repaired by deleting /m/ and lengthening /a/ — the long form samudrāniki.

def Aitha2026.WordCandNom.nExponent : WordCandNom → String

The n exponent each Word-level output leaves.

Equations

• Aitha2026.WordCandNom.destress.nExponent = "amni"
• Aitha2026.WordCandNom.degenerateFoot.nExponent = "amni"
• Aitha2026.WordCandNom.deleteI.nExponent = "amn"
• Aitha2026.WordCandNom.deleteIM.nExponent = "an"
• Aitha2026.WordCandNom.deleteNi.nExponent = "am"

def Aitha2026.WordCandDat.nExponent : WordCandDat → String

Equations

• Aitha2026.WordCandDat.faithful.nExponent = "amni"
• Aitha2026.WordCandDat.deleteN.nExponent = "ami"
• Aitha2026.WordCandDat.deleteM.nExponent = "ani"
• Aitha2026.WordCandDat.deleteMLengthen.nExponent = "āni"
• Aitha2026.WordCandDat.deleteNLengthen.nExponent = "āmi"

theorem Aitha2026.word_level_derives_weakN : WordCandNom.deleteNi.nExponent = weakN (caseSuffix TeluguCase.nom) ∧ WordCandDat.deleteMLengthen.nExponent = weakN (caseSuffix TeluguCase.dat)

The two Word-level winners are the two forms of the generalization weakN: the same underlying -am-ni surfaces short before nothing and long before a word-internal light syllable.

Phrase-level phonology (§5.3)

inductive Aitha2026.PhraseCand : Type

The Phrase-level candidates for samudram nunci 'from the ocean' ((66)): delete /m/ with or without lengthening, delete the postposition's /n/, or keep the /mn/ contact.

• deleteMLengthen : PhraseCand
• deleteM : PhraseCand
• deleteN : PhraseCand
• faithful : PhraseCand

@[instance_reducible]

instance Aitha2026.instDecidableEqPhraseCand : DecidableEq PhraseCand

Equations

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

def Aitha2026.instReprPhraseCand.repr : PhraseCand → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aitha2026.instReprPhraseCand : Repr PhraseCand

Equations

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

def Aitha2026.phraseRanking : List (Con × Constraints.Constraint PhraseCand)

(66), (68): at the Phrase level MAX outranks *DIST-0 and ALIGN-R, and segmental faithfulness outranks prosodic faithfulness.

Equations

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

def Aitha2026.phraseCands : List PhraseCand

Equations

• Aitha2026.phraseCands = [Aitha2026.PhraseCand.deleteMLengthen, Aitha2026.PhraseCand.deleteM, Aitha2026.PhraseCand.deleteN, Aitha2026.PhraseCand.faithful]

theorem Aitha2026.phraseCands_ne : phraseCands ≠ []

theorem Aitha2026.phrase_optimal : (OptimalityTheory.Tableau.ofRanking phraseCands (List.map (fun (x : Con × Constraints.Constraint PhraseCand) => x.2) phraseRanking) phraseCands_ne).optimal = {PhraseCand.faithful}

(66): across the postposition boundary the /mn/ contact is kept.

theorem Aitha2026.distZero_demoted : OptimalityTheory.Stratal.IsDemotedAcross Con.distZero phraseRanking wordDatRanking

*DIST-0 is demoted below MAX from Word to Phrase ((68)).

theorem Aitha2026.alignR_demoted : OptimalityTheory.Stratal.IsDemotedAcross Con.alignR phraseRanking wordDatRanking

ALIGN-R is demoted below MAX from Word to Phrase ((68)).