Lexical melodies: per-morpheme autosegmental contributions

A melody is one morpheme's underlying autosegmental contribution ([Rol18] §2.1): tier elements and backbone slots sponsored by the same morpheme ([Wol07]), plus lexical pre-linking ([Pul86]) in melody-local coordinates. Pre-linking is per-analysis data — no links is [McCMS12]'s universally-unlinked underlying form, partial linking is [McPL26]'s stratal /M^H/ — and [Rol18] Table 1's valued, unvalued, and floating are the substrate's Graph.IsLinkedLower, IsFloatingLower, and IsFloatingUpper. A word is the Graph.concat fold of its melodies ([JH15] §5) — the Generalized Nonlinear Affixation program ([BO12]'s term, [BS12]'s programmatic statement; survey: [Zim24]).

Main definitions

• Graph.melody — one morpheme's tones, slots, and pre-links.
• FloatingForm.ofGraph — an underlying graph as a derivation input.
• FloatingForm.gen_preserves_morphemes — GEN respects Consistency of Exponence: every candidate keeps its input's sponsors.

def Autosegmental.Graph.melody {S : Type u_1} {T : Type u_2} (m : Morpheme) (tones : List T) (tbus : List S) (links : Finset Link) : Graph (TierSpec T) (SegSpec S)

One morpheme's underlying autosegmental contribution ([Rol18] §2.1 Def 1): tones over tbus, every element sponsored by m, pre-linked by links in melody-local coordinates.

Equations

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

@[simp]

theorem Autosegmental.Graph.melody_upper {S : Type u_1} {T : Type u_2} (m : Morpheme) (tones : List T) (tbus : List S) (links : Finset Link) : (melody m tones tbus links).upper = LabeledTuple.ofList (List.map (fun (t : T) => { value := t, morpheme := m }) tones)

@[simp]

theorem Autosegmental.Graph.melody_lower {S : Type u_1} {T : Type u_2} (m : Morpheme) (tones : List T) (tbus : List S) (links : Finset Link) : (melody m tones tbus links).lower = LabeledTuple.ofList (List.map (fun (s : S) => { seg := s, morpheme := m }) tbus)

@[simp]

theorem Autosegmental.Graph.melody_links {S : Type u_1} {T : Type u_2} (m : Morpheme) (tones : List T) (tbus : List S) (links : Finset Link) : (melody m tones tbus links).links = links

theorem Autosegmental.Graph.melody_upper_morpheme {S : Type u_1} {T : Type u_2} (m : Morpheme) (tones : List T) (tbus : List S) (links : Finset Link) {k : ℕ} (hk : k < tones.length) : Option.map TierSpec.morpheme ((melody m tones tbus links).upper.get? k) = some m

Every tier element of a melody is sponsored by its morpheme.

theorem Autosegmental.Graph.melody_lower_morpheme {S : Type u_1} {T : Type u_2} (m : Morpheme) (tones : List T) (tbus : List S) (links : Finset Link) {j : ℕ} (hj : j < tbus.length) : Option.map SegSpec.morpheme ((melody m tones tbus links).lower.get? j) = some m

Every backbone slot of a melody is sponsored by its morpheme.

def Autosegmental.FloatingForm.ofGraph {S : Type u_1} {T : Type u_2} (g : Graph (TierSpec T) (SegSpec S)) : FloatingForm S T

Package an underlying graph as a derivation input: nothing deleted, surface links mirror the underlying links.

Equations

• Autosegmental.FloatingForm.ofGraph g = { toGraph := g, deletedTier := ∅, surfaceLinks := g.links }

theorem Autosegmental.FloatingForm.mkInput_eq_ofGraph {S : Type u_1} {T : Type u_2} (lower : List (SegSpec S)) (upper : List (TierSpec T)) (links : Finset Link) : mkInput lower upper links = ofGraph { upper := LabeledTuple.ofList upper, lower := LabeledTuple.ofList lower, links := links }

mkInput is ofGraph of the corresponding raw graph.

theorem Autosegmental.FloatingForm.gen_preserves_morphemes {S : Type u_1} {T : Type u_2} [DecidableEq S] [DecidableEq T] (f g : FloatingForm S T) : g ∈ f.gen → g.upperMorpheme? = f.upperMorpheme? ∧ g.lowerMorpheme? = f.lowerMorpheme?

Consistency of Exponence ([Zim24] §4): GEN never alters morphemic affiliation — every one-step candidate carries its input's sponsors on both tiers.