Non-crossing constraint for two-layer association lines

A Finset (ι × κ) of links between two ordered tiers is non-crossing when k₁ < k₂ → i₁ ≤ i₂ for any two links (k₁, i₁), (k₂, i₂) — i.e. the index coordinates monovary, which in a two-layer drawing is exactly the absence of crossing segments; equivalently (over linear tiers), the componentwise order is total on the link set, [YJ15]'s edge-order axiom. This is the discrete-index [Gol76] / [Sag86] No-Crossing Constraint ([Sag88] derives it from association-as-temporal-overlap) and the canonical filter on autosegmental GEN.

Main definitions

• IsNonCrossing links: the link set monovaries ([Preorder]-general).
• Crosses a b / IndexCrosses links p: two links cross; p crosses some link already in links — the decidable GEN filter.

Main results

• isNonCrossing_insert_iff_not_indexCrosses: a candidate may be added iff it crosses nothing (IsNonCrossing.insert_of_not_indexCrosses is the GEN direction).
• isNonCrossing_image / IsNonCrossing.image_monotone: IsNonCrossing commutes with Finset.image, and survives monotone reindexing of the upper coordinate.

Set-level non-crossing property (via mathlib MonovaryOn)

def Autosegmental.IsNonCrossing {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] (links : Finset (ι × κ)) : Prop

The link set has no crossings: its two index coordinates monovary.

Equations

• Autosegmental.IsNonCrossing links = MonovaryOn Prod.snd Prod.fst ↑links

theorem Autosegmental.isNonCrossing_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] {links : Finset (ι × κ)} : IsNonCrossing links ↔ ∀ l₁ ∈ links, ∀ l₂ ∈ links, l₁.1 < l₂.1 → l₁.2 ≤ l₂.2

IsNonCrossing in elementary form.

@[simp]

theorem Autosegmental.isNonCrossing_empty {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] : IsNonCrossing ∅

@[simp]

theorem Autosegmental.isNonCrossing_singleton {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] (p : ι × κ) : IsNonCrossing {p}

theorem Autosegmental.isNonCrossing_pair {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] (a b : ι × κ) : IsNonCrossing {a, b} ↔ (a.1 < b.1 → a.2 ≤ b.2) ∧ (b.1 < a.1 → b.2 ≤ a.2)

A pair is non-crossing iff its two links agree in tier- and backbone-order.

theorem Autosegmental.IsNonCrossing.subset {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] {s t : Finset (ι × κ)} (hst : s ⊆ t) (h : IsNonCrossing t) : IsNonCrossing s

A subset of a non-crossing link set is non-crossing.

theorem Autosegmental.isNonCrossing_insert_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] {links : Finset (ι × κ)} [DecidableEq ι] [DecidableEq κ] (p : ι × κ) : IsNonCrossing (insert p links) ↔ IsNonCrossing links ∧ ∀ q ∈ links, IsNonCrossing {p, q}

Inserting p keeps non-crossing iff p crosses no existing link: the insert-algebra form, Set.pairwise_insert specialised to IsNonCrossing via monovaryOn_insert.

@[instance_reducible]

instance Autosegmental.instDecidableIsNonCrossingOfDecidableLTOfDecidableLE {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] {links : Finset (ι × κ)} [DecidableLT ι] [DecidableLE κ] : Decidable (IsNonCrossing links)

Equations

• Autosegmental.instDecidableIsNonCrossingOfDecidableLTOfDecidableLE = decidable_of_iff (∀ l₁ ∈ links, ∀ l₂ ∈ links, l₁.1 < l₂.1 → l₁.2 ≤ l₂.2) ⋯

Reindexing along Finset.image

theorem Autosegmental.isNonCrossing_image {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} {κ' : Type u_4} [Preorder ι'] [Preorder κ'] [DecidableEq ι'] [DecidableEq κ'] {links : Finset (ι × κ)} (f : ι × κ → ι' × κ') : IsNonCrossing (Finset.image f links) ↔ MonovaryOn (Prod.snd ∘ f) (Prod.fst ∘ f) ↑links

IsNonCrossing transports across a Finset.image: the image link set is non-crossing iff the index coordinates monovary after reindexing by f. The Finset companion of monovaryOn_image, and the single place the definition is unfolded against an image.

theorem Autosegmental.IsNonCrossing.image_monotone {ι : Type u_1} {ι' : Type u_2} {κ : Type u_3} [LinearOrder ι] [Preorder ι'] [Preorder κ] [DecidableEq ι'] [DecidableEq κ] {links : Finset (ι × κ)} {ρ : ι → ι'} (hρ : Monotone ρ) (h : IsNonCrossing links) : IsNonCrossing (Finset.image (Prod.map ρ id) links)

Pushing a non-crossing link set forward along a monotone map on the upper (first) coordinate keeps it non-crossing: the autosegmental analogue of SimpleGraph.map along a monotone vertex map. The upper index needs a LinearOrder (the run-collapse domain is ℕ) so that ρ reflects <. Used to lift planarity through the OCP run-collapse ρ (Autosegmental/Collapse.lean).

Relational composition through a shared tier

Association relations compose through a shared middle tier — the Finset companion of SetRel.comp. Planarity is not closed under composition: fan-in followed by fan-out at a single middle position (an autosegment multiply-linked from above whose position multiply-links onward) composes to a crossing — see the counterexample below. It is closed when the middle tier does not fan through, in either direction: IsNonCrossing.relComp_of_injOn_fst (no fan-out) and IsNonCrossing.relComp_of_injOn_snd (no fan-in).

def Autosegmental.relComp {ι : Type u_1} {κ : Type u_3} {μ : Type u_5} [DecidableEq ι] [DecidableEq κ] [DecidableEq μ] (R : Finset (ι × κ)) (S : Finset (κ × μ)) : Finset (ι × μ)

Relational composition of link sets through a shared middle tier.

Equations

• Autosegmental.relComp R S = Finset.image (fun (p : (ι × κ) × κ × μ) => (p.1.1, p.2.2)) ({p ∈ R ×ˢ S | p.1.2 = p.2.1})

@[simp]

theorem Autosegmental.mem_relComp {ι : Type u_1} {κ : Type u_3} {μ : Type u_5} [DecidableEq ι] [DecidableEq κ] [DecidableEq μ] {R : Finset (ι × κ)} {S : Finset (κ × μ)} {p : ι × μ} : p ∈ relComp R S ↔ ∃ (j : κ), (p.1, j) ∈ R ∧ (j, p.2) ∈ S

theorem Autosegmental.relComp_assoc {ι : Type u_1} {κ : Type u_3} {μ : Type u_5} {ν : Type u_6} [DecidableEq ι] [DecidableEq κ] [DecidableEq μ] [DecidableEq ν] (R : Finset (ι × κ)) (S : Finset (κ × μ)) (T : Finset (μ × ν)) : relComp (relComp R S) T = relComp R (relComp S T)

theorem Autosegmental.IsNonCrossing.relComp_of_injOn_fst {ι : Type u_1} {κ : Type u_3} {μ : Type u_5} [DecidableEq ι] [DecidableEq κ] [DecidableEq μ] [Preorder ι] [PartialOrder κ] [Preorder μ] {R : Finset (ι × κ)} {S : Finset (κ × μ)} (hR : IsNonCrossing R) (hS : IsNonCrossing S) (h : Set.InjOn Prod.fst ↑S) : IsNonCrossing (relComp R S)

Composition preserves non-crossing when the middle tier does not fan out: S is functional on middle positions (Set.InjOn Prod.fst), so a middle tie forces equal outputs.

theorem Autosegmental.IsNonCrossing.relComp_of_injOn_snd {ι : Type u_1} {κ : Type u_3} {μ : Type u_5} [DecidableEq ι] [DecidableEq κ] [DecidableEq μ] [Preorder ι] [PartialOrder κ] [Preorder μ] {R : Finset (ι × κ)} {S : Finset (κ × μ)} (hR : IsNonCrossing R) (hS : IsNonCrossing S) (h : Set.InjOn Prod.snd ↑R) : IsNonCrossing (relComp R S)

Composition preserves non-crossing when the middle tier does not fan in: R is injective onto middle positions (Set.InjOn Prod.snd), so a middle tie contradicts the strict order on inputs.

The crossing relation and the GEN filter

def Autosegmental.Crosses {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] (a b : ι × κ) : Prop

Two links cross: as a pair they fail to be non-crossing (equivalently their endpoints straddle in opposite tier- and backbone-order — crosses_iff).

Equations

• Autosegmental.Crosses a b = ¬Autosegmental.IsNonCrossing {a, b}

def Autosegmental.IndexCrosses {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] (links : Finset (ι × κ)) (p : ι × κ) : Prop

p crosses some link already in links — the decidable GEN filter.

Equations

• Autosegmental.IndexCrosses links p = ∃ l ∈ links, Autosegmental.Crosses p l

@[instance_reducible]

instance Autosegmental.instDecidableCrossesOfDecidableLTOfDecidableLE {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {a b : ι × κ} [DecidableLT ι] [DecidableLE κ] : Decidable (Crosses a b)

Equations

• Autosegmental.instDecidableCrossesOfDecidableLTOfDecidableLE = Autosegmental.instDecidableCrossesOfDecidableLTOfDecidableLE._aux_1

@[instance_reducible]

instance Autosegmental.instDecidableIndexCrossesOfDecidableLTOfDecidableLE {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {links : Finset (ι × κ)} {p : ι × κ} [DecidableLT ι] [DecidableLE κ] : Decidable (IndexCrosses links p)

Equations

• Autosegmental.instDecidableIndexCrossesOfDecidableLTOfDecidableLE = Autosegmental.instDecidableIndexCrossesOfDecidableLTOfDecidableLE._aux_1

theorem Autosegmental.crosses_comm {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {a b : ι × κ} : Crosses a b ↔ Crosses b a

Crossing is symmetric: {a, b} is the same pair as {b, a}.

theorem Autosegmental.not_indexCrosses_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {links : Finset (ι × κ)} {p : ι × κ} : ¬IndexCrosses links p ↔ ∀ l ∈ links, IsNonCrossing {p, l}

p crosses nothing iff it is pairwise non-crossing with every existing link.

theorem Autosegmental.isNonCrossing_insert_iff_not_indexCrosses {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {links : Finset (ι × κ)} {p : ι × κ} : IsNonCrossing (insert p links) ↔ IsNonCrossing links ∧ ¬IndexCrosses links p

Adding p keeps non-crossing iff it crosses no existing link: the GEN-filter form of isNonCrossing_insert_iff.

theorem Autosegmental.IsNonCrossing.insert_of_not_indexCrosses {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {links : Finset (ι × κ)} {p : ι × κ} (hNC : IsNonCrossing links) (hNX : ¬IndexCrosses links p) : IsNonCrossing (insert p links)

GEN direction of isNonCrossing_insert_iff_not_indexCrosses.

theorem Autosegmental.crosses_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [LinearOrder κ] [DecidableEq ι] [DecidableEq κ] {a b : ι × κ} : Crosses a b ↔ a.1 < b.1 ∧ b.2 < a.2 ∨ b.1 < a.1 ∧ a.2 < b.2

Crosses in elementary order form: one link's endpoints straddle the other's in opposite order.

theorem Autosegmental.indexCrosses_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [LinearOrder κ] [DecidableEq ι] [DecidableEq κ] {links : Finset (ι × κ)} {p : ι × κ} : IndexCrosses links p ↔ ∃ l ∈ links, p.1 < l.1 ∧ l.2 < p.2 ∨ l.1 < p.1 ∧ p.2 < l.2

IndexCrosses in elementary index-ordering form.

Link shift (the concatenation offset)

The coordinate offset that places a morpheme's links past the preceding tiers under concatenation ([JH15]). Shared by the bipartite Graph and the n-tier MultiGraph, which apply it to their one / each tier-pair respectively.

def Autosegmental.shiftLink (δ₁ δ₂ : ℕ) (p : ℕ × ℕ) : ℕ × ℕ

Shift a link's two endpoints by (δ₁, δ₂).

Equations

• Autosegmental.shiftLink δ₁ δ₂ p = (p.1 + δ₁, p.2 + δ₂)

@[simp]

theorem Autosegmental.shiftLink_apply (δ₁ δ₂ : ℕ) (p : ℕ × ℕ) : shiftLink δ₁ δ₂ p = (p.1 + δ₁, p.2 + δ₂)

@[simp]

theorem Autosegmental.shiftLink_zero : shiftLink 0 0 = id

theorem Autosegmental.shiftLink_comp (a₁ a₂ b₁ b₂ : ℕ) : shiftLink a₁ a₂ ∘ shiftLink b₁ b₂ = shiftLink (a₁ + b₁) (a₂ + b₂)

theorem Autosegmental.isNonCrossing_image_shiftLink (s : Finset (ℕ × ℕ)) (δ₁ δ₂ : ℕ) : IsNonCrossing (Finset.image (shiftLink δ₁ δ₂) s) ↔ IsNonCrossing s

Shifting a link set preserves non-crossing: shiftLink is a coordinatewise order-embedding, so via isNonCrossing_image it preserves monovariance.