The block alignment

Flipping the odd colouring on the edges whose representative is outgoing aligns the block values of the data colouring with the Definition 5 per-flag values: outgoing flags carry the partner of their colour, incoming flags the colour itself.

noncomputable def RS.colouringOfFlip {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) : MixedColouring k ℓ (edgeCount W + edgeCount W)

The flipped data colouring of an orientation.

Equations

• RS.colouringOfFlip W F o ψ φ = RS.colouringOf W F ψ (RS.EdgeSubset.OddColouring.flip F (RS.outRepSet W F o) ⋯ φ)

theorem RS.starFlagEnum_blockFlag (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : (starFlagEnum W) (blockFlag W v j) = slotEmbed W v j

The slot half of a block flag is the slot half of its embedded slot.

theorem RS.blockRestrict_colouringOfFlip_mem {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) (h : blockFlag W v j ∈ F.flags) : blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v j = Sum.inr (if o.isOut (blockFlag W v j) = true then oddPartner ℓ (↑φ ⟨blockFlag W v j, h⟩) else ↑φ ⟨blockFlag W v j, h⟩)

The four-case alignment: the block value of the flipped data colouring at a participating slot is the Definition 5 per-flag value of its flag.

theorem RS.blockRestrict_colouringOfFlip_not_mem {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) (h : blockFlag W v j ∉ F.flags) : blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v j = Sum.inl (↑ψ ⟨blockFlag W v j, h⟩)

Non-participating block values are unchanged by the flip.