The block data in canonical form

The colour-data extractors evaluated at the blocks of the flipped data colouring: the even multiset is the Definition 5 even-colour multiset at the block's vertex, and the odd list carries the Definition 5 odd values.

theorem RS.oddListOf_coe_multiset {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (s : Finset (Fin d)) (hs : ∀ (j : Fin d), j ∈ s ↔ (c j).isRight = true) : ↑(oddListOf c) = Multiset.map (fun (j : ↥s) => (c ↑j).getRight ⋯) s.attach.val

The odd list of a colouring over its participating slots, for any finset enumerating them.

theorem RS.evenMultisetOf_coe {k ℓ d : ℕ} (c : MixedColouring k ℓ d) (s : Finset (Fin d)) (hs : ∀ (j : Fin d), j ∈ s ↔ (c j).isLeft = true) : evenMultisetOf c = Multiset.map (fun (j : ↥s) => (c ↑j).getLeft ⋯) s.attach.val

The even multiset of a colouring over its even slots, for any finset enumerating them.

theorem RS.blockRestrict_colouringOfFlip_isRight {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)) : (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v j).isRight = true ↔ blockFlag W v j ∈ F.flags

Participation of a flipped block slot is participation of its flag.

theorem RS.oddListOf_blockRestrict {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) : ↑(oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)) = ↑(F.oddListAt o φ (blockVertex W v))

The block odd list is the Definition 5 odd list (as multisets).

theorem RS.evenMultisetOf_blockRestrict {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) : evenMultisetOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v) = F.evenColoursAt ψ (blockVertex W v)

The block even multiset is the Definition 5 even-colour multiset.

theorem RS.oddFinsetOf_blockRestrict {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) : oddFinsetOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v) = (F.oddListAt o φ (blockVertex W v)).toFinset

The block odd finset is the Definition 5 odd set.

theorem RS.oddListOf_blockRestrict_nodup_iff {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) : (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v)).Nodup ↔ (F.oddListAt o φ (blockVertex W v)).Nodup

The block odd list is duplicate-free iff the Definition 5 odd list is.

theorem RS.starCoord_cast {k ℓ R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) {d₁ d₂ : ℕ} (h : d₁ = d₂) (c : MixedColouring k ℓ d₂) : starCoord f P e' d₁ (c ∘ ⇑(finCongr h)) = starCoord f P e' d₂ c

The cast rule for star coordinates.