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. This is the discrete-index [Gol76] / [Sag86] No-Crossing Constraint 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.

@[implicit_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).

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

@[implicit_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

@[implicit_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.