Relating to the grid: the End Rule ([Pri83])

[Pri83]'s Relating to the Grid reads a metrical grid off a prosodic tree by the Relative Prominence Projection Rule ([LP77]) — formalised as Prosody.Tree.columns — and observes that a uniform metrical tree (every constituent strong on the same side) projects to a grid whose single strongest column sits at one end: the End Rule.

This file stress-tests the grid projection against that prediction. A uniformly right-strong (iambic) word and a uniformly left-strong (trochaic) word project, by decide, to staircase column profiles whose strict maximum is the rightmost (resp. leftmost) syllable — the End Rule, recovered through Prosody.Tree.columns. It also leans on the projection's information loss: the grid records where the prominence peak is, not the bracketing that produced it (Prosody.Grid.ofTree_not_injective).

Uniform metrical words

Every foot is binary; the head sits consistently on the right (iambic) or the left (trochaic), and the head foot likewise — so the head-projection chain runs to one edge of the word.

def Prince1983.σh : Prosody.Tree

A head (strong) syllable.

Equations

• Prince1983.σh = Prosody.Tree.σ 0 true

def Prince1983.σw : Prosody.Tree

A weak syllable.

Equations

• Prince1983.σw = Prosody.Tree.σ

def Prince1983.ftH (cs : List Prosody.Tree) : Prosody.Tree

A head (strong) foot over cs.

Equations

• Prince1983.ftH cs = Prosody.Tree.ft true cs

def Prince1983.ftW (cs : List Prosody.Tree) : Prosody.Tree

A weak foot over cs.

Equations

• Prince1983.ftW cs = Prosody.Tree.ft false cs

def Prince1983.om (cs : List Prosody.Tree) : Prosody.Tree

A prosodic word over cs.

Equations

• Prince1983.om cs = Prosody.Tree.om cs

def Prince1983.rightStrong : Prosody.Tree

A uniformly right-strong word: the head foot is rightmost and every foot is iambic (head syllable rightmost), so prominence climbs toward the right edge.

Equations

• Prince1983.rightStrong = Prince1983.om [Prince1983.ftW [Prince1983.σw, Prince1983.σh], Prince1983.ftH [Prince1983.σw, Prince1983.σh]]

def Prince1983.leftStrong : Prosody.Tree

A uniformly left-strong word: the head foot is leftmost and every foot is trochaic (head syllable leftmost), so prominence climbs toward the left edge.

Equations

• Prince1983.leftStrong = Prince1983.om [Prince1983.ftH [Prince1983.σh, Prince1983.σw], Prince1983.ftW [Prince1983.σh, Prince1983.σw]]

The End Rule

def Prince1983.EndRuleRight (t : Prosody.Tree) : Prop

End Rule, right ([Pri83]): the rightmost grid column strictly dominates every other — the prominence peak is at the right edge.

Equations

• Prince1983.EndRuleRight t = ∀ h ∈ List.dropLast t.columns, h < (List.getLast? t.columns).getD 0

@[implicit_reducible]

instance Prince1983.instDecidableEndRuleRight (t : Prosody.Tree) : Decidable (EndRuleRight t)

Equations

• Prince1983.instDecidableEndRuleRight t = id inferInstance

def Prince1983.EndRuleLeft (t : Prosody.Tree) : Prop

End Rule, left ([Pri83]): the leftmost grid column strictly dominates every other — the prominence peak is at the left edge.

Equations

• Prince1983.EndRuleLeft t = ∀ h ∈ List.tail t.columns, h < List.headD t.columns 0

@[implicit_reducible]

instance Prince1983.instDecidableEndRuleLeft (t : Prosody.Tree) : Decidable (EndRuleLeft t)

Equations

• Prince1983.instDecidableEndRuleLeft t = id inferInstance

The RPPR projects uniform trees to End-Rule grids

theorem Prince1983.gridColumns_rightStrong : rightStrong.columns = [1, 2, 1, 3]

The right-strong word projects to a staircase peaking at the right edge.

theorem Prince1983.gridColumns_leftStrong : leftStrong.columns = [3, 1, 2, 1]

The left-strong word projects to a staircase peaking at the left edge.

theorem Prince1983.endRuleRight_rightStrong : EndRuleRight rightStrong

End Rule (right): a uniformly right-strong word is strongest at its right edge.

theorem Prince1983.endRuleLeft_leftStrong : EndRuleLeft leftStrong

End Rule (left): a uniformly left-strong word is strongest at its left edge.

theorem Prince1983.headTerminals_rightStrong : rightStrong.headTerminals = [σh]

The End-Rule peak IS the head terminal ([Pri83]; [LP77]): the rightmost column End Rule Right promotes is the head foot's head σ — the head terminal (Liberman & Prince's head terminal) as a node, not just the tallest height.

theorem Prince1983.endRulePeak_is_head : rightStrong.headHeights = [rightStrong.columns.peak]

And its prominence is the grid peak: on a uniform (non-recursive headed) word the head terminal's height is the peak — the concrete instance of Prosody.Tree.headHeights_eq_peak.