The chord diagram has half as many chords as the subset has boundary flags

Each chord is the sorted pair of a boundary flag's label and its chain partner's, so the two ends of a chord give the same chord and nothing else does. The map from boundary flags to chords is therefore two to one, and the diagram's cardinality is half the boundary's.

This is what makes "the number of chords" a single notion: it is oddLabelCount / 2 read off the state, and labelChords.card read off the diagram, and they agree.

Degenerate chords never cross

A label outside the subset contributes a chord with both ends at itself. Crossing asks for a strict interleaving, so such a chord crosses nothing and counts for nothing — which is why an involution extended by the identity off a subset has the crossing count of its genuine chords alone.

The involution a subset induces on the interface labels

Chords pair up the labels a subset uses. Extending by the identity off those labels gives an involution of the whole interface, whose genuine chords are the subset's and whose fixed points are the unused labels. This is the object the restriction transports are applied to.

theorem RS.EdgeSubset.boundaryLabel_boundaryFlag {α : Type} {W : Fragment α} (F : EdgeSubset W) {i : α} (h : W.boundaryFlag i ∈ F.boundaryFlags) : F.boundaryLabel h = i

A boundary flag's label is its own index.

noncomputable def RS.EdgeSubset.chordInv {α : Type} {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (i : α) : α

The label a subset's chain carries a used label to; the identity on unused ones.

Equations

• F.chordInv κ i = if h : W.boundaryFlag i ∈ F.boundaryFlags then F.boundaryLabel ⋯ else i

theorem RS.EdgeSubset.boundaryFlag_chordInv {α : Type} {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) {i : α} (h : W.boundaryFlag i ∈ F.boundaryFlags) : W.boundaryFlag (F.chordInv κ i) = κ.pathMatch (W.boundaryFlag i) h

A used label's image is used.

theorem RS.EdgeSubset.chordInv_mem {α : Type} {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) {i : α} (h : W.boundaryFlag i ∈ F.boundaryFlags) : W.boundaryFlag (F.chordInv κ i) ∈ F.boundaryFlags

The chord partner of a participating boundary label is itself participating.

theorem RS.EdgeSubset.chordInv_invol {α : Type} {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) (i : α) : F.chordInv κ (F.chordInv κ i) = i

The induced map is an involution.

theorem RS.EdgeSubset.chordInv_ne {α : Type} {W : Fragment α} (F : EdgeSubset W) (κ : F.RelTransitionSystem) {i : α} (h : W.boundaryFlag i ∈ F.boundaryFlags) : F.chordInv κ i ≠ i

The induced map is fixed-point-free on the used labels.