The label chord diagram of a transition system

The boundary pairing of a relative transition system, recorded as a finite set of label chords (each low-to-high): the combinatorial index over which the pairing-resolved open-sector values live. SamePairing is exactly equality of chord diagrams.

noncomputable def RS.EdgeSubset.labelChords {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Finset (α × α)

The chord diagram of a system: for each participating boundary flag, the sorted pair of its label and its path match's label.

Equations

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

theorem RS.EdgeSubset.mem_labelChords {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {p : α × α} : p ∈ labelChords κ ↔ ∃ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), p = (min (F.boundaryLabel hδ) (F.boundaryLabel ⋯), max (F.boundaryLabel hδ) (F.boundaryLabel ⋯))

Membership: a pair is a chord exactly when it is the sorted label pair of some participating boundary flag.

theorem RS.EdgeSubset.samePairing_of_labelChords {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (h : labelChords κ = labelChords κ') : SamePairing κ κ'

The converse: equal chord diagrams force the same pairing. The chord of δ in κ' is the chord of δ in κ (the only κ' chord containing δ's label, by label injectivity), and the partner's label determines the partner.

structure RS.IsChordDiagram {α : Type} [LinearOrder α] (P : Finset (α × α)) : Prop

A well-formed chord diagram.

• ordered (p : α × α) : p ∈ P → p.1 < p.2

  Every chord is recorded low end first.

• disjoint (p : α × α) : p ∈ P → ∀ q ∈ P, p ≠ q → PairDisjoint p q

  Distinct chords share no end.

theorem RS.EdgeSubset.labelChords_of_allInternal {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (hall : F.allInternal) (κ : F.RelTransitionSystem) : labelChords κ = ∅

On an all-internal subset the chord diagram is empty: there are no participating boundary flags.