The cap value in coordinates

The cap value of an even vector is the coordinate-weighted sum of the cap values of the colour basis vectors: linearity through the coordinate expansion.

theorem RS.capVal_expansion {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ P.ω.obj { arity := 1 }) (m : ℕ) (v : (superPow (stdSuperPair k ℓ) (m + m)).even) : capVal f P e m v = ∑ c : { c : MixedColouring k ℓ (m + m) // c.IsEven }, coordOf v ↑c * capVal f P e m (evenBasisVec c)

The cap value in coordinates.