The incoherent stress of Kuikuro

Formalization of [BFK+25] (NLLT 43). Kuikuro builds iambic feet left to right with final trochaic reversal; the last foot heads the word, and the primary stress is the head of the head foot (p. 2365). The paper's title result is that the default High tone does not dock on this syllable: a tone domain left-aligns to the primary stress of the phrase and expands rightward up to (but not including) the next foot head — Culminativity-H ((7)), the paper's one new constraint — so the High target can surface up to three syllables away from the stress it is a correlate of (§7), dissociating the metrically most prominent syllable from the phonetically salient one ([Gor16]'s incoherence, extended).

Main definitions

• fell, weFell, annatto — words in isolation (Figs. 1–2, §1) as Prosody.Trees; annattoFell — the two-word phrase of Fig. 3, with the noun as phrase-head word.
• toneDomainTail, toneTarget — rightward-maximal tone-domain expansion over a grid: the run of unstressed columns after the phrase head, capped before the next foot head and the phrase-final syllable ((4)–(7)).

Main results

• footing_optimal — trochaic reversal is OT-optimal under *V:]φ ≫ Parse-σ ≫ Iamb ((1)–(3), Table 2).
• isHeaded_*, headTerminals_* — each word's primary stress is its unique head terminal (metrical culminativity, [Hym06]).
• toneDomainTail_unstressed — expansion never admits a stressed syllable: the Culminativity-H of ((7)) holds of every predicted domain by construction.
• tone_coherent_in_isolation, stress_tone_incoherence — in isolation the High target is the head terminal itself; in the phrase it is a height-1 syllable three to the right of the peak, blocked by the next foot head.

Deferred alongside lexical tone (§5): lexical long vowels (Max-μ, Tables 3–4), word minimality (§3.5), final shortening (§4.1), and the generality of initial-vowel unparsing (§4.3). Weights: 1 = short σ, 2 = long σ (iambic lengthening); a foot's isHead σ is its head, and the head foot/word carries isHead := true.

References

• [BFK+25] — the paper.
• [LP77], [Hay95b], [PS93] — the grid, foot typology, and violable-constraint machinery.
• [Gor16] — incoherent stress; [Hym06] — culminativity.

Words in isolation ([BFK+25] §3)

def BeckerEtAl2025.fell : Prosody.Tree

[(ala:)(makí:)lɨ] 's/he fell' ([BFK+25] Fig. 1): two iambs and a stray final σ. The rightmost foot heads the word, so the long [kí:] is the primary stress.

Equations

• BeckerEtAl2025.fell = Prosody.Tree.om [Prosody.Tree.ft false [Prosody.Tree.σ 1, Prosody.Tree.σ 2 true], Prosody.Tree.ft true [Prosody.Tree.σ 1, Prosody.Tree.σ 2 true], Prosody.Tree.σ 1]

def BeckerEtAl2025.weFell : Prosody.Tree

[(tsiha:)(lama:)(kílɨ)] 'we fell' ([BFK+25] Fig. 2): even parity, so the final two short syllables reverse to a trochee — the head foot — whose initial [kí] is the primary stress.

Equations

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

def BeckerEtAl2025.annatto : Prosody.Tree

[(umí:)ŋi] 'annatto' ([BFK+25] §1, p. 2365): one iamb and a stray final σ; the long [mí:] is the primary stress.

Equations

• BeckerEtAl2025.annatto = Prosody.Tree.om [Prosody.Tree.ft true [Prosody.Tree.σ 1, Prosody.Tree.σ 2 true], Prosody.Tree.σ 1]

The grid: secondary stress on every foot head, primary on the head foot's

Reading Tree.columns ∘ the footing recovers the stress profile: 1 unstressed, 2 a secondary (a non-head foot's head), 3 the primary (the head foot's head).

theorem BeckerEtAl2025.gridColumns_fell : fell.columns = [1, 2, 1, 3, 1]

theorem BeckerEtAl2025.gridColumns_weFell : weFell.columns = [1, 2, 1, 2, 3, 1]

theorem BeckerEtAl2025.gridColumns_annatto : annatto.columns = [1, 3, 1]

Primary stress is the head terminal ([BFK+25] p. 2365)

Each word has a unique head terminal (Tree.IsHeaded — metrical culminativity, Liberman & Prince's head-terminal uniqueness; cf. [Hym06]), and it is exactly the head syllable of the head foot — the long kí:/mí:, or the reversed-trochee's initial kí. The primary stress is read off the grid's live column as an element.

theorem BeckerEtAl2025.isHeaded_fell : fell.IsHeaded

theorem BeckerEtAl2025.isHeaded_weFell : weFell.IsHeaded

theorem BeckerEtAl2025.isHeaded_annatto : annatto.IsHeaded

theorem BeckerEtAl2025.headTerminals_fell : fell.headTerminals = [Prosody.Tree.σ 2 true]

's/he fell': the head terminal is the long kí: (head of the rightmost iamb).

theorem BeckerEtAl2025.headTerminals_weFell : weFell.headTerminals = [Prosody.Tree.σ 1 true]

'we fell': the head terminal is the reversed trochee's initial short kí.

theorem BeckerEtAl2025.headTerminals_annatto : annatto.headTerminals = [Prosody.Tree.σ 2 true]

'annatto': the head terminal is the long mí:.

theorem BeckerEtAl2025.isHeadTerminal_fell : fell.IsHeadTerminal (Prosody.Tree.σ 2 true)

The same fact declaratively ([LP77]): kí: is the head terminal of fell — reached from ω by an all-head descent (ω → head foot → head σ), Tree.IsHeadTerminal — lifted from the computed list by Tree.headTerminal_sound, not just by computing the list.

The trochaic reversal is OT-optimal ([BFK+25] §3.1, Table 2)

Why the final foot reverses to a trochee: an even-parity /σσσσ/ parsed as two iambs leaves a phrase-final long vowel (*V:]φ); leaving the last two σ unparsed violates Parse-σ; so they parse as a trochee, violating only the low-ranked Iamb. Ranking *V:]φ ≫ Parse-σ ≫ Iamb ([BFK+25] (1)–(3), Table 2).

inductive BeckerEtAl2025.FootingCand : Type

The three footings of /σσσσ/ weighed in [BFK+25]'s Table 2.

• twoIambs : FootingCand

  (σ́σ:)(σ́σ:) — two iambs; a final long vowel.

• iambStrays : FootingCand

  (σ́σ:)σσ — one iamb, the last two σ unparsed.

• iambTrochee : FootingCand

  (σ́σ:)(´σσ) — an iamb and a final trochee (the optimum).

@[instance_reducible]

instance BeckerEtAl2025.instDecidableEqFootingCand : DecidableEq FootingCand

Equations

• BeckerEtAl2025.instDecidableEqFootingCand x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BeckerEtAl2025.instReprFootingCand : Repr FootingCand

Equations

• BeckerEtAl2025.instReprFootingCand = { reprPrec := BeckerEtAl2025.instReprFootingCand.repr }

def BeckerEtAl2025.instReprFootingCand.repr : FootingCand → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance BeckerEtAl2025.instFintypeFootingCand : Fintype FootingCand

Equations

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

@[instance_reducible]

instance BeckerEtAl2025.instInhabitedFootingCand : Inhabited FootingCand

Equations

• BeckerEtAl2025.instInhabitedFootingCand = { default := BeckerEtAl2025.instInhabitedFootingCand.default }

def BeckerEtAl2025.FootingCand.toTree : FootingCand → Prosody.Tree

Each candidate as a footed tree (rightmost foot the head).

Equations

• One or more equations did not get rendered due to their size.
• BeckerEtAl2025.FootingCand.iambStrays.toTree = Prosody.Tree.om [Prosody.Tree.ft true [Prosody.Tree.σ 1, Prosody.Tree.σ 2 true], Prosody.Tree.σ 1, Prosody.Tree.σ 1]

def BeckerEtAl2025.cParse : OptimalityTheory.Constraint FootingCand

Parse-σ ([BFK+25] (1)): one mark per unparsed (stray) σ — a σ-leaf under ω.

Equations

• BeckerEtAl2025.cParse c = match c.toTree with | RoseTree.node value cs => (List.filter (fun (d : RoseTree Prosody.Constituent) => decide (d.value.level = Prosody.Level.syl)) cs).length

def BeckerEtAl2025.cIamb : OptimalityTheory.Constraint FootingCand

Iamb ([BFK+25] (2)): one mark per foot that is not right-headed (head σ ≠ final).

Equations

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

def BeckerEtAl2025.cStarV : OptimalityTheory.Constraint FootingCand

*V:]φ ([BFK+25] (3)): one mark for a long vowel in the phrase-final σ (for a one-word phrase, the word-final σ).

Equations

• BeckerEtAl2025.cStarV c = match c.toTree.terminals.getLast? with | some leaf => if decide ((RoseTree.value leaf).weight? = some 2) = true then 1 else 0 | none => 0

def BeckerEtAl2025.candidates : List FootingCand

Equations

• BeckerEtAl2025.candidates = [BeckerEtAl2025.FootingCand.twoIambs, BeckerEtAl2025.FootingCand.iambStrays, BeckerEtAl2025.FootingCand.iambTrochee]

def BeckerEtAl2025.footingRanking : List (OptimalityTheory.Constraint FootingCand)

The ranking *V:]φ ≫ Parse-σ ≫ Iamb ([BFK+25] Table 2).

Equations

• BeckerEtAl2025.footingRanking = [BeckerEtAl2025.cStarV, BeckerEtAl2025.cParse, BeckerEtAl2025.cIamb]

theorem BeckerEtAl2025.starV_violations : List.map cStarV candidates = [1, 0, 0]

The violation profiles ([BFK+25] Table 2):

candidate	*V:]φ	Parse-σ	Iamb
(σ́σ:)(σ́σ:)	1*	0	0
(σ́σ:)σσ	0	2*	0
☞ (σ́σ:)(´σσ)	0	0	1

Max-μ — which governs lexical long vowels (Tables 4 and 6; ranked below *V:]φ and above Parse-σ) — plays no role among these all-short candidates and is omitted.

theorem BeckerEtAl2025.parse_violations : List.map cParse candidates = [0, 2, 0]

theorem BeckerEtAl2025.iamb_violations : List.map cIamb candidates = [0, 0, 1]

theorem BeckerEtAl2025.footing_optimal : (OptimalityTheory.Tableau.ofFintype footingRanking).optimal = {FootingCand.iambTrochee}

The trochaic reversal wins ([BFK+25] Table 2): under *V:]φ ≫ Parse-σ ≫ Iamb the optimal footing of /σσσσ/ is the iamb + final trochee — no final long vowel, no unparsed σ, at the cost of one (low-ranked) non-right-headed foot.

The tone domain and Culminativity-H ([BFK+25] §4.2)

A phrase carries one High tone. Its domain left-aligns to the primary stress of the phrase ((4)), expands rightward maximally ((5)), excludes the phrase-final syllable ((6)), and stops before the next foot head — Culminativity-H ((7)): at most one foot head per domain. Over a grid, expansion takes the run of height-1 columns after the head column; the High target is the domain's last syllable.

def BeckerEtAl2025.toneDomainTail (cols : Prosody.Grid) (head : ℕ) : Prosody.Grid

The heights of the syllables a tone domain expands over: the unstressed (height-1) run after the phrase-head column, capped before the phrase-final syllable ((5)–(7)).

Equations

• BeckerEtAl2025.toneDomainTail cols head = List.takeWhile (fun (x : ℕ) => decide (x ≤ 1)) (List.drop (head + 1) (List.dropLast cols))

def BeckerEtAl2025.toneTarget (cols : Prosody.Grid) (head : ℕ) : ℕ

The High-tone target: the last syllable of the maximally expanded domain.

Equations

• BeckerEtAl2025.toneTarget cols head = head + List.length (BeckerEtAl2025.toneDomainTail cols head)

theorem BeckerEtAl2025.toneDomainTail_unstressed (cols : Prosody.Grid) (head h : ℕ) : h ∈ toneDomainTail cols head → h ≤ 1

Culminativity-H holds of every predicted domain by construction: expansion never admits a stressed syllable, so no domain contains a second foot head ((7)).

theorem BeckerEtAl2025.tone_coherent_in_isolation : toneTarget fell.columns 3 = 3 ∧ toneTarget weFell.columns 4 = 4 ∧ toneTarget annatto.columns 1 = 1

In isolation the tone is coherent: the domain cannot expand — the phrase-final cap ((6)) closes it at the head — so the High target is the head terminal itself, the default penultimate tone of §3. Head indices are visible in gridColumns_* above.

theorem BeckerEtAl2025.isCulminative_words : fell.columns.IsCulminative ∧ weFell.columns.IsCulminative ∧ annatto.columns.IsCulminative

Each word's grid is culminative: exactly one peak column, the head terminal's.

def BeckerEtAl2025.annattoFell : Prosody.Tree

The two-word phrase [(umɨ:)ŋi ⟨a⟩(láma:)(kilɨ)] 'the annatto fell' (Fig. 3): the noun is the phrase-head word, and the verb refoots in phrasal position — initial vowel unparsed (§4.3), one iamb, and a final trochee.

Equations

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

theorem BeckerEtAl2025.gridColumns_annattoFell : annattoFell.columns = [1, 4, 1, 1, 1, 2, 3, 1]

The phrase grid: the noun's head terminal is promoted to the phrase peak (height 4).

theorem BeckerEtAl2025.annattoFell_headed : annattoFell.IsHeaded ∧ annattoFell.columns.IsCulminative

The phrase is headed, culminatively, by the noun's long [mɨ:].

theorem BeckerEtAl2025.stress_tone_incoherence : toneTarget annattoFell.columns 1 = 4 ∧ List.getD annattoFell.columns 4 0 = 1 ∧ List.getD annattoFell.columns 5 0 = 2

The incoherence (§1, §7): from the phrase peak (index 1), the tone domain expands over three unstressed syllables and targets index 4 — the height-1 [lá] — while expansion is blocked by the next foot head [ma:] (index 5, height 2). The metrically most prominent syllable and the High-toned phonetically salient one come apart.