Fermionic vanishing of star coordinates

Repeated odd colours kill the star coordinate: the adjacent-swap inversion count is the both-odd indicator, so a colouring fixed by an adjacent swap of equal odd colours equals its own negation.

theorem RS.oddInversions_adjacent {k ℓ n : ℕ} (i : ℕ) (h2 : i + 1 < n) (c : MixedColouring k ℓ n) : oddInversions (Equiv.swap ⟨i, ⋯⟩ ⟨i + 1, h2⟩) c = if (c ⟨i, ⋯⟩).isRight = true ∧ (c ⟨i + 1, h2⟩).isRight = true then 1 else 0

The adjacent swap has exactly the both-odd inversion.

theorem RS.starCoord_adjacent_repeat {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 ℓ)) {d : ℕ} (i : ℕ) (h2 : i + 1 < d) (c : MixedColouring k ℓ d) (hodd : (c ⟨i, ⋯⟩).isRight = true) (heq : c ⟨i, ⋯⟩ = c ⟨i + 1, h2⟩) : starCoord f P e' d c = 0

Adjacent equal odd colours kill the star coordinate.

theorem RS.starCoord_repeat_zero {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 ℓ)) {d : ℕ} (c : MixedColouring k ℓ d) (i j : Fin d) (hij : ↑i < ↑j) (hodd : (c i).isRight = true) (heq : c i = c j) : starCoord f P e' d c = 0

Repeated odd colours kill the star coordinate.