The master colour sum

The parameter value as a pure colour-combinatorial sum: the cap expansion through the closed form, the permutation and cast transports, and the star-vector coordinates.

theorem RS.parameter_colour_sum {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 })) (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 ℓ) : f.val W = circleVal f ^ W.circles * ∑ c : { c : MixedColouring k ℓ (edgeCount W + edgeCount W) // c.IsEven }, ((-1) ^ oddInversions (sortSplitPerm W) (↑c ∘ ⇑(finCongr ⋯)) * ∏ v : Fin (degList (starAssignEnum W)).length, starCoord f P e' ((degList (starAssignEnum W)).get v) (blockRestrict (degList (starAssignEnum W)) ((↑c ∘ ⇑(finCongr ⋯)) ∘ ⇑(sortSplitPerm W)) v)) * betaDiag (edgeCount W) ↑c

The master colour sum: the parameter value is the circle factor times the colour sum of the transported star coordinates against the diagonal cap pairing.