Block data of the data colouring

The flags of the v-th block enumerate the fragment's flags at the block's vertex, and the block values of the data colouring are the colouring data at those flags: participating flags carry the odd colour (or its partner on partner slots), the rest the even colour.

noncomputable def RS.blockFlag (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : W.Flag

The flag of the j-th slot in the v-th block.

Equations

• RS.blockFlag W v j = (RS.starFlagEnum W).symm (RS.slotEmbed W v j)

theorem RS.vertexOf_blockFlag (W : ClosedFragment) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : W.vertexOf (blockFlag W v j) = blockVertex W v

Block flags sit at the block's vertex.

theorem RS.blockFlag_injective (W : ClosedFragment) (v : Fin (ds W).length) : Function.Injective (blockFlag W v)

The block-flag enumeration is injective.

theorem RS.image_blockFlag (W : ClosedFragment) (v : Fin (ds W).length) : Finset.image (blockFlag W v) Finset.univ = {g : W.Flag | W.vertexOf g = blockVertex W v}

Block flags enumerate the vertex's flags: the image of the block-flag enumeration is the set of flags at the block's vertex.

theorem RS.blockRestrict_colouringOf {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : blockRestrict (ds W) (cSorted W (colouringOf W F ψ φ)) v j = if h : blockFlag W v j ∈ F.flags then Sum.inr (if ↑(slotEmbed W v j) < edgeCount W then ↑φ ⟨blockFlag W v j, h⟩ else oddPartner ℓ (↑φ ⟨blockFlag W v j, h⟩)) else Sum.inl (↑ψ ⟨blockFlag W v j, h⟩)

The block value of the data colouring: the colouring data at the block flag, with the odd partner on partner slots.

theorem RS.blockRestrict_colouringOf_not_mem {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) (h : blockFlag W v j ∉ F.flags) : blockRestrict (ds W) (cSorted W (colouringOf W F ψ φ)) v j = Sum.inl (↑ψ ⟨blockFlag W v j, h⟩)

Non-participating block flags carry the even colour.

theorem RS.blockRestrict_colouringOf_mem {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) (h : blockFlag W v j ∈ F.flags) : blockRestrict (ds W) (cSorted W (colouringOf W F ψ φ)) v j = Sum.inr (if ↑(slotEmbed W v j) < edgeCount W then ↑φ ⟨blockFlag W v j, h⟩ else oddPartner ℓ (↑φ ⟨blockFlag W v j, h⟩))

Participating block flags carry the odd colour or its partner.

noncomputable def RS.evenSlots (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) : Finset (Fin ((ds W).get v))

The non-participating slots of a block.

Equations

• RS.evenSlots W F v = {j : Fin ((RS.ds W).get v) | RS.blockFlag W v j ∉ F.flags}

theorem RS.mem_evenSlots {W : ClosedFragment} {F : EdgeSubset W} {v : Fin (ds W).length} (j : Fin ((ds W).get v)) : j ∈ evenSlots W F v ↔ blockFlag W v j ∉ F.flags

Membership in the non-participating slots.

theorem RS.blockSlot_not_mem {W : ClosedFragment} {F : EdgeSubset W} {v : Fin (ds W).length} (j : ↥(evenSlots W F v)) : blockFlag W v ↑j ∉ F.flags

The defining property of a non-participating block slot.

theorem RS.evenColoursAt_blockVertex {k : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (v : Fin (ds W).length) : F.evenColoursAt ψ (blockVertex W v) = Multiset.map (fun (j : ↥(evenSlots W F v)) => ↑ψ ⟨blockFlag W v ↑j, ⋯⟩) (evenSlots W F v).attach.val

The even colours at a block's vertex are the even data at the non-participating block slots.

noncomputable def RS.oddSlots (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) : Finset (Fin ((ds W).get v))

The participating slots of a block.

Equations

• RS.oddSlots W F v = {j : Fin ((RS.ds W).get v) | RS.blockFlag W v j ∈ F.flags}

theorem RS.mem_oddSlots {W : ClosedFragment} {F : EdgeSubset W} {v : Fin (ds W).length} (j : Fin ((ds W).get v)) : j ∈ oddSlots W F v ↔ blockFlag W v j ∈ F.flags

Membership in the participating slots.

theorem RS.oddSlot_mem {W : ClosedFragment} {F : EdgeSubset W} {v : Fin (ds W).length} (j : ↥(oddSlots W F v)) : blockFlag W v ↑j ∈ F.flags

The defining property of a participating block slot.

theorem RS.map_flagsAt_blockVertex {β : Type} (W : ClosedFragment) (F : EdgeSubset W) (v : Fin (ds W).length) (g : ↥F.flags → β) : Multiset.map g {f : ↥F.flags | W.attach ↑f = Sum.inl (blockVertex W v)}.val = Multiset.map (fun (j : ↥(oddSlots W F v)) => g ⟨blockFlag W v ↑j, ⋯⟩) (oddSlots W F v).attach.val

Participating flags at a block's vertex reindex over the participating slots, for any value function.

theorem RS.prod_blockVertex {M : Type u_1} [CommMonoid M] (W : ClosedFragment) (g : W.Vertex → M) : ∏ vtx : W.Vertex, g vtx = ∏ v : Fin (ds W).length, g (blockVertex W v)

Vertex products reindex over blocks.

theorem RS.blockRestrict_colouringOf_isRight {k ℓ : ℕ} (W : ClosedFragment) (F : EdgeSubset W) (ψ : F.EvenColouring k) (φ : F.OddColouring ℓ) (v : Fin (ds W).length) (j : Fin ((ds W).get v)) : (blockRestrict (ds W) (cSorted W (colouringOf W F ψ φ)) v j).isRight = true ↔ blockFlag W v j ∈ F.flags

Participation of a block slot is participation of its flag.