The per-vertex value

The star coordinate of a block of the flipped data colouring is the block sorting sign times the Definition 5 vertex factor's normalised form: the canonical permutation carries the block to the canonical colouring, whose star coordinate the functional hRS evaluates.

theorem RS.starCoord_block_flip_nodup {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (he'e : CategoryTheory.CategoryStruct.comp e e' = CategoryTheory.CategoryStruct.id (stdSuperPair k ℓ)) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (hnd : (F.oddListAt o φ (blockVertex W v)).Nodup) : starCoord f P e' ((ds W).get v) (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v) = ↑(sortSign (oddListOf (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v))) * (↑(sortSign (F.oddListAt o φ (blockVertex W v))) * (hRS f P e').evalOdd (F.evenColoursAt ψ (blockVertex W v)) (F.oddListAt o φ (blockVertex W v)))

The per-vertex value (duplicate-free case): the star coordinate of the block is the block sorting sign times the sign-normalised Definition 5 vertex factor.

theorem RS.starCoord_block_flip_not_nodup {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (hee' : CategoryTheory.CategoryStruct.comp e' e = CategoryTheory.CategoryStruct.id (P.ω.obj { arity := 1 })) (he'e : CategoryTheory.CategoryStruct.comp e e' = CategoryTheory.CategoryStruct.id (stdSuperPair k ℓ)) (W : ClosedFragment) (F : EdgeSubset W) {κ : F.TransitionSystem} (o : κ.Orientation) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (hnd : ¬(F.oddListAt o φ (blockVertex W v)).Nodup) : starCoord f P e' ((ds W).get v) (blockRestrict (ds W) (cSorted W (colouringOfFlip W F o ψ φ)) v) = 0

The per-vertex vanishing (repeated case): a repeated odd value kills the block's star coordinate.