Coordinates of the assembled star vector

The coordinates of the model star vector factor into star coordinates over the degree blocks: the merge coordinate product rule threaded through the sum casts and the block enumeration.

theorem RS.isEven_comp_finCongr {k ℓ n₁ n₂ : ℕ} (h : n₁ = n₂) (c : MixedColouring k ℓ n₂) : MixedColouring.IsEven (c ∘ ⇑(finCongr h)) ↔ c.IsEven

Parity is invariant under an index cast.

theorem RS.blockRestrict_cons_head {k ℓ : ℕ} (d : ℕ) (ds : List ℕ) (c : MixedColouring k ℓ (d :: ds).sum) : blockRestrict (d :: ds) c ⟨0, ⋯⟩ = MixedColouring.firstHalf (c ∘ ⇑(finCongr ⋯))

The head block is the first half through the sum cast.

theorem RS.blockRestrict_cons_tail {k ℓ : ℕ} (d : ℕ) (ds : List ℕ) (c : MixedColouring k ℓ (d :: ds).sum) (v : Fin ds.length) : blockRestrict (d :: ds) c v.succ = blockRestrict ds (MixedColouring.secondHalf (c ∘ ⇑(finCongr ⋯))) v

The tail blocks are block restrictions of the second half through the sum cast.

theorem RS.coordOf_modelStarVec {k ℓ R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (ds : List ℕ) (c : MixedColouring k ℓ ds.sum) (_hc : c.IsEven) : coordOf (modelStarVec f P e' ds) c = ∏ v : Fin ds.length, starCoord f P e' (ds.get v) (blockRestrict ds c v)

The assembled coordinates factor over the blocks.