The nouns that say -ni

Telugu nouns show two stem alternations. The strong one (il-lu in-ṭi 'house') is contextual allomorphy of the nominalizer n conditioned by [ACC], the feature every nonnominative case contains under Caha's containment, as McFadden proposes. The weak one (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 the phonology of one underlying -am-ni, derived in Kiparsky's Stratal OT from prespecified stress on the singular suffix -ni.

This file defines the Vocabulary Items of the strong alternation, the weak generalization, the singular suffix, and the Stem, Word, and Phrase tableaux with the marks of the paper's (49), (59), (62), (63), (66), and (67) under the rankings of (64) and (68).

Main definitions

• strongItems, strongN: the Vocabulary Items of (4) and the n exponent they insert.
• weakN: the weak alternation by the syllable that follows n.
• numItems, numSg: the singular suffix -ni of (40).
• wordOrder, phraseOrder: the rankings of (64) and (68).

Main results

• strong_rows, weak_rows: both alternations against every paradigm cell of the pool.
• weak_not_case_function, weak_violates_aba: the arguments against case conditioning.
• oblique_across_quantifier: the locality contrast of (33)–(36).
• wordDat_optimal, wordNom_optimal: both surface forms from one underlying -am-ni.
• distZero_alignR_max_reranked and its siblings: the Word-to-Phrase rerankings of (68).

Implementation notes

The cells of the paradigms are the cases of Telugu.Case and the uses of the postpositions of Telugu.Adpositions, a postposition with a value it marks, the paper's P cell being lō; they are ordered by the scoped Caha containment order on their comparative values.

References

• [Ait26]
• [Cah09]
• [McF18]
• [Kip00]

Case

def Aitha2026.caseOfLabel : String → Option Case

The case of a paradigm cell by the paper's label, its P the postposition lō.

Equations

• Aitha2026.caseOfLabel "nom" = some Case.nom
• Aitha2026.caseOfLabel "acc" = some Case.acc
• Aitha2026.caseOfLabel "gen" = some Case.gen
• Aitha2026.caseOfLabel "dat" = some Case.dat
• Aitha2026.caseOfLabel "p" = some Case.loc
• Aitha2026.caseOfLabel 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

The features at the n head are the root it attaches to and, in every nonnominative case, [ACC].

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

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 ⋯

@[instance_reducible]

instance Aitha2026.instDecidableEqFeature : DecidableEq Feature

Equations

• Aitha2026.instDecidableEqFeature = Aitha2026.instDecidableEqFeature.decEq

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 : Case) : List Feature

The n head's bundle for root r in case c, with [ACC] in every nonnominative case, the natural class of the oblique ((3), [Cah09]).

Equations

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

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

forRoots roots e acc lists the items inserting e next to each root of roots, 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) insert 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 and -i for the -u class.

Equations

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

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

The exponent of n for root r in case c.

Equations

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

@[reducible, inline]

abbrev Aitha2026.PostpositionUse : Type

A use of a Telugu postposition is the postposition with a value it marks.

Equations

• Aitha2026.PostpositionUse = ((a : { a : Adposition // a ∈ Telugu.Adpositions.inventory }) × ↥(↑a).functions)

inductive Aitha2026.ParadigmCell : Type

A cell of the paradigms (1) and (8), a case or a use of a postposition.

• case (c : Telugu.Case) : ParadigmCell

  A case of Telugu.Case.

• postposition (u : PostpositionUse) : ParadigmCell

  A use of a postposition of Telugu.Adpositions.

def Aitha2026.instDecidableEqParadigmCell.decEq (x✝ x✝¹ : ParadigmCell) : Decidable (x✝ = x✝¹)

Equations

• Aitha2026.instDecidableEqParadigmCell.decEq (Aitha2026.ParadigmCell.case a) (Aitha2026.ParadigmCell.case b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Aitha2026.instDecidableEqParadigmCell.decEq (Aitha2026.ParadigmCell.case c) (Aitha2026.ParadigmCell.postposition u) = isFalse ⋯
• Aitha2026.instDecidableEqParadigmCell.decEq (Aitha2026.ParadigmCell.postposition u) (Aitha2026.ParadigmCell.case c) = isFalse ⋯
• Aitha2026.instDecidableEqParadigmCell.decEq (Aitha2026.ParadigmCell.postposition a) (Aitha2026.ParadigmCell.postposition b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Aitha2026.instDecidableEqParadigmCell : DecidableEq ParadigmCell

Equations

• Aitha2026.instDecidableEqParadigmCell = Aitha2026.instDecidableEqParadigmCell.decEq

@[instance_reducible]

instance Aitha2026.instFintypeParadigmCell : Fintype ParadigmCell

Equations

• Aitha2026.instFintypeParadigmCell = Fintype.ofEquiv (Telugu.Case ⊕ Aitha2026.PostpositionUse) Aitha2026.ParadigmCell.proxyTypeEquiv

def Aitha2026.ParadigmCell.label : ParadigmCell → Case

The comparative value of a cell.

Equations

• (Aitha2026.ParadigmCell.case a).label = a.label
• (Aitha2026.ParadigmCell.postposition a).label = ↑a.snd

@[instance_reducible]

instance Aitha2026.instPreorderParadigmCell : Preorder ParadigmCell

The cells are ordered by the containment order on their comparative values.

Equations

• Aitha2026.instPreorderParadigmCell = Preorder.lift Aitha2026.ParadigmCell.label

@[instance_reducible]

instance Aitha2026.instDecidableLEParadigmCell : DecidableLE ParadigmCell

Equations

• Aitha2026.instDecidableLEParadigmCell a b = { decide := decide (a.label = b.label) || decide ([a.label, b.label].Sublist Case.containment), reflects_decide := ⋯ }

theorem Aitha2026.strongN_nonnom (r : Root) (c : ParadigmCell) : c.label.IsNonnominative → strongN r c.label = strongN r Case.acc

Every nonnominative cell takes the accusative's exponent, the nominative–nonnominative cut of the paradigm, by the Elsewhere Condition over [ACC].

The weak alternation (§3)

structure Aitha2026.Following : Type

What follows the n exponent is recorded by 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

@[instance_reducible]

instance Aitha2026.instReprFollowing : Repr Following

Equations

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

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

Equations

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

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 is -āni before a word-internal light syllable and -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 records the noun, its strong root if any, its number, its case if any, what follows n, the n exponent, and for singular weak nouns whether the form is long.

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

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

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

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.Cell.ofDatum (ex : Datum) : 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_ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (ex.feature? "n").isSome = true → (Cell.ofDatum ex).isSome = true

Every row recording an n exponent is a cell.

def Aitha2026.cells : List Cell

The cells of the pool.

Equations

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

def Aitha2026.strongCells : List (Root × Case × 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 × Case × String) : x ∈ strongCells → strongN x.1 x.2.1 = some x.2.2

The items of (4) insert 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 → c.long = some (decide (TriggersLong c.following))

In every singular weak cell of (6)–(8), (13)–(18), and (34) the form is long exactly when the following syllable is light and word-internal, the weak generalization.

def Aitha2026.oceanNom : Cell

The nominative short form of (8).

Equations

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

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 Case → Option Bool), ∀ c ∈ weakCells, f c.case = c.long

No assignment of a form to each case fits the weak cells, since the nominative carries both -am and -āni ((8) with (13)–(16)), so the weak alternation is not case allomorphy.

theorem Aitha2026.oblique_across_quantifier (row : Datum) : row ∈ Examples.all → row.feature? "intervener" = some "quantifier" → row.feature? "class" = some "strong" → (row.judgment = Judgment.acceptable ↔ (row.feature? "stem" = some "obl" ↔ row.feature? "case" ≠ some "nom"))

Across a postposed quantifier the strong oblique is licensed exactly when the overall case is nonnominative ((33)–(36)).

Paradigm shapes against containment (§3.1)

def Aitha2026.caseSuffix : ParadigmCell → Option Following

What follows n in each cell of the paradigms (1) and (8) is nothing in the unmarked nominative and genitive, a light suffix inside the prosodic word, or a heavy postposition outside it.

Equations

• Aitha2026.caseSuffix (Aitha2026.ParadigmCell.case a) = Option.map (fun (x : Morphology.Morph) => { internal := true, weight := Prosody.Syllable.Weight.light }) a.exponents.head?
• Aitha2026.caseSuffix (Aitha2026.ParadigmCell.postposition a) = some { internal := false, weight := Prosody.Syllable.Weight.heavy }

theorem Aitha2026.weak_violates_aba : ¬Morphology.IsContiguous fun (c : ParadigmCell) => weakN (caseSuffix c)

The weak paradigm (8) violates *ABA on the containment hierarchy, since the nominative form resurfaces in the genitive, which contains [ACC] ([Cah09]).

theorem Aitha2026.strong_contiguous : Morphology.IsContiguous fun (c : ParadigmCell) => strongN Root.house c.label

The strong paradigm of illu (1) is contiguous on the containment hierarchy.

The singular suffix (§4.2)

inductive Aitha2026.NumContext : Type

The context of Num records that 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 ⋯

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

Equations

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

@[instance_reducible]

instance Aitha2026.instReprNumContext : Repr NumContext

Equations

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

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

The Vocabulary Items of Num in the singular ((40)) insert -ni after -am and 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

• Aitha2026.numSg nExponent = DistributedMorphology.subsetPrinciple Aitha2026.numItems ↑(if nExponent = "am" then [Aitha2026.NumContext.afterAm] else [])

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

Weak nouns take -ni and strong nouns the null singular, so 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) leave the final heavy syllable unparsed, form three degenerate feet, or form 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 }

@[instance_reducible]

instance Aitha2026.instFintypeStemCandidate : Fintype StemCandidate

Equations

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

@[instance_reducible]

instance Aitha2026.instInhabitedStemCandidate : Inhabited StemCandidate

Equations

• Aitha2026.instInhabitedStemCandidate = { default := Aitha2026.instInhabitedStemCandidate.default }

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.stemRanking : List (OptimalityTheory.Constraint StemCandidate)

FT-BIN(μ) ≫ PARSE-SYL ≫ ALL-FT-LEFT ((46)–(48)), each read off a parse's footing as its non-bimoraic feet, its stray syllables, and the feet's distances from the left edge.

Equations

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

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

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

Word- and Phrase-level rankings (§5.2–5.3)

The constraints of the two strata are shared by label; each stratum fixes one order, and each tableau supplies only its candidates' violation marks (Tableau.ofOrder).

inductive Aitha2026.Con : Type

The constraints of (64) and (68).

• distZero : Con
• alignR : Con
• identStress : Con
• ftBin : Con
• complexCoda : Con
• maxMora : Con
• max : Con
• identLength : Con
• onset : 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.complexCoda prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.complexCoda")).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.onset prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Aitha2026.Con.onset")).group prec✝

@[instance_reducible]

instance Aitha2026.instReprCon : Repr Con

Equations

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

def Aitha2026.wordOrder : List Con

The Word-level ranking (64), with ONSET below IDENT-STRESS (§5.2); Hasse siblings are listed in the order of the paper's tableau columns.

Equations

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

def Aitha2026.phraseOrder : List Con

The Phrase-level ranking (68).

Equations

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

Word-level phonology (§5.2)

inductive Aitha2026.WordCandDat : Type

The candidates for dative samudr-am-ní-ki ((59)) keep /mn/, delete /n/ or /m/ with the mora, or 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 }

@[instance_reducible]

instance Aitha2026.instFintypeWordCandDat : Fintype WordCandDat

Equations

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

@[instance_reducible]

instance Aitha2026.instInhabitedWordCandDat : Inhabited WordCandDat

Equations

• Aitha2026.instInhabitedWordCandDat = { default := Aitha2026.instInhabitedWordCandDat.default }

def Aitha2026.WordCandDat.marks : WordCandDat → Con → ℕ

The marks of (59).

Equations

• Aitha2026.WordCandDat.faithful.marks Aitha2026.Con.distZero = 1
• Aitha2026.WordCandDat.deleteN.marks Aitha2026.Con.alignR = 1
• Aitha2026.WordCandDat.deleteN.marks Aitha2026.Con.maxMora = 1
• Aitha2026.WordCandDat.deleteN.marks Aitha2026.Con.max = 2
• Aitha2026.WordCandDat.deleteM.marks Aitha2026.Con.maxMora = 1
• Aitha2026.WordCandDat.deleteM.marks Aitha2026.Con.max = 1
• Aitha2026.WordCandDat.deleteMLengthen.marks Aitha2026.Con.max = 1
• Aitha2026.WordCandDat.deleteMLengthen.marks Aitha2026.Con.identLength = 1
• Aitha2026.WordCandDat.deleteNLengthen.marks Aitha2026.Con.alignR = 1
• Aitha2026.WordCandDat.deleteNLengthen.marks Aitha2026.Con.identLength = 1
• Aitha2026.WordCandDat.deleteNLengthen.marks Aitha2026.Con.max = 2
• x✝¹.marks x✝ = 0

theorem Aitha2026.wordDat_optimal : (OptimalityTheory.Tableau.ofOrder wordOrder WordCandDat.marks).optimal = {WordCandDat.deleteMLengthen}

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

inductive Aitha2026.WordCandNom : Type

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

@[instance_reducible]

instance Aitha2026.instFintypeWordCandNom : Fintype WordCandNom

Equations

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

@[instance_reducible]

instance Aitha2026.instInhabitedWordCandNom : Inhabited WordCandNom

Equations

• Aitha2026.instInhabitedWordCandNom = { default := Aitha2026.instInhabitedWordCandNom.default }

def Aitha2026.WordCandNom.marks : WordCandNom → Con → ℕ

The marks of (62).

Equations

• Aitha2026.WordCandNom.destress.marks Aitha2026.Con.identStress = 1
• Aitha2026.WordCandNom.degenerateFoot.marks Aitha2026.Con.ftBin = 1
• Aitha2026.WordCandNom.deleteI.marks Aitha2026.Con.complexCoda = 1
• Aitha2026.WordCandNom.deleteI.marks Aitha2026.Con.maxMora = 1
• Aitha2026.WordCandNom.deleteI.marks Aitha2026.Con.max = 1
• Aitha2026.WordCandNom.deleteIM.marks Aitha2026.Con.alignR = 1
• Aitha2026.WordCandNom.deleteIM.marks Aitha2026.Con.maxMora = 1
• Aitha2026.WordCandNom.deleteIM.marks Aitha2026.Con.max = 2
• Aitha2026.WordCandNom.deleteNi.marks Aitha2026.Con.maxMora = 1
• Aitha2026.WordCandNom.deleteNi.marks Aitha2026.Con.max = 2
• x✝¹.marks x✝ = 0

theorem Aitha2026.wordNom_optimal : (OptimalityTheory.Tableau.ofOrder wordOrder WordCandNom.marks).optimal = {WordCandNom.deleteNi}

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

inductive Aitha2026.WordCandQ : Type

The candidates for samudr-am-ní-antaṭi-ni with a postposed quantifier ((63)) destress -ni, foot it alone, delete /i/ into /mn/, delete /i/ and /m/ with /n/ as coda, delete /ni/, or delete /i/ and /m/ with /n/ resyllabified as onset.

• destress : WordCandQ
• degenerateFoot : WordCandQ
• deleteI : WordCandQ
• deleteIM : WordCandQ
• deleteNi : WordCandQ
• deleteIMResyllabify : WordCandQ

@[instance_reducible]

instance Aitha2026.instDecidableEqWordCandQ : DecidableEq WordCandQ

Equations

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

def Aitha2026.instReprWordCandQ.repr : WordCandQ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aitha2026.instReprWordCandQ : Repr WordCandQ

Equations

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

@[instance_reducible]

instance Aitha2026.instFintypeWordCandQ : Fintype WordCandQ

Equations

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

@[instance_reducible]

instance Aitha2026.instInhabitedWordCandQ : Inhabited WordCandQ

Equations

• Aitha2026.instInhabitedWordCandQ = { default := Aitha2026.instInhabitedWordCandQ.default }

def Aitha2026.WordCandQ.marks : WordCandQ → Con → ℕ

The marks of (63), with ONSET marked on every candidate whose an lacks an onset.

Equations

• Aitha2026.WordCandQ.destress.marks Aitha2026.Con.identStress = 1
• Aitha2026.WordCandQ.destress.marks Aitha2026.Con.onset = 1
• Aitha2026.WordCandQ.degenerateFoot.marks Aitha2026.Con.ftBin = 1
• Aitha2026.WordCandQ.degenerateFoot.marks Aitha2026.Con.onset = 1
• Aitha2026.WordCandQ.deleteI.marks Aitha2026.Con.distZero = 1
• Aitha2026.WordCandQ.deleteI.marks Aitha2026.Con.max = 1
• Aitha2026.WordCandQ.deleteIM.marks Aitha2026.Con.alignR = 1
• Aitha2026.WordCandQ.deleteIM.marks Aitha2026.Con.onset = 1
• Aitha2026.WordCandQ.deleteIM.marks Aitha2026.Con.max = 2
• Aitha2026.WordCandQ.deleteNi.marks Aitha2026.Con.onset = 1
• Aitha2026.WordCandQ.deleteNi.marks Aitha2026.Con.max = 2
• Aitha2026.WordCandQ.deleteIMResyllabify.marks Aitha2026.Con.identStress = 1
• Aitha2026.WordCandQ.deleteIMResyllabify.marks Aitha2026.Con.max = 2
• x✝¹.marks x✝ = 0

theorem Aitha2026.wordQ_optimal : (OptimalityTheory.Tableau.ofOrder wordOrder WordCandQ.marks).optimal = {WordCandQ.deleteNi}

Before the heavy an the stressed -ni is again deleted, leaving the coda /m/ before an onsetless syllable ((63)).

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 (ParadigmCell.case Telugu.Case.nom)) ∧ WordCandDat.deleteMLengthen.nExponent = weakN (caseSuffix (ParadigmCell.case Telugu.Case.dat))

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

Phrase-level phonology (§5.3)

inductive Aitha2026.PhraseCandP : Type

The 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 : PhraseCandP
• deleteM : PhraseCandP
• deleteN : PhraseCandP
• faithful : PhraseCandP

@[instance_reducible]

instance Aitha2026.instDecidableEqPhraseCandP : DecidableEq PhraseCandP

Equations

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

@[instance_reducible]

instance Aitha2026.instReprPhraseCandP : Repr PhraseCandP

Equations

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

def Aitha2026.instReprPhraseCandP.repr : PhraseCandP → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aitha2026.instFintypePhraseCandP : Fintype PhraseCandP

Equations

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

@[instance_reducible]

instance Aitha2026.instInhabitedPhraseCandP : Inhabited PhraseCandP

Equations

• Aitha2026.instInhabitedPhraseCandP = { default := Aitha2026.instInhabitedPhraseCandP.default }

def Aitha2026.PhraseCandP.marks : PhraseCandP → Con → ℕ

The marks of (66), as printed.

Equations

• Aitha2026.PhraseCandP.deleteMLengthen.marks Aitha2026.Con.max = 1
• Aitha2026.PhraseCandP.deleteM.marks Aitha2026.Con.identStress = 1
• Aitha2026.PhraseCandP.deleteM.marks Aitha2026.Con.max = 1
• Aitha2026.PhraseCandP.deleteN.marks Aitha2026.Con.max = 1
• Aitha2026.PhraseCandP.deleteN.marks Aitha2026.Con.alignR = 1
• Aitha2026.PhraseCandP.faithful.marks Aitha2026.Con.distZero = 1
• Aitha2026.PhraseCandP.faithful.marks Aitha2026.Con.alignR = 2
• x✝¹.marks x✝ = 0

theorem Aitha2026.phraseP_optimal : (OptimalityTheory.Tableau.ofOrder phraseOrder PhraseCandP.marks).optimal = {PhraseCandP.faithful}

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

inductive Aitha2026.PhraseCandQ : Type

The candidates for the Word-level output of (63) at the Phrase level ((67)) keep the onsetless an, resyllabify /m/ as its onset, lengthen /a/ and resyllabify, or foot the shortened dra alone.

• faithful : PhraseCandQ
• resyllabify : PhraseCandQ
• lengthen : PhraseCandQ
• degenerateFoot : PhraseCandQ

@[instance_reducible]

instance Aitha2026.instDecidableEqPhraseCandQ : DecidableEq PhraseCandQ

Equations

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

def Aitha2026.instReprPhraseCandQ.repr : PhraseCandQ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Aitha2026.instReprPhraseCandQ : Repr PhraseCandQ

Equations

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

@[instance_reducible]

instance Aitha2026.instFintypePhraseCandQ : Fintype PhraseCandQ

Equations

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

@[instance_reducible]

instance Aitha2026.instInhabitedPhraseCandQ : Inhabited PhraseCandQ

Equations

• Aitha2026.instInhabitedPhraseCandQ = { default := Aitha2026.instInhabitedPhraseCandQ.default }

def Aitha2026.PhraseCandQ.marks : PhraseCandQ → Con → ℕ

The marks of (67).

Equations

• Aitha2026.PhraseCandQ.faithful.marks Aitha2026.Con.onset = 1
• Aitha2026.PhraseCandQ.resyllabify.marks Aitha2026.Con.identStress = 1
• Aitha2026.PhraseCandQ.resyllabify.marks Aitha2026.Con.alignR = 1
• Aitha2026.PhraseCandQ.resyllabify.marks Aitha2026.Con.maxMora = 1
• Aitha2026.PhraseCandQ.lengthen.marks Aitha2026.Con.identLength = 1
• Aitha2026.PhraseCandQ.lengthen.marks Aitha2026.Con.alignR = 1
• Aitha2026.PhraseCandQ.degenerateFoot.marks Aitha2026.Con.ftBin = 1
• Aitha2026.PhraseCandQ.degenerateFoot.marks Aitha2026.Con.identStress = 1
• Aitha2026.PhraseCandQ.degenerateFoot.marks Aitha2026.Con.alignR = 1
• Aitha2026.PhraseCandQ.degenerateFoot.marks Aitha2026.Con.maxMora = 1
• x✝¹.marks x✝ = 0

theorem Aitha2026.phraseQ_optimal : (OptimalityTheory.Tableau.ofOrder phraseOrder PhraseCandQ.marks).optimal = {PhraseCandQ.resyllabify}

The coda /m/ resyllabifies as the onset of an, shifting stress, samudra.man.ta.ṭi.ni without compensatory lengthening ((67)).

Rerankings (68)

theorem Aitha2026.distZero_alignR_max_reranked : OptimalityTheory.Stratal.Reranked Con.distZero Con.max wordOrder phraseOrder ∧ OptimalityTheory.Stratal.Reranked Con.alignR Con.max wordOrder phraseOrder

*DIST-0 and ALIGN-RIGHT outrank MAX at the Word level and are outranked by it at the Phrase level, so consonants delete at the Word level and are kept and resyllabified at the Phrase level.

theorem Aitha2026.prosodic_segmental_reranked : OptimalityTheory.Stratal.Reranked Con.identStress Con.max wordOrder phraseOrder ∧ OptimalityTheory.Stratal.Reranked Con.maxMora Con.identLength wordOrder phraseOrder

Prosodic faithfulness (IDENT-STRESS, MAX-μ) outranks segmental faithfulness (MAX, IDENT-LENGTH) at the Word level and is outranked by it at the Phrase level.

theorem Aitha2026.identStress_onset_reranked : OptimalityTheory.Stratal.Reranked Con.identStress Con.onset wordOrder phraseOrder

IDENT-STRESS outranks ONSET at the Word level and ONSET outranks it at the Phrase level, so the onsetless an of (63) is resyllabified only in (67).