Vanishing branches of the fibre identity

Non-Eulerian patterns kill every master summand in their fibre: the odd-degree vertex is a block of odd parity.

theorem RS.masterSummand_vanish_of_not_eulerian {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (s : Finset W.Flag) (hclosed : ∀ g ∈ s, W.pairing g ∈ s) (hfibre : colourFlags W c = s) (hnotE : ¬{ flags := s, pairing_mem := hclosed }.Eulerian) : masterSummand f P e' W c = 0

Non-Eulerian vanishing: a colouring whose pattern is a closed non-Eulerian subset has vanishing master summand.

theorem RS.masterSummand_vanish_of_impure {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (himpure : ¬PairPure c) : masterSummand f P e' W c = 0

Impure vanishing: a colouring with a mixed-parity pair has vanishing master summand.

theorem RS.masterSummand_vanish_of_not_closed {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (s : Finset W.Flag) (hfibre : colourFlags W c = s) (hnc : ¬∀ g ∈ s, W.pairing g ∈ s) : masterSummand f P e' W c = 0

Non-closed vanishing: a colouring whose pattern is not pairing-closed has vanishing master summand.

theorem RS.colourFormEntry_inr_ne {k ℓ : ℕ} {u v : Fin (2 * ℓ)} (h : v ≠ oddPartner ℓ u) : colourFormEntry k ℓ (Sum.inr u) (Sum.inr v) = 0

The entry of a non-partner odd pair vanishes.

theorem RS.masterSummand_vanish_of_not_diagonal {k ℓ R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (hpure : PairPure c) (hnd : ¬Diagonal W c) : masterSummand f P e' W c = 0

Off-diagonal vanishing: a pure non-diagonal colouring has vanishing master summand.