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/Jardine2016a, 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 ([goldsmith-1976]) 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.
• The junction simp kit — tier words and lengths (AR.tierWord_junction_true, AR.tierLength_junction_true, …) and links (AR.link_junction) — which the builders inherit as transparent aliases; per-builder planarity (AR.isPlanar_single, …).

The junction in coordinates

The complete association as a two-tier AR (Bool-indexed: true the melody tier, false the timing tier), built by ofData; the No-Crossing keystone in the foundational path form.

@[reducible, inline]

abbrev Autosegmental.TwoTier (α β : Type u) : Bool → Type u

The two-tier alphabet: melody labels over true, timing labels over false.

Equations

• Autosegmental.TwoTier α β b = bif b then α else β

@[instance_reducible]

instance Autosegmental.instDecidableEqTwoTierTrue {α β : Type u} [DecidableEq α] : DecidableEq (TwoTier α β true)

Equations

• Autosegmental.instDecidableEqTwoTierTrue = Autosegmental.instDecidableEqTwoTierTrue._aux_1

@[instance_reducible]

instance Autosegmental.instDecidableEqTwoTierFalse {α β : Type u} [DecidableEq β] : DecidableEq (TwoTier α β false)

Equations

• Autosegmental.instDecidableEqTwoTierFalse = Autosegmental.instDecidableEqTwoTierFalse._aux_1

def Autosegmental.AR.junction {α β : Type u} (as : List α) (bs : List β) : AR Sigma.fst

Complete many-to-many association of a melody onto a slot sequence, in coordinates.

Equations

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

instance Autosegmental.instFiniteVSigmaBoolTwoTierObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesJunction {α β : Type u} (as : List α) (bs : List β) : Finite (AR.junction as bs).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_junction_true {α β : Type u} (as : List α) (bs : List β) : tierWord true = as

@[simp]

theorem Autosegmental.AR.tierWord_junction_false {α β : Type u} (as : List α) (bs : List β) : tierWord false = bs

@[simp]

theorem Autosegmental.AR.tierLength_junction_true {α β : Type u} (as : List α) (bs : List β) : (junction as bs).tierLength true = as.length

@[simp]

theorem Autosegmental.AR.tierLength_junction_false {α β : Type u} (as : List α) (bs : List β) : (junction as bs).tierLength false = bs.length

@[simp]

theorem Autosegmental.AR.link_junction {α β : Type u} (as : List α) (bs : List β) {b b' : Bool} {p q : ℕ} : (junction as bs).link b b' p q ↔ b = true ∧ b' = false ∧ p < as.length ∧ q < bs.length ∨ b = false ∧ b' = true ∧ p < bs.length ∧ q < as.length

Junction links are complete: every in-bounds melody–timing pair.

theorem Autosegmental.AR.isPlanar_junction_iff {α β : Type u} (as : List α) (bs : List β) : IsPlanar (junction as bs).obj.edges (junction as bs).obj.arcs ↔ as.length ≤ 1 ∨ bs.length ≤ 1

The No-Crossing Constraint selects the one-sided junctions: a complete association is planar iff one side has at most one node — the one-to-many spread, many-to-one contour, and degenerate cases.

The planar local configurations

@[reducible, inline]

abbrev Autosegmental.AR.single {α β : Type u} (a : α) (b : β) : AR Sigma.fst

One-to-one association.

Equations

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

@[reducible, inline]

abbrev Autosegmental.AR.bare {α β : Type u} (b : β) : AR Sigma.fst

A bare (unassociated) timing slot.

Equations

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

@[reducible, inline]

abbrev Autosegmental.AR.float {α β : Type u} (a : α) : AR Sigma.fst

A floating autosegment ([Leb73]).

Equations

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

@[reducible, inline]

abbrev Autosegmental.AR.contour {α β : Type u} (as : List α) (b : β) : AR Sigma.fst

Several melody nodes on one slot.

Equations

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

@[reducible, inline]

abbrev Autosegmental.AR.spread {α β : Type u} (a : α) (bs : List β) : AR Sigma.fst

One melody node over several slots.

Equations

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

theorem Autosegmental.AR.isPlanar_single {α β : Type u} (a : α) (b : β) : IsPlanar (single a b).obj.edges (single a b).obj.arcs

theorem Autosegmental.AR.isPlanar_bare {α β : Type u} (b : β) : IsPlanar (bare b).obj.edges (bare b).obj.arcs

theorem Autosegmental.AR.isPlanar_float {α β : Type u} (a : α) : IsPlanar (float a).obj.edges (float a).obj.arcs

theorem Autosegmental.AR.isPlanar_contour {α β : Type u} (as : List α) (b : β) : IsPlanar (contour as b).obj.edges (contour as b).obj.arcs

theorem Autosegmental.AR.isPlanar_spread {α β : Type u} (a : α) (bs : List β) : IsPlanar (spread a bs).obj.edges (spread a bs).obj.arcs

theorem Autosegmental.AR.factorEmbeds_iff_two_tier {α β : Type u} {F : AR Sigma.fst} {X : AR Sigma.fst} [Finite F.obj.V] [Finite X.obj.V] : F.FactorEmbeds X ↔ ∃ ot ≤ X.tierLength true, ∃ of ≤ X.tierLength false, F.IsFactorAt X fun (b : Bool) => bif b then ot else of

Two-tier factor embedding is a search over two bounded offsets.

def Autosegmental.dataEmbeds {α β : Type u} (wsF wsX : (b : Bool) → List (TwoTier α β b)) (LF LX : Bool → Bool → ℕ → ℕ → Prop) : Prop

The data-level factor check: wsF/LF occurs in wsX/LX at some pair of bounded offsets — list windows match and links transport shifted. The decidable face of FactorEmbeds for ofData-presented forms.

Equations

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

@[instance_reducible]

instance Autosegmental.instDecidableDataEmbedsOfDecidableEq {α β : Type u} {wsF wsX : (b : Bool) → List (TwoTier α β b)} {LF LX : Bool → Bool → ℕ → ℕ → Prop} [DecidableEq α] [DecidableEq β] [(i j : Bool) → (p q : ℕ) → Decidable (LF i j p q)] [(i j : Bool) → (p q : ℕ) → Decidable (LX i j p q)] : Decidable (dataEmbeds wsF wsX LF LX)

Equations

• Autosegmental.instDecidableDataEmbedsOfDecidableEq = id inferInstance

theorem Autosegmental.AR.factorEmbeds_ofData_iff {α β : Type u} {wsF wsX : (b : Bool) → List (TwoTier α β b)} {LF LX : Bool → Bool → ℕ → ℕ → Prop} : FactorEmbeds (ofData wsF LF) (ofData wsX LX) ↔ dataEmbeds wsF wsX LF LX

The spec: on ofData-presented two-tier forms, factor embedding is the data-level check — the bridge that turns banned-subgraph verdicts into kernel computations.

Two-tier representations from words

def Autosegmental.TwoTier.words {α β : Type u} (as : List α) (bs : List β) (b : Bool) : List (TwoTier α β b)

The tier words of a melody word and a timing word.

Equations

• Autosegmental.TwoTier.words as bs true = as
• Autosegmental.TwoTier.words as bs false = bs

@[simp]

theorem Autosegmental.TwoTier.words_true {α β : Type u} (as : List α) (bs : List β) : words as bs true = as

@[simp]

theorem Autosegmental.TwoTier.words_false {α β : Type u} (as : List α) (bs : List β) : words as bs false = bs

def Autosegmental.TwoTier.links (L : ℕ → ℕ → Prop) (i j : Bool) (p q : ℕ) : Prop

Association lines from melody position p to timing position q under L.

Equations

• Autosegmental.TwoTier.links L i j p q = (i = true ∧ j = false ∧ L p q)

@[instance_reducible]

instance Autosegmental.TwoTier.instDecidableLinksOfDecidableRelNat (L : ℕ → ℕ → Prop) [DecidableRel L] (i j : Bool) (p q : ℕ) : Decidable (links L i j p q)

Equations

• Autosegmental.TwoTier.instDecidableLinksOfDecidableRelNat L i j p q = Autosegmental.TwoTier.instDecidableLinksOfDecidableRelNat._aux_1 L i j p q

def Autosegmental.AR.ofWords {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : AR Sigma.fst

The representation of a melody as over a timing word bs, associated by L on positions: the general two-tier form, of which junction is the complete case.

Equations

• Autosegmental.AR.ofWords as bs L = Autosegmental.AR.ofData (Autosegmental.TwoTier.words as bs) (Autosegmental.TwoTier.links L)

instance Autosegmental.instFiniteVSigmaBoolTwoTierObjGraphAndIsTierOrderedArcsTierFstNoInternalAssocEdgesOfWords {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : Finite (AR.ofWords as bs L).obj.V

@[simp]

theorem Autosegmental.AR.tierWord_ofWords_true {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : tierWord true = as

@[simp]

theorem Autosegmental.AR.tierWord_ofWords_false {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : tierWord false = bs

theorem Autosegmental.AR.factorEmbeds_ofWords_iff {α β : Type u} (as as' : List α) (bs bs' : List β) (L L' : ℕ → ℕ → Prop) : (ofWords as bs L).FactorEmbeds (ofWords as' bs' L') ↔ dataEmbeds (TwoTier.words as bs) (TwoTier.words as' bs') (TwoTier.links L) (TwoTier.links L')

Embedding between representations of words is the data-level check, hence decidable.

@[instance_reducible]

instance Autosegmental.instDecidableFactorEmbedsBoolTwoTierOfWordsOfDecidableEqOfDecidableRelNat {α β : Type u} [DecidableEq α] [DecidableEq β] (as as' : List α) (bs bs' : List β) (L L' : ℕ → ℕ → Prop) [DecidableRel L] [DecidableRel L'] : Decidable ((AR.ofWords as bs L).FactorEmbeds (AR.ofWords as' bs' L'))

Equations

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

@[simp]

theorem Autosegmental.AR.tierLength_ofWords_true {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : (ofWords as bs L).tierLength true = as.length

@[simp]

theorem Autosegmental.AR.tierLength_ofWords_false {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) : (ofWords as bs L).tierLength false = bs.length

theorem Autosegmental.AR.link_ofWords {α β : Type u} (as : List α) (bs : List β) (L : ℕ → ℕ → Prop) (p q : ℕ) : (ofWords as bs L).link true false p q ↔ p < as.length ∧ q < bs.length ∧ L p q

The lines of a representation of words: in bounds, and related by L.

theorem Autosegmental.AR.not_link_ofWords_false {α β : Type u} (as : List α) (bs : List β) (i j : Bool) (p q : ℕ) : ¬(ofWords as bs fun (x x_1 : ℕ) => False).link i j p q

A representation of words with no lines.

theorem Autosegmental.AR.link_iff_of_true_false {α β : Type u} {X : AR Sigma.fst} {Y : AR Sigma.fst} [Finite X.obj.V] [Finite Y.obj.V] (h : ∀ (p q : ℕ), X.link true false p q ↔ Y.link true false p q) (i j : Bool) (p q : ℕ) : X.link i j p q ↔ Y.link i j p q

Two-tier links are determined by the melody-to-timing case.

Realizations of word primitives

The realization of a string whose primitives are representations of words has the readers of one representation of words: the tier words concatenate, and a line lives inside one symbol's primitive, at that symbol's offsets.

def Autosegmental.wordOffset {S : Type u_3} {γ : Type u_4} (f : S → List γ) (w : List S) (k : ℕ) : ℕ

The offset of the k-th symbol's word in the concatenation.

Equations

• Autosegmental.wordOffset f w k = (List.map (fun (s : S) => (f s).length) (List.take k w)).sum

theorem Autosegmental.wordOffset_add_length_le {S : Type u_3} {γ : Type u_4} (f : S → List γ) {w : List S} {k : ℕ} (hk : k < w.length) : wordOffset f w k + (f w[k]).length ≤ (List.map f w).flatten.length

def Autosegmental.blockLinks {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (w : List S) (p q : ℕ) : Prop

The lines of a concatenation of word primitives: inside one symbol's primitive, at its offsets.

Equations

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

@[instance_reducible]

instance Autosegmental.instDecidableRelNatBlockLinks {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) [(s : S) → DecidableRel (L s)] (w : List S) : DecidableRel (blockLinks as bs L w)

Equations

• Autosegmental.instDecidableRelNatBlockLinks as bs L w x✝¹ x✝ = id inferInstance

theorem Autosegmental.blockLinks_lt {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) {w : List S} {p q : ℕ} (h : blockLinks as bs L w p q) : p < (List.map as w).flatten.length ∧ q < (List.map bs w).flatten.length

theorem Autosegmental.AR.tierWord_realize_true_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) : tierWord true = (List.map as w).flatten

theorem Autosegmental.AR.tierWord_realize_false_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) : tierWord false = (List.map bs w).flatten

theorem Autosegmental.AR.tierOffset_true_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) (k : ℕ) : tierOffset g₀ true w k = wordOffset as w k

theorem Autosegmental.AR.tierOffset_false_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) (k : ℕ) : tierOffset g₀ false w k = wordOffset bs w k

theorem Autosegmental.AR.link_realize_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (w : List S) (p q : ℕ) : link (realize g₀ w) true false p q ↔ blockLinks as bs L w p q

theorem Autosegmental.AR.factorEmbeds_realize_iff_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (F : AR Sigma.fst) [Finite F.obj.V] (w : List S) : F.FactorEmbeds (realize g₀ w) ↔ F.FactorEmbeds (ofWords (List.map as w).flatten (List.map bs w).flatten (blockLinks as bs L w))

The realization of word primitives has the readers of one representation of words.

theorem Autosegmental.AR.free_realize_iff_of_eq_ofWords {α β : Type u} {S : Type u_3} (as : S → List α) (bs : S → List β) (L : S → ℕ → ℕ → Prop) (g₀ : S → AR Sigma.fst) [∀ (s : S), Finite (g₀ s).obj.V] (hg : ∀ (s : S), g₀ s = ofWords (as s) (bs s) (L s)) (B : List { F : AR Sigma.fst // Finite F.obj.V }) (w : List S) : Free (realize g₀ w) B ↔ (ofWords (List.map as w).flatten (List.map bs w).flatten (blockLinks as bs L w)).Free B

def Autosegmental.AR.surfacesWith {α β : Type u} (X : AR Sigma.fst) [Finite X.obj.V] (a : α) (j : ℕ) : Prop

A timing slot surfaces with melody label a: some a-labelled melody node links to it.

Equations

• X.surfacesWith a j = ∃ (k : ℕ), X.link true false k j ∧ (Autosegmental.AR.tierWord true)[k]? = some a