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.
• leftBound links m / rightBound links m / window links m: the nearest index linked on either side of an upper node m, and the interval between them.

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.
• isNonCrossing_insert_iff_mem_window: a candidate may be added iff its index lies in its node's window; IsNonCrossing.union_of_leftBound / union_of_rightBound: spreading to the nearest index on one side never crosses.

References

• [YJ15]
• [Gol76]
• [Sag86]
• [Sag88]

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.

theorem Autosegmental.isNonCrossing_union_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [Preorder κ] [DecidableEq ι] [DecidableEq κ] {s t : Finset (ι × κ)} : IsNonCrossing (s ∪ t) ↔ IsNonCrossing s ∧ IsNonCrossing t ∧ ∀ a ∈ s, ∀ b ∈ t, IsNonCrossing {a, b}

A union is non-crossing iff each part is and no link of one crosses a link of the other, the Set.pairwise_union shape.

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

Relational composition through a shared tier

Association relations compose through a shared middle tier — the Finset companion of SetRel.comp. Non-crossing 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 = { decide := !decide (Autosegmental.IsNonCrossing {a, b}), reflects_decide := ⋯ }

@[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 = { decide := decide (∃ (a : ι × κ) (_ : a ∈ links), Autosegmental.Crosses p a), reflects_decide := ⋯ }

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

Two links cross iff 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.

The window of a node

For an upper node m, leftIndices and rightIndices are the lower indices linked from nodes left and right of m. In a non-crossing set every left index lies at or before every right index, so the indices m may link to without crossing form an interval, its window, from the nearest left index leftBound to the nearest right index rightBound: isNonCrossing_insert_iff_mem_window is the GEN filter as an interval, and IsNonCrossing.union_of_leftBound / union_of_rightBound are local spreading, to the nearest linked index on one side, which never crosses.

def Autosegmental.leftIndices {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] (links : Finset (ι × κ)) (m : ι) : Finset κ

The indices linked from nodes left of m.

Equations

• Autosegmental.leftIndices links m = Finset.image (fun (x : ι × κ) => x.2) ({x ∈ links | x.1 < m})

def Autosegmental.rightIndices {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] (links : Finset (ι × κ)) (m : ι) : Finset κ

The indices linked from nodes right of m.

Equations

• Autosegmental.rightIndices links m = Finset.image (fun (x : ι × κ) => x.2) ({x ∈ links | m < x.1})

def Autosegmental.leftBound {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] (links : Finset (ι × κ)) (m : ι) : WithBot κ

The nearest index linked from a node left of m.

Equations

• Autosegmental.leftBound links m = (Autosegmental.leftIndices links m).max

def Autosegmental.rightBound {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] (links : Finset (ι × κ)) (m : ι) : WithTop κ

The nearest index linked from a node right of m.

Equations

• Autosegmental.rightBound links m = (Autosegmental.rightIndices links m).min

def Autosegmental.window {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] (links : Finset (ι × κ)) (m : ι) : Set κ

The indices m may link to without crossing.

Equations

• Autosegmental.window links m = {j : κ | Autosegmental.leftBound links m ≤ ↑j ∧ ↑j ≤ Autosegmental.rightBound links m}

@[simp]

theorem Autosegmental.mem_leftIndices {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {x : κ} : x ∈ leftIndices links m ↔ ∃ n < m, (n, x) ∈ links

@[simp]

theorem Autosegmental.mem_rightIndices {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {x : κ} : x ∈ rightIndices links m ↔ ∃ (n : ι), m < n ∧ (n, x) ∈ links

@[instance_reducible]

instance Autosegmental.instDecidablePredMemSetWindow {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} : DecidablePred fun (x : κ) => x ∈ window links m

Equations

• Autosegmental.instDecidablePredMemSetWindow j = { decide := decide (Autosegmental.leftBound links m ≤ ↑j) && decide (↑j ≤ Autosegmental.rightBound links m), reflects_decide := ⋯ }

theorem Autosegmental.mem_window_iff {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j : κ} : j ∈ window links m ↔ (∀ x ∈ leftIndices links m, x ≤ j) ∧ ∀ x ∈ rightIndices links m, j ≤ x

theorem Autosegmental.notMem_window_of_mem_leftIndices {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j x : κ} (hx : x ∈ leftIndices links m) (h : j < x) : j ∉ window links m

theorem Autosegmental.notMem_window_of_mem_rightIndices {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j x : κ} (hx : x ∈ rightIndices links m) (h : x < j) : j ∉ window links m

theorem Autosegmental.not_indexCrosses_iff_mem_window {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j : κ} [DecidableEq ι] : ¬IndexCrosses links (m, j) ↔ j ∈ window links m

The GEN filter is membership in the window.

theorem Autosegmental.isNonCrossing_insert_iff_mem_window {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j : κ} [DecidableEq ι] : IsNonCrossing (insert (m, j) links) ↔ IsNonCrossing links ∧ j ∈ window links m

theorem Autosegmental.IsNonCrossing.left_le_right {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {x y : κ} (h : IsNonCrossing links) (hx : x ∈ leftIndices links m) (hy : y ∈ rightIndices links m) : x ≤ y

In a non-crossing set the window is an interval: every index linked left of m lies at or before every index linked right of it.

theorem Autosegmental.IsNonCrossing.mem_window_of_leftBound_eq {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j : κ} (h : IsNonCrossing links) (hj : leftBound links m = ↑j) : j ∈ window links m

The nearest left index lies in the window.

theorem Autosegmental.IsNonCrossing.mem_window_of_rightBound_eq {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} {m : ι} {j : κ} (h : IsNonCrossing links) (hj : rightBound links m = ↑j) : j ∈ window links m

The nearest right index lies in the window.

theorem Autosegmental.leftIndices_mono {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} : Monotone (leftIndices links)

theorem Autosegmental.rightIndices_anti {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} : Antitone (rightIndices links)

theorem Autosegmental.leftBound_mono {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} : Monotone (leftBound links)

theorem Autosegmental.rightBound_mono {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} : Monotone (rightBound links)

theorem Autosegmental.IsNonCrossing.union_of_leftBound {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} [DecidableEq ι] (h : IsNonCrossing links) {s : Finset (ι × κ)} (hs : ∀ p ∈ s, leftBound links p.1 = ↑p.2) : IsNonCrossing (links ∪ s)

Lines from any nodes to the nearest index linked left of each cross neither one another nor the links of a non-crossing set, so local spreading to the left is safe.

theorem Autosegmental.IsNonCrossing.union_of_rightBound {ι : Type u_1} {κ : Type u_3} [Preorder ι] [DecidableLT ι] [LinearOrder κ] {links : Finset (ι × κ)} [DecidableEq ι] (h : IsNonCrossing links) {s : Finset (ι × κ)} (hs : ∀ p ∈ s, rightBound links p.1 = ↑p.2) : IsNonCrossing (links ∪ s)

Lines from any nodes to the nearest index linked right of each cross neither one another nor the links of a non-crossing set, so local spreading to the right is safe.