The per-step crossing-parity decomposition

The chord-crossing count of a boundary pairing changes, across the transposition of pathMatch_repair_swap, exactly by the mutual-crossing change of the two re-paired chords: all third-chord contributions cancel mod 2. The count is a sum of ordered-pair crossing indicators; splitting the index square by membership in the four touched ends leaves an untouched block (termwise equal), a mixed block (per-third-chord parity transfer, third_chord_reparity) and the four-end block (evaluated to the mutual-crossing indicator).

def RS.chordPairCrossSym {α : Type} [LinearOrder α] (p q : α × α) : Prop

Symmetrized crossing of two chords given by (unordered) label pairs: each chord is normalized low-to-high and the two normalized chords interleave, in either order.

Equations

• RS.chordPairCrossSym p q = (RS.ChordPairCross (min p.1 p.2) (max p.1 p.2) (min q.1 q.2) (max q.1 q.2) ∨ RS.ChordPairCross (min q.1 q.2) (max q.1 q.2) (min p.1 p.2) (max p.1 p.2))

theorem RS.chordPairCrossSym_iff {α : Type} [LinearOrder α] (p₁ p₂ q₁ q₂ : α) : chordPairCrossSym (p₁, p₂) (q₁, q₂) ↔ ChordPairCross (min p₁ p₂) (max p₁ p₂) (min q₁ q₂) (max q₁ q₂)

The symmetrization is redundant: ChordPairCross of normalized chords is itself symmetric (its two disjuncts swap).

theorem RS.EdgeSubset.chordCrossingCount_repair_parity {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hne : e₁ ≠ e₂) (hPne : κ.pathMatch e₁ he₁ ≠ e₂) (hcross : κ'.pathMatch e₁ he₁ = e₂) (hfar : κ'.pathMatch (κ.pathMatch e₁ he₁) ⋯ = κ.pathMatch e₂ he₂) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → κ'.pathMatch δ hδ = κ.pathMatch δ hδ) : (chordCrossingCount κ + chordCrossingCount κ') % 2 = ((if chordPairCrossSym (F.boundaryLabel he₁, F.boundaryLabel ⋯) (F.boundaryLabel he₂, F.boundaryLabel ⋯) then 1 else 0) + if chordPairCrossSym (F.boundaryLabel he₁, F.boundaryLabel he₂) (F.boundaryLabel ⋯, F.boundaryLabel ⋯) then 1 else 0) % 2

The per-step crossing-parity decomposition: across a pairing transposition (two ends of distinct chords re-pair, the far ends re-pair with each other, everything else is preserved), the crossing count changes mod 2 exactly by the mutual-crossing change of the two re-paired chords.