The metrical grid

[LP77] [Pri83] [Hay95a] [HV87] [IM09]

The metrical grid is the prominence dual of the prosodic word: a column of marks over each syllable, taller standing for greater relative prominence (primary > secondary > unstressed). This file is organised as a small tower of objects, each adding structure to the plain grid and each connected to the plainer one below by a forgetful map:

Marks        rendered rows of marks; the Continuous Column Constraint lives here
  ↑ rows                                    (Prince 1983's autonomous grid)
Grid         column heights — the pure rhythmic grid
  ↑ toGrid                                   (add the head terminal)
MarkedGrid   a grid whose columns carry the head-spine (Liberman & Prince's head terminals)
  ↑ project                                  (the RPPR)
Tree         the bracketed grid — brackets at all layers ([hayes-1995] §3.5)

The projection Grid.project is the Relative Prominence Projection Rule ([LP77]): a homomorphism from the tree into the head-marked grid, built from a small algebra (cell/juxtapose/promote/clear). The grid readers (columns, terminals, headTerminals, headHeights) are the forgetful maps out of it. What the forgetful map onto the pure grid drops is theorem-shaped: constituency (Grid.ofTree_not_injective; the grid underdetermines bracketing, [Hay95a] §3.8) and, under recursion, order-invariant culminativity (Grid.not_culminative_under_recursion).

Main definitions

• Grid / Grid.peak / Grid.IsCulminative — the pure grid (column heights) and its invariants.
• Marks / Marks.IsContinuous / Grid.rows — the rendered grid and the Continuous Column Constraint, which holds for any rendered grid by construction.
• MarkedGrid / Grid.project — the head-marked grid and the RPPR projection from a tree.
• Tree.columns / Tree.headTerminals / Tree.headHeights / Tree.IsHeaded — the grid readers.

Main results

• Grid.ofTree_isContinuous — the Continuous Column Constraint, by construction (free).
• Grid.peak_toProsTree — head-preservation for a foot (its grid peaks at the head σ).
• Tree.headHeights_eq_peak — on a non-recursive headed word the head terminal's height is the grid peak: metrical primary stress is the tallest column.
• Grid.ofTree_not_injective / Grid.not_culminative_under_recursion — what the projection forgets: constituency, and order-invariant culminativity under recursion.
• Grid.head_below_peak_under_recursion / Grid.head_below_peak_unlayered — the peak can desert the head terminal under recursion or without Layeredness.

The tower carriers

The four objects of the tower (see the module header): the rendered Marks, the pure Grid, and the head-marked grid MarkedGrid built from Columns. Operations follow, one namespace each.

@[reducible, inline]

abbrev Prosody.Marks : Type

A rendered metrical grid: rows of head-marks, bottom row first.

Equations

• Prosody.Marks = List (List Bool)

@[reducible, inline]

abbrev Prosody.Grid : Type

A metrical grid ([Hay95a] §3.2): the beat count (column height) over each position, left to right. Absolute heights carry no significance; only relative prominence does.

Equations

• Prosody.Grid = List ℕ

structure Prosody.Column (α : Type u_1) : Type u_1

One column of a marked grid: the σ-leaf it sits over, its mark count (height), and whether it lies on the current head-spine (the head terminal so far, [LP77]).

• terminal : α

  The σ-leaf under this column.

• height : ℕ

  The column height = number of grid marks.

• onSpine : Bool

  Whether this column is (so far) the head terminal.

@[reducible, inline]

abbrev Prosody.MarkedGrid (α : Type u_1) : Type u_1

A grid whose columns carry the head-spine (the head terminals, [LP77]) — the pure grid plus a head marking. It deliberately does not record the full bracketing (that is Tree; Grid.ofTree_not_injective is the honest statement that heights lose it).

Equations

• Prosody.MarkedGrid α = List (Prosody.Column α)

Marks: the Continuous Column Constraint

def Prosody.Marks.IsContinuous (m : Marks) : Prop

The Continuous Column Constraint ([Pri83]; [Hay95a] §3.4.2 (9)): no column has a gap. A violable predicate on an arbitrary rendered grid.

Equations

• m.IsContinuous = List.IsChain (fun (lower upper : List Bool) => Prosody.Marks.rowSubmask✝ upper lower = true) m

@[implicit_reducible]

instance Prosody.Marks.instDecidableIsContinuous (m : Marks) : Decidable m.IsContinuous

Equations

• m.instDecidableIsContinuous = id inferInstance

The head-marked grid: the marked-grid algebra

def Prosody.MarkedGrid.toGrid {α : Type u_1} (b : MarkedGrid α) : Grid

Forget the marking: the underlying pure grid of column heights.

Equations

• b.toGrid = List.map (fun (x : Prosody.Column α) => x.height) b

def Prosody.MarkedGrid.terminals {α : Type u_1} (b : MarkedGrid α) : List α

The terminals under the columns, left to right.

Equations

• b.terminals = List.map (fun (x : Prosody.Column α) => x.terminal) b

def Prosody.MarkedGrid.headHeights {α : Type u_1} (b : MarkedGrid α) : Grid

The head-spine columns' heights — the head terminals' prominences.

Equations

• b.headHeights = List.map (fun (x : Prosody.Column α) => x.height) (List.filter (fun (x : Prosody.Column α) => x.onSpine) b)

def Prosody.MarkedGrid.headTerminals {α : Type u_1} (b : MarkedGrid α) : List α

The head-spine terminals — the head terminals.

Equations

• b.headTerminals = List.map (fun (x : Prosody.Column α) => x.terminal) (List.filter (fun (x : Prosody.Column α) => x.onSpine) b)

def Prosody.MarkedGrid.cell {α : Type u_1} (x : α) : MarkedGrid α

A single terminal: one column of height 1, on its own head-spine.

Equations

• Prosody.MarkedGrid.cell x = [{ terminal := x, height := 1, onSpine := true }]

def Prosody.MarkedGrid.juxtapose {α : Type u_1} (bs : List (MarkedGrid α)) : MarkedGrid α

Juxtapose sibling constituents.

Equations

• Prosody.MarkedGrid.juxtapose bs = bs.flatten

def Prosody.MarkedGrid.promote {α : Type u_1} (b : MarkedGrid α) : MarkedGrid α

The head-projection step of the RPPR ([LP77]): a head edge raises the head by one grid mark — bump every head-spine column.

Equations

• b.promote = List.map (fun (c : Prosody.Column α) => { terminal := c.terminal, height := c.height + if c.onSpine = true then 1 else 0, onSpine := c.onSpine }) b

def Prosody.MarkedGrid.clear {α : Type u_1} (b : MarkedGrid α) : MarkedGrid α

A weak edge: heights freeze, the head-spine marking is dropped.

Equations

• b.clear = List.map (fun (c : Prosody.Column α) => { terminal := c.terminal, height := c.height, onSpine := false }) b

def Prosody.MarkedGrid.edge {α : Type u_1} (isHead : Bool) (b : MarkedGrid α) : MarkedGrid α

One edge of the descent: a head edge projects, any other clears the spine.

Equations

• Prosody.MarkedGrid.edge isHead b = if isHead = true then b.promote else b.clear

@[simp]

theorem Prosody.MarkedGrid.edge_true {α : Type u_1} (b : MarkedGrid α) : edge true b = b.promote

@[simp]

theorem Prosody.MarkedGrid.edge_false {α : Type u_1} (b : MarkedGrid α) : edge false b = b.clear

The algebra of the marked grid

@[simp]

theorem Prosody.MarkedGrid.toGrid_cell {α : Type u_1} (x : α) : (cell x).toGrid = [1]

@[simp]

theorem Prosody.MarkedGrid.headHeights_cell {α : Type u_1} (x : α) : (cell x).headHeights = [1]

@[simp]

theorem Prosody.MarkedGrid.headTerminals_cell {α : Type u_1} (x : α) : (cell x).headTerminals = [x]

@[simp]

theorem Prosody.MarkedGrid.toGrid_clear {α : Type u_1} (b : MarkedGrid α) : b.clear.toGrid = b.toGrid

@[simp]

theorem Prosody.MarkedGrid.headHeights_clear {α : Type u_1} (b : MarkedGrid α) : b.clear.headHeights = []

@[simp]

theorem Prosody.MarkedGrid.headTerminals_clear {α : Type u_1} (b : MarkedGrid α) : b.clear.headTerminals = []

@[simp]

theorem Prosody.MarkedGrid.headHeights_promote {α : Type u_1} (b : MarkedGrid α) : b.promote.headHeights = List.map (fun (x : ℕ) => x + 1) b.headHeights

@[simp]

theorem Prosody.MarkedGrid.headTerminals_promote {α : Type u_1} (b : MarkedGrid α) : b.promote.headTerminals = b.headTerminals

@[simp]

theorem Prosody.MarkedGrid.toGrid_juxtapose {α : Type u_1} (bs : List (MarkedGrid α)) : (juxtapose bs).toGrid = List.flatMap (fun (x : MarkedGrid α) => x.toGrid) bs

@[simp]

theorem Prosody.MarkedGrid.headHeights_juxtapose {α : Type u_1} (bs : List (MarkedGrid α)) : (juxtapose bs).headHeights = List.flatMap (fun (x : MarkedGrid α) => x.headHeights) bs

@[simp]

theorem Prosody.MarkedGrid.headTerminals_juxtapose {α : Type u_1} (bs : List (MarkedGrid α)) : (juxtapose bs).headTerminals = List.flatMap (fun (x : MarkedGrid α) => x.headTerminals) bs

@[simp]

theorem Prosody.MarkedGrid.headHeights_edge {α : Type u_1} (b : MarkedGrid α) (h : Bool) : (edge h b).headHeights = if h = true then List.map (fun (x : ℕ) => x + 1) b.headHeights else []

@[simp]

theorem Prosody.MarkedGrid.headTerminals_edge {α : Type u_1} (b : MarkedGrid α) (h : Bool) : (edge h b).headTerminals = if h = true then b.headTerminals else []

Grid: peak, the RPPR projection, and the readers

The pure grid: peak, culminativity, rendering

def Prosody.Grid.peak (g : Grid) : ℕ

The prominence peak: the tallest column.

Equations

• g.peak = List.foldr max 0 g

@[simp]

theorem Prosody.Grid.peak_nil : peak [] = 0

theorem Prosody.Grid.le_peak {g : Grid} {h : ℕ} (hh : h ∈ g) : h ≤ g.peak

Every column is at most the peak.

theorem Prosody.Grid.peak_le {g : Grid} {n : ℕ} (h : ∀ x ∈ g, x ≤ n) : g.peak ≤ n

The peak is bounded by any common bound on the columns.

def Prosody.Grid.IsCulminative (g : Grid) : Prop

Culminativity ([LP77]; [Hay95a]): exactly one column is tallest. Note this is strictly stronger than having a unique head terminal (IsHeaded) — two columns can tie.

Equations

• g.IsCulminative = (List.countP (fun (x : ℕ) => x == g.peak) g = 1)

@[implicit_reducible]

instance Prosody.Grid.instDecidableIsCulminative (g : Grid) : Decidable g.IsCulminative

Equations

• g.instDecidableIsCulminative = id inferInstance

def Prosody.Grid.rows (g : Grid) : Marks

Render a grid as stacked rows of marks: row r carries a mark over every column taller than r.

Equations

• g.rows = List.map (fun (r : ℕ) => List.map (fun (x : ℕ) => decide (r < x)) g) (List.range g.peak)

theorem Prosody.Grid.rows_isContinuous (g : Grid) : g.rows.IsContinuous

The Continuous Column Constraint is free. Every rendered grid satisfies it, because a column is a solid stack of marks by construction — continuity is the shape of a histogram, not a theorem about trees ([Hay95a] §3.4.2).

The RPPR projection

def Prosody.Tree.project (t : Tree) : MarkedGrid Tree

The Relative Prominence Projection Rule ([LP77]) as a homomorphism Tree → MarkedGrid: a σ-leaf is one cell; any other node juxtaposes its children, projecting across head edges and clearing the spine across the rest.

Equations

• t.project = (RoseTree.fold Prosody.Tree.projectStep✝ t).2

@[simp]

theorem Prosody.Tree.project_node (a : Constituent) (cs : List Tree) : project (RoseTree.node a cs) = if a.isSyl = true ∧ cs = [] then MarkedGrid.cell (RoseTree.node a []) else MarkedGrid.juxtapose (List.map (fun (c : Tree) => MarkedGrid.edge (RoseTree.value c).isHead c.project) cs)

Reading the grid off a tree (the forgetful maps)

def Prosody.Tree.terminals (t : Tree) : List Tree

The σ-leaves of a tree, left to right: the terminal tier the grid sits over.

Equations

• t.terminals = t.project.terminals

def Prosody.Tree.columns (t : Tree) : Grid

The grid-column heights ([LP77]): each σ-leaf's height is 1 plus the contiguous run of head edges ending at it.

Equations

• t.columns = t.project.toGrid

def Prosody.Tree.headTerminals (t : Tree) : List Tree

The head terminals ([LP77]): the σ-leaves reached from the root by all head edges.

Equations

• t.headTerminals = t.project.headTerminals

def Prosody.Tree.headHeights (t : Tree) : Grid

The head terminals' prominences: the live cells' heights.

Equations

• t.headHeights = t.project.headHeights

def Prosody.Tree.IsHeaded (t : Tree) : Prop

A tree is headed when it has a unique head terminal.

Equations

• t.IsHeaded = (List.length t.headHeights = 1)

@[implicit_reducible]

instance Prosody.Tree.instDecidableIsHeaded (t : Tree) : Decidable t.IsHeaded

Equations

• t.instDecidableIsHeaded = id inferInstance

def Prosody.Grid.ofTree (t : Tree) : Marks

The metrical grid of a tree, as stacked rows.

Equations

• Prosody.Grid.ofTree t = t.columns.rows

theorem Prosody.Grid.ofTree_isContinuous (t : Tree) : (ofTree t).IsContinuous

Grid.ofTree always satisfies the Continuous Column Constraint ([Pri83]; [Hay95a]) — free from Grid.rows_isContinuous: a projected grid is a histogram.

The reader recursions

Each reader is a homomorphism out of the marked-grid algebra, so on a node it is the juxtaposition of the children's readings, projected across head edges. These fuse project_node with the algebra once, so the downstream proofs never re-walk the fold.

theorem Prosody.Tree.columns_node (a : Constituent) (cs : List Tree) : columns (RoseTree.node a cs) = if a.isSyl = true ∧ cs = [] then [1] else List.flatMap (fun (c : Tree) => (MarkedGrid.edge (RoseTree.value c).isHead c.project).toGrid) cs

theorem Prosody.Tree.headHeights_node (a : Constituent) (cs : List Tree) : headHeights (RoseTree.node a cs) = if a.isSyl = true ∧ cs = [] then [1] else List.flatMap (fun (c : Tree) => if (RoseTree.value c).isHead = true then List.map (fun (x : ℕ) => x + 1) c.headHeights else []) cs

theorem Prosody.Tree.headTerminals_node (a : Constituent) (cs : List Tree) : headTerminals (RoseTree.node a cs) = if a.isSyl = true ∧ cs = [] then [RoseTree.node a []] else List.flatMap (fun (c : Tree) => if (RoseTree.value c).isHead = true then c.headTerminals else []) cs

The head terminals compute the head-terminal relation

inductive Prosody.Tree.IsHeadTerminal : Tree → Tree → Prop

leaf is a head terminal of t, reached from the root by an all-head descent.

• leaf {a : Constituent} (ha : a.isSyl = true) : IsHeadTerminal (RoseTree.node a []) (RoseTree.node a [])
• head {a : Constituent} {cs : List (RoseTree Constituent)} {c leaf : Tree} : c ∈ cs → (RoseTree.value c).isHead = true → c.IsHeadTerminal leaf → IsHeadTerminal (RoseTree.node a cs) leaf

theorem Prosody.Tree.headTerminal_sound {t leaf : Tree} (h : leaf ∈ t.headTerminals) : t.IsHeadTerminal leaf

Soundness of headTerminals ([LP77]): every head terminal the projection computes really is one — reached from the root by an all-head descent. (The decide-verified lists give the converse concretely, so the full iff is not needed.)

Head-preservation: the foot commuting square

Reading a Foot's grid recovers its head — the depth-1 core of the transport story: its column heights are 2 at the head σ and 1 elsewhere, so the grid peaks at 2.

theorem Prosody.Tree.columns_toProsTree {S : Type u_1} (w : S → Syllable.Weight) (f : Foot S) : (Foot.toProsTree w f).columns = f.toGrid

Head-preservation for a foot ([LP77]): projecting a foot's prosodic tree recovers its metrical grid — the commuting square columns ∘ toProsTree = toGrid.

theorem Prosody.Tree.peak_toProsTree {S : Type u_1} (w : S → Syllable.Weight) (f : Foot S) : (Foot.toProsTree w f).columns.peak = 2

A foot's grid peaks at 2 — its head σ carries the primary mark ([LP77]).

What the grid forgets

The forgetful map onto the pure grid is one-way: it drops constituency (ofTree_not_injective; [Hay95a] §3.8 argues for bracketing precisely because the grid underdetermines it) and, under recursion, order-invariant culminativity (not_culminative_under_recursion).

theorem Prosody.Grid.ofTree_not_injective : ¬Function.Injective ofTree

The grid render is not injective — it forgets constituency: a σ parsed under a foot and the same σ left bare render to the same grid ([Hay95a] §3.8).

theorem Prosody.Tree.not_culminative_under_recursion : ∃ (t : Tree), IsWord t ∧ ¬t.columns.IsCulminative

Recursion can break culminativity: a word recursively dominating another word, each heading its own σ, has two equally tall columns — no unique peak.

The word peak is the head terminal

On a non-recursive headed word the grid peak is the head terminal ([LP77]): metrical primary stress is the tallest column. Recursion is the sole obstruction, and — this being [Hay95a] §3.4.2(C)'s "the higher grid mark may only be assigned to a syllable that already bears stress" — the peak sits atop a foot head.

theorem Prosody.Tree.headHeights_sublist_columns (t : Tree) : List.Sublist t.headHeights t.columns

Head-terminal heights are a sublist of the columns.

theorem Prosody.Tree.headHeight_le_peak {t : Tree} {h : ℕ} (hh : h ∈ t.headHeights) : h ≤ t.columns.peak

Every head-terminal height is at most the peak.

theorem Prosody.Tree.mem_toGrid_edge {h : Bool} {b : MarkedGrid Tree} {c : ℕ} (hc : c ∈ (MarkedGrid.edge h b).toGrid) : c ∈ b.toGrid ∨ c ∈ (MarkedGrid.edge h b).headHeights

An edge column is either a child column or a head height of the edge — the algebraic split that replaces the foot-internal case analysis.

theorem Prosody.Tree.col_le_two_or_head {t : Tree} (hw : IsWord t) (hr : noRec t = 0) (c : ℕ) : c ∈ t.columns → c ≤ 2 ∨ c ∈ t.headHeights

In a word every column is ≤ 2 unless it is a head-terminal height — the genuine non-recursion content, now one algebraic split (mem_toGrid_edge) plus the depth bound.

theorem Prosody.Tree.two_le_head {t : Tree} (hw : IsWord t) (hr : noRec t = 0) {h : ℕ} (hh : h ∈ t.headHeights) : 2 ≤ h

In a word the head terminal sits below ω, so its height is at least 2.

theorem Prosody.Tree.headHeights_eq_peak {t : Tree} (hw : IsWord t) (hh : t.IsHeaded) (hr : noRec t = 0) : t.headHeights = [t.columns.peak]

On a non-recursive headed word, the head terminal is the grid peak ([LP77]): metrical primary stress is the tallest column.

theorem Prosody.Tree.head_below_peak_under_recursion : ∃ (t : Tree), IsWord t ∧ t.IsHeaded ∧ t.columns.IsCulminative ∧ t.headHeights ≠ [t.columns.peak]

Under recursion the peak can desert the head terminal, even when culminative ([IM09] for recursive ω; the peak≠head-terminal consequence is a property of this model).

theorem Prosody.Tree.head_below_peak_unlayered : ∃ (t : Tree), t.IsHeaded ∧ noRec t = 0 ∧ ¬IsWord t ∧ t.headHeights ≠ [t.columns.peak]

Without Layeredness the peak can desert the head terminal too.