The high-status set of a pairing

The labels whose boundary end is the high end of its chord: the potential function of the canonical route's state relabels. On the canonical route the chain direction at every participating end equals its high-status, so the accumulated relabel set is the high-status difference of the endpoint pairings — empty exactly when the pairing returns.

noncomputable def RS.EdgeSubset.highSet {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} (κ : F.RelTransitionSystem) : Finset α

The labels whose participating boundary end is the high end of its chord.

Equations

• RS.EdgeSubset.highSet κ = Finset.image (fun (b : ↥F.boundaryFlags) => F.boundaryLabel ⋯) ({b ∈ F.boundaryFlags.attach | W.pairing ↑b ∈ F.internalFlags ∧ F.boundaryLabel ⋯ < F.boundaryLabel ⋯})

theorem RS.EdgeSubset.mem_highSet {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {i : α} : i ∈ highSet κ ↔ ∃ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), W.pairing δ ∈ F.internalFlags ∧ F.boundaryLabel ⋯ < F.boundaryLabel hδ ∧ F.boundaryLabel hδ = i

Membership in the high-status set: a label that is the high end of its chord.

theorem RS.EdgeSubset.highSet_of_samePairing {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ κ' : F.RelTransitionSystem} (h : SamePairing κ κ') : highSet κ = highSet κ'

The high-status set only sees the pairing.

theorem RS.EdgeSubset.mem_highSet_iff_lt {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {δ : W.Flag} (hδ : δ ∈ F.boundaryFlags) (hint : W.pairing δ ∈ F.internalFlags) : F.boundaryLabel hδ ∈ highSet κ ↔ F.boundaryLabel ⋯ < F.boundaryLabel hδ

Membership at a given end's label reduces to the label comparison at that end.

theorem RS.EdgeSubset.mem_highSet_repair_untouched {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) {e₁ e₂ : W.Flag} (he₁ : e₁ ∈ F.boundaryFlags) (he₂ : e₂ ∈ F.boundaryFlags) (hout : ∀ (δ : W.Flag) (hδ : δ ∈ F.boundaryFlags), δ ≠ e₁ → δ ≠ e₂ → δ ≠ κ.pathMatch e₁ he₁ → δ ≠ κ.pathMatch e₂ he₂ → (κ.repair a b c d v hsq).pathMatch δ hδ = κ.pathMatch δ hδ) {δ : W.Flag} (hδ : δ ∈ F.boundaryFlags) (hint : W.pairing δ ∈ F.internalFlags) (h1 : δ ≠ e₁) (h2 : δ ≠ e₂) (h3 : δ ≠ κ.pathMatch e₁ he₁) (h4 : δ ≠ κ.pathMatch e₂ he₂) : F.boundaryLabel hδ ∈ highSet (κ.repair a b c d v hsq) ↔ F.boundaryLabel hδ ∈ highSet κ

Untouched ends keep their status across a repair.

theorem RS.EdgeSubset.mem_highSet_repair_end {α : Type} [LinearOrder α] {W : Fragment α} {F : EdgeSubset W} {κ : F.RelTransitionSystem} {a b c d : W.Flag} {v : W.Vertex} (hsq : RepairSquare κ a b c d v) {x y : W.Flag} (hx : x ∈ F.boundaryFlags) (hy : y ∈ F.boundaryFlags) (hint : W.pairing x ∈ F.internalFlags) (hnew : (κ.repair a b c d v hsq).pathMatch x hx = y) : F.boundaryLabel hx ∈ highSet (κ.repair a b c d v hsq) ↔ F.boundaryLabel hy < F.boundaryLabel hx

The re-paired end's status is the comparison against its new partner.