Local autosegmental configurations

The named building blocks of autosegmental representations. AR.junction as bs links every melody node of as to every timing slot of bs; its planar specializations — single, bare, float, contour, spread — are the local configurations of autosegmental tonology, and concat-products of them build every representation in the current tone studies (Studies/Jardine2016Tone, Studies/Jardine2017, Studies/Jardine2019). Building through them (rather than raw structure literals) carries the in-bounds proof at arbitrary alphabets, where the studies' by decide cannot go, and gives every configuration a simp kit.

The keystone is isPlanar_junction_iff: a junction is planar iff one side has at most one node, so among complete many-to-many associations the No-Crossing Constraint ([Gol76]) admits exactly the one-to-many (spread), many-to-one (contour) and degenerate configurations. (Formaliser's synthesis: the literature treats the NCC as a filter on representations, not as a characterisation of local generators.)

concat is the coproduct, so builder products reach exactly the block-diagonal link relations; connected shared-node configurations (e.g. a spread-fed contour, H→μ₁ with L→μ₁μ₂) are planar but not products. TODO: a gluing operation dual to concat (identify a shared boundary slot) reaching them, with the completeness target every planar AR is a concat/glue expression over the builders; at that point junction becomes primary and the five kits derive from its (the SimpleGraph.completeBipartiteGraph move).

Main definitions

• AR.junction — complete many-to-many association of a melody onto a slot sequence.
• AR.single, AR.bare, AR.float, AR.contour, AR.spread — the planar local configurations: one-to-one, toneless slot, floating autosegment ([Leb73]; the tier-with-floats object is Floating.lean), several nodes on one slot, one node over several slots.

Main results

• AR.isPlanar_junction_iff — NCC-planarity of a junction: one side is at most a singleton.
• AR.linearize_junction — every slot of a junction carries the whole melody.
• Per-builder simp kits: tier projections (at the LabeledTuple level, so .len, .toList, .get? follow from the ofList kit), reduced link sets, linearization, planarity, and OCP-cleanliness.

The complete many-to-many association

def Autosegmental.AR.junction {α : Type u_1} {β : Type u_2} (as : List α) (bs : List β) : AR α β

Complete many-to-many association: melody nodes as, timing slots bs, every node linked to every slot. Planar only in the one-sided cases (isPlanar_junction_iff), which carry the linguistic names below.

Equations

• Autosegmental.AR.junction as bs = { upper := LabeledTuple.ofList as, lower := LabeledTuple.ofList bs, links := Finset.range as.length ×ˢ Finset.range bs.length, inBounds := ⋯ }

@[simp]

theorem Autosegmental.AR.junction_upper {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} : (junction as bs).upper = LabeledTuple.ofList as

@[simp]

theorem Autosegmental.AR.junction_lower {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} : (junction as bs).lower = LabeledTuple.ofList bs

theorem Autosegmental.AR.junction_links {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} : (junction as bs).links = Finset.range as.length ×ˢ Finset.range bs.length

@[simp]

theorem Autosegmental.AR.mem_links_junction {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} {p : ℕ × ℕ} : p ∈ (junction as bs).links ↔ p.1 < as.length ∧ p.2 < bs.length

theorem Autosegmental.AR.isPlanar_junction_iff {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} : (junction as bs).IsPlanar ↔ as.length ≤ 1 ∨ bs.length ≤ 1

The No-Crossing Constraint selects the one-sided junctions: a complete many-to-many association is planar iff one side has at most one node — the one-to-many spread, the many-to-one contour, and their degenerate cases. Any 2×2 junction contains the crossing pair (0,1), (1,0).

theorem Autosegmental.AR.junction_linkedLabels {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} {j : ℕ} (hj : j < bs.length) : (junction as bs).linkedLabels j = as

theorem Autosegmental.AR.linearize_junction {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} : (junction as bs).linearize = List.map (fun (b : β) => (b, as)) bs

Every slot of a junction carries the whole melody.

theorem Autosegmental.AR.isCleanAR_junction {α : Type u_1} {β : Type u_2} {as : List α} {bs : List β} [DecidableEq α] : IsCleanAR (junction as bs) ↔ OCP.IsClean as

The planar local configurations

def Autosegmental.AR.single {α : Type u_1} {β : Type u_2} (a : α) (b : β) : AR α β

One melody node linked to one timing slot.

Equations

• Autosegmental.AR.single a b = Autosegmental.AR.junction [a] [b]

def Autosegmental.AR.bare {α : Type u_1} {β : Type u_2} (b : β) : AR α β

A bare (unassociated) timing slot.

Equations

• Autosegmental.AR.bare b = Autosegmental.AR.junction [] [b]

def Autosegmental.AR.float {α : Type u_1} {β : Type u_2} (a : α) : AR α β

A floating melody node: on the tier, linked to nothing ([Leb73]).

Equations

• Autosegmental.AR.float a = Autosegmental.AR.junction [a] []

def Autosegmental.AR.contour {α : Type u_1} {β : Type u_2} (as : List α) (b : β) : AR α β

A contour: several melody nodes sharing one timing slot.

Equations

• Autosegmental.AR.contour as b = Autosegmental.AR.junction as [b]

def Autosegmental.AR.spread {α : Type u_1} {β : Type u_2} (a : α) (bs : List β) : AR α β

A spread: one melody node linked across several timing slots.

Equations

• Autosegmental.AR.spread a bs = Autosegmental.AR.junction [a] bs

Tier projections

@[simp]

theorem Autosegmental.AR.single_upper {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (single a b).upper = LabeledTuple.ofList [a]

@[simp]

theorem Autosegmental.AR.single_lower {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (single a b).lower = LabeledTuple.ofList [b]

@[simp]

theorem Autosegmental.AR.bare_upper {α : Type u_1} {β : Type u_2} {b : β} : (bare b).upper = LabeledTuple.ofList []

@[simp]

theorem Autosegmental.AR.bare_lower {α : Type u_1} {β : Type u_2} {b : β} : (bare b).lower = LabeledTuple.ofList [b]

@[simp]

theorem Autosegmental.AR.float_upper {α : Type u_1} {β : Type u_2} {a : α} : (float a).upper = LabeledTuple.ofList [a]

@[simp]

theorem Autosegmental.AR.float_lower {α : Type u_1} {β : Type u_2} {a : α} : (float a).lower = LabeledTuple.ofList []

@[simp]

theorem Autosegmental.AR.contour_upper {α : Type u_1} {β : Type u_2} {b : β} {as : List α} : (contour as b).upper = LabeledTuple.ofList as

@[simp]

theorem Autosegmental.AR.contour_lower {α : Type u_1} {β : Type u_2} {b : β} {as : List α} : (contour as b).lower = LabeledTuple.ofList [b]

@[simp]

theorem Autosegmental.AR.spread_upper {α : Type u_1} {β : Type u_2} {a : α} {bs : List β} : (spread a bs).upper = LabeledTuple.ofList [a]

@[simp]

theorem Autosegmental.AR.spread_lower {α : Type u_1} {β : Type u_2} {a : α} {bs : List β} : (spread a bs).lower = LabeledTuple.ofList bs

Link sets

@[simp]

theorem Autosegmental.AR.single_links {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (single a b).links = {(0, 0)}

@[simp]

theorem Autosegmental.AR.bare_links {α : Type u_1} {β : Type u_2} {b : β} : (bare b).links = ∅

@[simp]

theorem Autosegmental.AR.float_links {α : Type u_1} {β : Type u_2} {a : α} : (float a).links = ∅

@[simp]

theorem Autosegmental.AR.contour_links {α : Type u_1} {β : Type u_2} {b : β} {as : List α} : (contour as b).links = Finset.range as.length ×ˢ {0}

@[simp]

theorem Autosegmental.AR.spread_links {α : Type u_1} {β : Type u_2} {a : α} {bs : List β} : (spread a bs).links = {0} ×ˢ Finset.range bs.length

Linearization

@[simp]

theorem Autosegmental.AR.linearize_single {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (single a b).linearize = [(b, [a])]

@[simp]

theorem Autosegmental.AR.linearize_bare {α : Type u_1} {β : Type u_2} {b : β} : (bare b).linearize = [(b, [])]

@[simp]

theorem Autosegmental.AR.linearize_float {α : Type u_1} {β : Type u_2} {a : α} : (float a).linearize = []

@[simp]

theorem Autosegmental.AR.linearize_contour {α : Type u_1} {β : Type u_2} {b : β} {as : List α} : (contour as b).linearize = [(b, as)]

@[simp]

theorem Autosegmental.AR.linearize_spread {α : Type u_1} {β : Type u_2} {a : α} {bs : List β} : (spread a bs).linearize = List.map (fun (b : β) => (b, [a])) bs

Planarity: the builders live inside the NCC by construction

@[simp]

theorem Autosegmental.AR.isPlanar_single {α : Type u_1} {β : Type u_2} {a : α} {b : β} : (single a b).IsPlanar

@[simp]

theorem Autosegmental.AR.isPlanar_bare {α : Type u_1} {β : Type u_2} {b : β} : (bare b).IsPlanar

@[simp]

theorem Autosegmental.AR.isPlanar_float {α : Type u_1} {β : Type u_2} {a : α} : (float a).IsPlanar

@[simp]

theorem Autosegmental.AR.isPlanar_contour {α : Type u_1} {β : Type u_2} {b : β} {as : List α} : (contour as b).IsPlanar

@[simp]

theorem Autosegmental.AR.isPlanar_spread {α : Type u_1} {β : Type u_2} {a : α} {bs : List β} : (spread a bs).IsPlanar

OCP-cleanliness

@[simp]

theorem Autosegmental.AR.isCleanAR_single {α : Type u_1} {β : Type u_2} {a : α} {b : β} [DecidableEq α] : IsCleanAR (single a b)

@[simp]

theorem Autosegmental.AR.isCleanAR_bare {α : Type u_1} {β : Type u_2} {b : β} [DecidableEq α] : IsCleanAR (bare b)

@[simp]

theorem Autosegmental.AR.isCleanAR_float {α : Type u_1} {β : Type u_2} {a : α} [DecidableEq α] : IsCleanAR (float a)

@[simp]

theorem Autosegmental.AR.isCleanAR_spread {α : Type u_1} {β : Type u_2} {a : α} {bs : List β} [DecidableEq α] : IsCleanAR (spread a bs)

theorem Autosegmental.AR.isCleanAR_contour {α : Type u_1} {β : Type u_2} {b : β} {as : List α} [DecidableEq α] : IsCleanAR (contour as b) ↔ OCP.IsClean as