Block parity dictionary

The parity bridge between vertex blocks of the sorted colouring and flag-degrees of the colouring's pattern: the v-th block of the sorted colouring is even iff the pattern-flags at the corresponding vertex have even count. Corollary: the master summand vanishes whenever any block is odd-parity.

noncomputable def RS.blockVertex (W : ClosedFragment) (v : Fin (degList (starAssignEnum W)).length) : W.Vertex

The vertex corresponding to the v-th block of the sorted colouring: applying the vertex enumeration to the block index.

Equations

• RS.blockVertex W v = (Fintype.equivFin W.Vertex).symm ((finCongr ⋯) v)

@[reducible, inline]

noncomputable abbrev RS.ds (W : ClosedFragment) : List ℕ

The degree list of the star assignment: one entry per vertex, recording how many slots it carries.

Equations

• RS.ds W = RS.degList (RS.starAssignEnum W)

@[reducible, inline]

noncomputable abbrev RS.cSorted {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) : MixedColouring k ℓ (ds W).sum

A colouring read in block order: slot j of block v gets the colour the original colouring gave that vertex's jth flag.

Equations

• RS.cSorted W c = (c ∘ ⇑(finCongr ⋯)) ∘ ⇑(RS.sortSplitPerm W)

noncomputable def RS.slotEmbed (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : Fin (edgeCount W + edgeCount W)

The slot a block position occupies in the unsorted colouring.

Equations

• RS.slotEmbed W v j = (RS.sortEquiv (RS.starAssignEnum W)).symm ((RS.blockSigmaEquiv (RS.ds W)) ⟨v, j⟩)

theorem RS.blockRestrict_val {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : blockRestrict (ds W) (cSorted W c) v j = c (slotEmbed W v j)

The sorted colouring at a block position equals the original colouring at the unsorted slot.

theorem RS.assign_slotEmbed (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : starAssignEnum W (slotEmbed W v j) = (finCongr ⋯) v

The assignment at an embedded slot equals the block index (up to finCongr).

theorem RS.vertexOf_slotEmbed (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : W.vertexOf ((starFlagEnum W).symm (slotEmbed W v j)) = blockVertex W v

The vertex at an embedded slot is the block's vertex.

theorem RS.slotEmbed_injective (W : ClosedFragment) (v : Fin (ds W).length) : Function.Injective (slotEmbed W v)

The slot embedding is injective in its block-offset argument.

theorem RS.slotEmbed_recover (W : ClosedFragment) (v : Fin (ds W).length) (s : Fin (edgeCount W + edgeCount W)) (jw : Fin ((ds W).get v)) (hq : ⟨v, jw⟩ = (sortSigma (starAssignEnum W)) s) : slotEmbed W v jw = s

The slot embedding recovers the original slot from the sigma decomposition.

theorem RS.blockRestrict_oddSet_card {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (v : Fin (ds W).length) : (blockRestrict (ds W) (cSorted W c) v).oddSet.card = {g ∈ colourFlags W c | W.vertexOf g = blockVertex W v}.card

Block parity: the v-th block of the sorted colouring has the same odd-set cardinality as the pattern-flags at the corresponding vertex.

theorem RS.blockRestrict_parity {k ℓ : ℕ} (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (v : Fin (ds W).length) : (blockRestrict (ds W) (cSorted W c) v).IsEven ↔ Even {g ∈ colourFlags W c | W.vertexOf g = blockVertex W v}.card

Block parity dictionary: the v-th block of the sorted colouring is even iff the pattern-flags at the corresponding vertex have even count.

theorem RS.masterSummand_vanish_of_block_odd {k ℓ R : ℕ} (f : EdgeRankParameter R) (P : DelignePackage (SkeinObj f)) (e' : P.ω.obj { arity := 1 } ⟶ stdSuperPair k ℓ) (W : ClosedFragment) (c : MixedColouring k ℓ (edgeCount W + edgeCount W)) (v : Fin (degList (starAssignEnum W)).length) (hodd : ¬(blockRestrict (degList (starAssignEnum W)) ((c ∘ ⇑(finCongr ⋯)) ∘ ⇑(sortSplitPerm W)) v).IsEven) : masterSummand f P e' W c = 0

Master summand vanishing: if any block of the sorted colouring is odd-parity, the master summand is zero, since the star coordinate vanishes on odd-parity colourings and the product absorbs the zero.