The pairing transposition of a non-localized repair

A non-localized repair square touches two genuinely distinct boundary chords. The repaired matching pairs one end of the first chord with one end of the second, pairs the two remaining ends with each other, and agrees with the old matching everywhere else: the boundary pairing changes by conjugation with a transposition of two ends of distinct chords. This is the algebraic heart of the holonomy programme — repair words act on boundary pairings through transposition conjugations.

theorem RS.EdgeSubset.pathMatch_repair_swap {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) (hnl : ¬SquareLocalized κ a b c d) : ∃ (e₁ : W.Flag) (e₂ : W.Flag) (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags), e₁ ≠ e₂ ∧ κ.pathMatch e₁ he₁ ≠ e₂ ∧ (κ.repair a b c d v hsq).pathMatch e₁ he₁ = e₂ ∧ (κ.repair a b c d v hsq).pathMatch (κ.pathMatch e₁ he₁) ⋯ = κ.pathMatch e₂ he₂ ∧ ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ

The pairing transposition: a non-localized repair square re-pairs one end of each of its two distinct boundary chords with one end of the other, re-pairs the two far ends with each other, and preserves every other path match — the boundary pairing changes by conjugation with a transposition.