The assembled star vector

The image vector of the star-tensor class, assembled recursively through the structure maps: each vertex contributes its star vector, tensored on through μ and recast along the sum. The parameter value of a closed fragment is then the circle power times the cap functional evaluated on the sorted assembled vector — arc (b) of the extraction, complete.

noncomputable def RS.omegaStarVec {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (ds : List ℕ) : (P.ω.obj { arity := ds.sum }).even

The assembled star vector of a degree list.

Equations

• One or more equations did not get rendered due to their size.
• RS.omegaStarVec f P [] = RS.omegaVec f P (CategoryTheory.CategoryStruct.id { arity := 0 })

theorem RS.omegaVec_starTensorClass {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (ds : List ℕ) : omegaVec f P (starTensorClass f ds) = omegaStarVec f P ds

The star-tensor class assembles: its image vector is the recursively assembled star vector.

theorem RS.parameter_star_factor {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (W : ClosedFragment) : f.val W = circleVal f ^ W.circles * (omegaFun f P (bundleCapClass f (edgeCount W))) ((P.ω.map (bundleMapClass f (sortEquiv (starAssignEnum W)).symm)).evenMap (omegaStarVec f P (degList (starAssignEnum W))))

The parameter value, factored (arc (b) complete): the value of a closed fragment is the circle power times the cap functional on the sorted assembled star vector.