The reindexing at the heart of the extraction

The master summand under a colouring flip, the fibre sum it induces, and the identification of the parameter with Definition 5's mixed partition function.

theorem RS.masterSummand_colouringOfFlip {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 ℓ) : masterSummand f P e' W (colouringOfFlip W F o ψ φ) = (-1) ^ κ.circuitCount * ∏ v : W.Vertex, ↑(F.oddSignAt o φ v) * (hRS f P e').evalOdd (F.evenColoursAt ψ v) (F.oddListAt o φ v)

The termwise value identity: the master summand of the flipped data colouring is the Definition 5 term.

theorem RS.fibreSum_eq {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) (s : Finset W.Flag) : ∑ c : { c : MixedColouring k ℓ (edgeCount W + edgeCount W) // c.IsEven } with colourFlags W ↑c = s, masterSummand f P e' W ↑c = if hc : ∀ g ∈ s, W.pairing g ∈ s then if { flags := s, pairing_mem := hc }.Eulerian then { flags := s, pairing_mem := hc }.mixedValue (hRS f P e') else 0 else 0

The fibre identity, assembled from the vanishing branches and the termwise value identity.

theorem RS.parameter_eq_mixedPartition {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (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 ℓ)) (hform : SuperVect.Hom.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ P.ω { arity := 1 } { arity := 1 }) (CategoryTheory.CategoryStruct.comp (P.ω.map (ε_ { arity := 1 } { arity := 1 })) (CategoryTheory.Functor.OplaxMonoidal.η P.ω))) (SuperVect.tensorHom e e) = stdForm k ℓ) (hcopair : (SuperVect.tensorHom e' e').comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε P.ω) (CategoryTheory.CategoryStruct.comp (P.ω.map (η_ { arity := 1 } { arity := 1 })) (CategoryTheory.Functor.OplaxMonoidal.δ P.ω { arity := 1 } { arity := 1 }))) = stdCopair k ℓ) : f.val W = mixedPartition (hRS f P e') W

The conditional master identity.