Embeddings of autosegmental graphs

Two flavours of precedence-preserving embedding between autosegmental graphs, and the relationship between them:

• Subgraph embedding (Graph.SubgraphEmbeds/Free) — a containment relation on Graph objects: "does the forbidden block F occur as a contiguous block of G at some offset?". This is [Jar17]'s connected-subgraph embedding and the basis of his banned-subgraph grammars (Ch. 5): G is well-formed w.r.t. a forbidden set {Fᵢ} exactly when no Fᵢ embeds (Free). Stays at the Graph layer, with no morphism machinery — consumers (Studies.Jardine2017) need only the object layer.

• Precedence-preserving morphisms (precPreserving/PrecAR) — an order-embedding property of AR.Homs, promoted to a wide subcategory. These are the morphisms that preserve the linear order on each tier; they are the home of phonological process functoriality (Jardine Ch. 7; Studies.LaoideKemp2026's lenition is a functor on PrecAR but not on the full AR). The morphism-axis analogue of the object-axis WellFormedAR (ObjectProperty.FullSubcategory for planarity); here the tool is MorphismProperty + WideSubcategory, with the Category inherited free from IsMultiplicative.

The two are connected but distinct: a SubgraphEmbeds block embedding (the offset translation j ↦ j + δ) is an order-embedding, so subgraph translations are canonical instances of precedence-preserving maps — but precPreserving is strictly more general (any order-embedding, not only contiguous translations), and the two serve orthogonal purposes (well-formedness vs functoriality).

Subgraph embedding (the containment relation; banned-subgraph grammars)

def Autosegmental.Graph.IsSubgraphAt {α : Type u_1} {β : Type u_2} (F G : Graph α β) (δᵤ δₗ : ℕ) : Prop

F's upper tier appears at offset δᵤ in G's upper tier, F's lower tier at offset δₗ in G's lower tier, and all of F's association lines are present in G shifted by (δᵤ, δₗ).

Equations

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

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableIsSubgraphAtOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (F G : Graph α β) (δᵤ δₗ : ℕ) : Decidable (F.IsSubgraphAt G δᵤ δₗ)

Equations

• F.instDecidableIsSubgraphAtOfDecidableEq G δᵤ δₗ = id inferInstance

def Autosegmental.Graph.SubgraphEmbeds {α : Type u_1} {β : Type u_2} (F G : Graph α β) : Prop

F subgraph-embeds into G iff some offset (δᵤ, δₗ) places F as a contiguous block inside G — [Jar17]'s connected-subgraph embedding.

Equations

• F.SubgraphEmbeds G = ∃ δᵤ ∈ Finset.range (G.upper.len + 1), ∃ δₗ ∈ Finset.range (G.lower.len + 1), F.IsSubgraphAt G δᵤ δₗ

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableSubgraphEmbedsOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (F G : Graph α β) : Decidable (F.SubgraphEmbeds G)

Equations

• F.instDecidableSubgraphEmbedsOfDecidableEq G = id inferInstance

theorem Autosegmental.Graph.SubgraphEmbeds.refl {α : Type u_1} {β : Type u_2} (G : Graph α β) : G.SubgraphEmbeds G

SubgraphEmbeds is reflexive: F is a subgraph of itself at offset (0, 0).

Monotonicity under concatenation

A subgraph that embeds in A still embeds in A concatenated with anything: the [JH15] concat only appends tier positions and index-shifts links, so an existing block-embedding survives — at the same offset on the left (concat_left, the left block is an unshifted prefix), shifted by the prepended block's tier lengths on the right (concat_right, via get?_concat_right and the shiftLink image). These are the embedding-side of realize's monoid homomorphism: the realization of a contiguous symbol window embeds in the realization of the whole string.

theorem Autosegmental.Graph.SubgraphEmbeds.concat_left {α : Type u_1} {β : Type u_2} {F A : Graph α β} (C : Graph α β) (h : F.SubgraphEmbeds A) : F.SubgraphEmbeds (A.concat C)

Left concat-monotonicity: an embedding into A survives appending C on the right, at the same offset (A's tier positions and links are an unshifted prefix of A.concat C's).

theorem Autosegmental.Graph.SubgraphEmbeds.concat_right {α : Type u_1} {β : Type u_2} {F A : Graph α β} (C : Graph α β) (h : F.SubgraphEmbeds A) : F.SubgraphEmbeds (C.concat A)

Right concat-monotonicity: an embedding into A survives prepending C on the left, shifted by C's tier lengths (A becomes the index-shifted right block of C.concat A).

def Autosegmental.Graph.Free {α : Type u_1} {β : Type u_2} (G : Graph α β) (fs : List (Graph α β)) : Prop

G is free of the forbidden block patterns fs: no F ∈ fs subgraph-embeds into G. This is [Jar17]'s forbidden-substructure well-formedness predicate — the positional analogue of G being SimpleGraph.Free of a family of patterns — letting a consumer write G.Free forbidden for the whole set rather than conjoining one ¬ SubgraphEmbeds Fᵢ G per pattern.

Equations

• G.Free fs = ∀ F ∈ fs, ¬F.SubgraphEmbeds G

@[implicit_reducible]

instance Autosegmental.Graph.instDecidableFreeOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (G : Graph α β) (fs : List (Graph α β)) : Decidable (G.Free fs)

Equations

• G.instDecidableFreeOfDecidableEq fs = id inferInstance

Link-free embedding reduces to per-tier factor occurrence

A forbidden subgraph with no association lines decouples: the two tiers impose independent contiguous-factor constraints, with no link to fix their relative offset. This is the structural fact behind the link-free fragment of the autosegmental → star-free placement (Studies.Jardine2019): a link-free forbidden grammar reads as a Boolean combination of per-tier factor constraints.

theorem Autosegmental.Graph.subgraphEmbeds_iff_infix_of_links_empty {α : Type u_1} {β : Type u_2} (F G : Graph α β) (hF : F.links = ∅) : F.SubgraphEmbeds G ↔ F.upper.toList <:+: G.upper.toList ∧ F.lower.toList <:+: G.lower.toList

For a forbidden subgraph with no association lines, embedding reduces to two independent tier-factor occurrences: F subgraph-embeds in G iff F's upper tier is a contiguous factor of G's upper tier and F's lower tier is a contiguous factor of G's lower tier. The tiers are unconstrained relative to each other precisely because there are no links to couple their offsets.

Precedence-preserving morphisms (the order-embedding wide subcategory)

def Autosegmental.precPreserving {α : Type u_1} {β : Type u_2} : CategoryTheory.MorphismProperty (AR α β)

A morphism of AR is precedence-preserving iff both tier maps are order-embeddings (strictly monotone Fin-reindexings) — it preserves the linear order on each tier. SubgraphEmbeds block translations are canonical instances; this property is more general (any order-embedding).

Equations

• Autosegmental.precPreserving f = (StrictMono f.fU.toFun ∧ StrictMono f.fL.toFun)

instance Autosegmental.instIsMultiplicativeARPrecPreserving {α : Type u_1} {β : Type u_2} : precPreserving.IsMultiplicative

theorem Autosegmental.precPreserving.reflects_zero {α : Type u_1} {β : Type u_2} {A B : AR α β} {f : A.Hom B} (hf : precPreserving f) (j : Fin A.lower.len) (h0 : ↑(f.fL.toFun j) = 0) : ↑j = 0

A precedence-preserving morphism reflects the initial position: an order-embedding sends only the slot-0 lower element to slot 0. This is the structural content of "lenition targets the word-initial position".

@[reducible, inline]

abbrev Autosegmental.PrecAR (α : Type u_3) (β : Type u_4) : Type (max u_3 u_4)

The precedence-preserving wide subcategory of AR: same objects, with morphisms restricted to order-embedding tier maps. The Category instance is inherited from WideSubcategory via precPreserving.IsMultiplicative.

Equations

• Autosegmental.PrecAR α β = CategoryTheory.WideSubcategory Autosegmental.precPreserving