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 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 β

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

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

def 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]

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

A bare (unassociated) timing slot.

Equations

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

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

A floating autosegment ([Leb73]).

Equations

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

def 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]

def 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.

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