The evaluation leaf

The base of the cap recursion: the strand evaluation on a transported two-position basis vector is the colour form entry of the two colours. Both mixed-parity colourings are excluded by evenness; the pure branches route through the one-position basis presentations and the standard-form identification.

theorem RS.stdForm_evenPair {k ℓ : ℕ} (x y : (stdSuperPair k ℓ).even) : (stdForm k ℓ).evenMap (evenPair x y) = stdFormEven k x y

The standard form on even pairs is the even form.

theorem RS.stdForm_oddPair {k ℓ : ℕ} (x y : (stdSuperPair k ℓ).odd) : (stdForm k ℓ).evenMap (oddPair x y) = stdFormOdd ℓ x y

The standard form on odd pairs is the odd form.

theorem RS.omegaFun_ev_basis {R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) {k ℓ : ℕ} (e : stdSuperPair k ℓ ⟶ 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 ℓ) (c : MixedColouring k ℓ 2) (hc : c.IsEven) : (omegaFun f P (evClass f)) ((stdToOmega f P e 2).evenMap (evenBasisVec ⟨c, hc⟩)) = colourFormEntry k ℓ (c 0) (c 1)

The evaluation leaf: the strand evaluation on a transported two-position basis vector is the colour form entry of the two colours.