The crossing-parity delta of the diagram gluing

The crossing-count parity change of a label chord diagram across the Temperley–Lieb gluing glueChords i j — the chord-sign ratio the converse's per-cut splitting carries.

• diagCrossCount — the abstract crossing count of a chord diagram: ordered pairs of chords, gated so that the first-starting chord is listed first; for a well-formed diagram each crossing unordered pair contributes exactly one element.
• diagCrossCount_glue_cross — the glue delta: gluing the cut {i, j} (chords (i,x), (j,y) concatenating into (x,y)) changes the crossing parity by the number of surviving chords crossing the cut, plus the mutual-crossing indicator of the two cut chords.

theorem RS.chordPairCross_comm {α : Type} [LinearOrder α] {x y u w : α} : ChordPairCross x y u w ↔ ChordPairCross u w x y

ChordPairCross is symmetric in its two chords: the two disjuncts swap.

noncomputable def RS.diagCrossCount {α : Type} [LinearOrder α] (P : Finset (α × α)) : ℕ

The abstract diagram crossing count: ordered pairs of chords that interleave, gated so the first-starting chord is listed first. On a well-formed diagram (IsChordDiagram) every crossing unordered pair of chords contributes exactly one ordered pair, so this is the plain crossing number.

Equations

• RS.diagCrossCount P = {pq ∈ P ×ˢ P | pq.1.1 < pq.2.1 ∧ RS.ChordPairCross pq.1.1 pq.1.2 pq.2.1 pq.2.2}.card

Order helpers

The system bridge

The glue delta, crossing case

theorem RS.diagCrossCount_glue_cross {α : Type} [LinearOrder α] {P : Finset (α × α)} (hP : IsChordDiagram P) {i j x y : α} (hij : i < j) (hxj : x ≠ j) (hi : (min i x, max i x) ∈ P) (hj : (min j y, max j y) ∈ P) : (diagCrossCount (glueChords i j P) + diagCrossCount P) % 2 = ((Finset.filter (CrossesCut i j) ((P.erase (min i x, max i x)).erase (min j y, max j y))).card + if ChordPairCross (min i x) (max i x) (min j y) (max j y) then 1 else 0) % 2

The glue delta, crossing case: gluing the cut {i, j} (i < j, chord (i,x) and chord (j,y) concatenating into (x,y), non-linked: x ≠ j) changes the diagram crossing count, mod 2, by the number of surviving third chords crossing the cut plus the mutual-crossing indicator of the two cut chords.