The elementary re-pairing move on relative transition systems

For a fixed edge subset F : EdgeSubset W, this file introduces the elementary 2-opt move on boundary-relative transition systems and proves that the moves connect any two systems.

Main definitions

• EdgeSubset.repairFun — the raw re-pairing of a matching function at four flags: a ↦ c, c ↦ a, b ↦ d, d ↦ b.
• EdgeSubset.RepairSquare — the admissibility data for a move: four pairwise distinct internal flags at a common vertex with a ↔ b and c ↔ d matched.
• EdgeSubset.RelTransitionSystem.repair — the elementary move, producing a transition system over the same F (so the edge subset, its internalFlags, and its boundaryFlags are untouched by construction).
• EdgeSubset.RelTransitionSystem.MatchEq — matching equality on internal flags; two systems whose matchings agree on F.internalFlags are indistinguishable to every field of RelTransitionSystem, so connectivity is stated up to MatchEq.
• EdgeSubset.IsRepairStep — one elementary move (up to MatchEq).
• EdgeSubset.disagreeSet — the internal flags where two systems' matchings differ.

Main results

• EdgeSubset.repair_connectivity — connectivity: any two relative transition systems on F are joined by a finite chain of elementary moves, with MatchEq at the endpoints. The proof is by induction on (disagreeSet κ κ').card: a disagreement at a yields an admissible square (repairSquare_of_disagree) whose repair strictly shrinks the disagreement set (disagreeSet_repair_subset).
• EdgeSubset.IsRepairStep.symm — the move is reversible, so chains can be traversed backwards.
• EdgeSubset.RelTransitionSystem.Orientation.ofMatchEq and …Orientation.transportRepair — orientation transport across MatchEq and (conditionally) across a move.

Orientation transport along a matching equality

Orientation.transportRepair transports an orientation across a repair when it already separates a from c (o.isOut c = !o.isOut a): the directions carry over unchanged. When instead o.isOut c = o.isOut a the transported orientation must flip isOut along the walk-orbit segment through c, which needs the orbit machinery; that construction is Orientation.segFlip in NonSeparatedStep.lean, with Orientation.flipOrbit of PathLedger.lean for a periodic segment.

The raw re-pairing function

def RS.EdgeSubset.repairFun {α : Type} {W : Fragment α} (m : W.Flag → W.Flag) (a b c d : W.Flag) : W.Flag → W.Flag

Re-pair a matching function at four flags: a ↦ c, c ↦ a, b ↦ d, d ↦ b, leaving every other flag to m.

Equations

• RS.EdgeSubset.repairFun m a b c d f = if f = a then c else if f = c then a else if f = b then d else if f = d then b else m f

theorem RS.EdgeSubset.repairFun_a {α : Type} {W : Fragment α} {m : W.Flag → W.Flag} {a b c d : W.Flag} : repairFun m a b c d a = c

The re-pairing sends a to c.

theorem RS.EdgeSubset.repairFun_c {α : Type} {W : Fragment α} {m : W.Flag → W.Flag} {a b c d : W.Flag} (h : c ≠ a) : repairFun m a b c d c = a

And c back to a.

theorem RS.EdgeSubset.repairFun_b {α : Type} {W : Fragment α} {m : W.Flag → W.Flag} {a b c d : W.Flag} (h1 : b ≠ a) (h2 : b ≠ c) : repairFun m a b c d b = d

It sends b to d.

theorem RS.EdgeSubset.repairFun_d {α : Type} {W : Fragment α} {m : W.Flag → W.Flag} {a b c d : W.Flag} (h1 : d ≠ a) (h2 : d ≠ c) (h3 : d ≠ b) : repairFun m a b c d d = b

And d back to b.

theorem RS.EdgeSubset.repairFun_of_ne {α : Type} {W : Fragment α} {m : W.Flag → W.Flag} {a b c d f : W.Flag} (h1 : f ≠ a) (h2 : f ≠ b) (h3 : f ≠ c) (h4 : f ≠ d) : repairFun m a b c d f = m f

Away from the four flags the matching is untouched: the move is local.

theorem RS.EdgeSubset.repairFun_congr {α : Type} {W : Fragment α} {m m' : W.Flag → W.Flag} {a b c d f : W.Flag} (hm : m f = m' f) : repairFun m a b c d f = repairFun m' a b c d f

The re-paired function depends on the underlying matching only through its value at the argument.

Admissibility data for a move

structure RS.EdgeSubset.RepairSquare {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (a b c d : W.Flag) (v : W.Vertex) : Prop

The data of an admissible 2-opt re-pairing move on κ : F.RelTransitionSystem: four pairwise distinct internal flags a, b, c, d attached to a common vertex v, with a ↔ b and c ↔ d matched by κ. (The distinctness facts a ≠ b and c ≠ d are derivable from match_ne and are not recorded.)

• ha : a ∈ F.internalFlags
• hc : c ∈ F.internalFlags
• hab : κ.match_ a = b
• hcd : κ.match_ c = d
• hac : a ≠ c
• had : a ≠ d
• hbc : b ≠ c
• hbd : b ≠ d
• hav : W.attach a = Sum.inl v
• hcv : W.attach c = Sum.inl v

theorem RS.EdgeSubset.RepairSquare.hb {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : b ∈ F.internalFlags

b is internal.

theorem RS.EdgeSubset.RepairSquare.hd {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : d ∈ F.internalFlags

d is internal.

theorem RS.EdgeSubset.RepairSquare.hba {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : b ≠ a

b ≠ a.

theorem RS.EdgeSubset.RepairSquare.hdc {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : d ≠ c

d ≠ c.

theorem RS.EdgeSubset.RepairSquare.hmb {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : κ.match_ b = a

κ matches b back to a.

theorem RS.EdgeSubset.RepairSquare.hmd {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : κ.match_ d = c

κ matches d back to c.

theorem RS.EdgeSubset.RepairSquare.hbv {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : W.attach b = Sum.inl v

b sits at the common vertex.

theorem RS.EdgeSubset.RepairSquare.hdv {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : W.attach d = Sum.inl v

d sits at the common vertex.

theorem RS.EdgeSubset.RepairSquare.match_ne_four {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) {f : W.Flag} (hf : f ∈ F.internalFlags) (h1 : f ≠ a) (h2 : f ≠ b) (h3 : f ≠ c) (h4 : f ≠ d) : κ.match_ f ≠ a ∧ κ.match_ f ≠ b ∧ κ.match_ f ≠ c ∧ κ.match_ f ≠ d

The κ-partner of a flag off the square stays off the square.

The elementary move

def RS.EdgeSubset.RelTransitionSystem.repair {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) (a b c d : W.Flag) (v : W.Vertex) (h : RepairSquare κ a b c d v) : F.RelTransitionSystem

The elementary move (2-opt re-pairing): given an admissible square (a ↔ b, c ↔ d matched, all four distinct, all at vertex v), the transition system matching a ↔ c and b ↔ d instead, keeping every other matched pair. The result is a system over the same edge subset F.

Equations

• κ.repair a b c d v h = { match_ := RS.EdgeSubset.repairFun κ.match_ a b c d, match_invol := ⋯, match_ne := ⋯, match_mem := ⋯, match_vertex := ⋯ }

@[simp]

theorem RS.EdgeSubset.RelTransitionSystem.repair_match_a {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : (κ.repair a b c d v h).match_ a = c

The repaired system's matching at a.

@[simp]

theorem RS.EdgeSubset.RelTransitionSystem.repair_match_c {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : (κ.repair a b c d v h).match_ c = a

At c.

@[simp]

theorem RS.EdgeSubset.RelTransitionSystem.repair_match_b {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : (κ.repair a b c d v h).match_ b = d

At b.

@[simp]

theorem RS.EdgeSubset.RelTransitionSystem.repair_match_d {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : (κ.repair a b c d v h).match_ d = b

At d.

theorem RS.EdgeSubset.RelTransitionSystem.repair_match_of_ne {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d f : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) (h1 : f ≠ a) (h2 : f ≠ b) (h3 : f ≠ c) (h4 : f ≠ d) : (κ.repair a b c d v h).match_ f = κ.match_ f

And everywhere else, unchanged.

Matching equality

def RS.EdgeSubset.RelTransitionSystem.MatchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ₁ κ₂ : F.RelTransitionSystem) : Prop

Two relative transition systems agree when their matchings agree on the internal flags. All fields of RelTransitionSystem constrain only internal flags, so MatchEq-related systems are interchangeable; the matching's values off F.internalFlags are junk.

Equations

• κ₁.MatchEq κ₂ = ∀ f ∈ F.internalFlags, κ₁.match_ f = κ₂.match_ f

theorem RS.EdgeSubset.RelTransitionSystem.MatchEq.refl {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : κ.MatchEq κ

Matching equality is reflexive.

theorem RS.EdgeSubset.RelTransitionSystem.MatchEq.symm {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (h : κ₁.MatchEq κ₂) : κ₂.MatchEq κ₁

It is symmetric.

theorem RS.EdgeSubset.RelTransitionSystem.MatchEq.trans {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ κ₃ : F.RelTransitionSystem} (h : κ₁.MatchEq κ₂) (h' : κ₂.MatchEq κ₃) : κ₁.MatchEq κ₃

It is transitive — an equivalence, so chains compose up to it.

Transport of squares and moves

theorem RS.EdgeSubset.RepairSquare.of_matchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (heq : κ.MatchEq κ') (h : RepairSquare κ a b c d v) : RepairSquare κ' a b c d v

A repair square transports across matching equality.

theorem RS.EdgeSubset.RelTransitionSystem.repair_congr {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (heq : κ.MatchEq κ') (h : RepairSquare κ a b c d v) (h' : RepairSquare κ' a b c d v) : (κ.repair a b c d v h).MatchEq (κ'.repair a b c d v h')

Repairing MatchEq-equal systems along the same square yields MatchEq-equal systems.

theorem RS.EdgeSubset.RelTransitionSystem.repair_repair {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) (h₂ : RepairSquare (κ.repair a b c d v h) a c b d v) : ((κ.repair a b c d v h).repair a c b d v h₂).MatchEq κ

The move is an involution: repairing back along the inverse square recovers the original matching on internal flags.

theorem RS.EdgeSubset.RepairSquare.symm {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) : RepairSquare (κ.repair a b c d v h) a c b d v

The inverse square: after the move, (a, c, b, d) is again admissible (the move a ↔ c, b ↔ d back to a ↔ b, c ↔ d).

The elementary step relation

def RS.EdgeSubset.IsRepairStep {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ₁ κ₂ : F.RelTransitionSystem) : Prop

One elementary move joins κ₁ to κ₂: some admissible square of κ₁ repairs it to a system matching-equal to κ₂.

Equations

• RS.EdgeSubset.IsRepairStep κ₁ κ₂ = ∃ (a : W.Flag) (b : W.Flag) (c : W.Flag) (d : W.Flag) (v : W.Vertex) (h : RS.EdgeSubset.RepairSquare κ₁ a b c d v), (κ₁.repair a b c d v h).MatchEq κ₂

theorem RS.EdgeSubset.IsRepairStep.congr {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₁' κ₂ κ₂' : F.RelTransitionSystem} (h1 : κ₁.MatchEq κ₁') (h2 : κ₂.MatchEq κ₂') (hstep : IsRepairStep κ₁ κ₂) : IsRepairStep κ₁' κ₂'

The step relation respects matching equality on both sides.

theorem RS.EdgeSubset.IsRepairStep.symm {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ₁ κ₂ : F.RelTransitionSystem} (hstep : IsRepairStep κ₁ κ₂) : IsRepairStep κ₂ κ₁

The step relation is symmetric: every move can be undone by a move, so chains of moves can be reversed.

The disagreement set

noncomputable def RS.EdgeSubset.disagreeSet {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ κ' : F.RelTransitionSystem) : Finset W.Flag

The internal flags at which two transition systems' matchings disagree.

Equations

• RS.EdgeSubset.disagreeSet κ κ' = {f ∈ F.internalFlags | κ.match_ f ≠ κ'.match_ f}

theorem RS.EdgeSubset.mem_disagreeSet {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {f : W.Flag} : f ∈ disagreeSet κ κ' ↔ f ∈ F.internalFlags ∧ κ.match_ f ≠ κ'.match_ f

Membership in the disagreement set: an internal flag the two matchings send to different places.

theorem RS.EdgeSubset.disagreeSet_eq_empty_iff {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} : disagreeSet κ κ' = ∅ ↔ κ.MatchEq κ'

The disagreement set is empty exactly for matching-equal systems.

theorem RS.EdgeSubset.repairSquare_of_disagree {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {a : W.Flag} (ha : a ∈ F.internalFlags) (hdis : κ.match_ a ≠ κ'.match_ a) {v : W.Vertex} (hav : W.attach a = Sum.inl v) : RepairSquare κ a (κ.match_ a) (κ'.match_ a) (κ.match_ (κ'.match_ a)) v

A disagreement at a yields an admissible square: with b := κ.match_ a, c := κ'.match_ a, d := κ.match_ c, the four flags are pairwise distinct internal flags at a's vertex.

theorem RS.EdgeSubset.disagreeSet_repair_subset {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) (hc' : κ'.match_ a = c) : disagreeSet (κ.repair a b c d v h) κ' ⊆ (disagreeSet κ κ').erase a

Disagreement decrease: repairing the square of a disagreement at a (with c = κ'.match_ a) removes both a and c from the disagreement set and adds nothing; in particular the new disagreement set avoids a.

Connectivity

theorem RS.EdgeSubset.repair_connectivity_of_card_le {α : Type} {W : Fragment α} {F : EdgeSubset W} (N : ℕ) (κ κ' : F.RelTransitionSystem) : (disagreeSet κ κ').card ≤ N → ∃ (n : ℕ) (chain : Fin (n + 1) → F.RelTransitionSystem), (chain 0).MatchEq κ ∧ (chain (Fin.last n)).MatchEq κ' ∧ ∀ (r : Fin n), IsRepairStep (chain r.castSucc) (chain r.succ)

Connectivity, with an explicit bound on the disagreement count: strong induction on (disagreeSet κ κ').card.

theorem RS.EdgeSubset.repair_connectivity {α : Type} {W : Fragment α} {F : EdgeSubset W} (κ κ' : F.RelTransitionSystem) : ∃ (n : ℕ) (chain : Fin (n + 1) → F.RelTransitionSystem), (chain 0).MatchEq κ ∧ (chain (Fin.last n)).MatchEq κ' ∧ ∀ (r : Fin n), IsRepairStep (chain r.castSucc) (chain r.succ)

Connectivity of the elementary move: any two boundary-relative transition systems on the same edge subset are joined by a finite chain of elementary re-pairing moves, matching-equal to the given systems at the endpoints.

Orientation transport

def RS.EdgeSubset.RelTransitionSystem.Orientation.ofMatchEq {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (heq : κ.MatchEq κ') (o : κ.Orientation) : κ'.Orientation

Orientations transport across matching equality: an orientation constrains isOut only through the matching's values on internal flags.

Equations

• RS.EdgeSubset.RelTransitionSystem.Orientation.ofMatchEq heq o = { isOut := o.isOut, match_flip := ⋯, pairing_flip := ⋯ }

def RS.EdgeSubset.RelTransitionSystem.Orientation.transportRepair {α : Type} {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (h : RepairSquare κ a b c d v) (o : κ.Orientation) (hflip : o.isOut c = !o.isOut a) : (κ.repair a b c d v h).Orientation

Orientation transport along a move (separated case): when the orientation already separates a and c (isOut c = !isOut a), it transports unchanged along the repair. When instead isOut c = isOut a the transported orientation must flip isOut along a walk segment; that is Orientation.segFlip.

Equations

• RS.EdgeSubset.RelTransitionSystem.Orientation.transportRepair h o hflip = { isOut := o.isOut, match_flip := ⋯, pairing_flip := ⋯ }