Block restrictions of colourings

Restricting a colouring of a concatenated total to its blocks through the block enumeration, with the enumeration's value laws at a cons: the vocabulary in which the assembled star vector's coordinates factor over the vertices.

theorem RS.blockSigmaEquiv_cons_zero_val (d : ℕ) (ds : List ℕ) (j : Fin d) : ↑((blockSigmaEquiv (d :: ds)) ⟨⟨0, ⋯⟩, j⟩) = ↑j

The head-block values of the enumeration.

theorem RS.blockSigmaEquiv_cons_succ_val (d : ℕ) (ds : List ℕ) (v : Fin ds.length) (j : Fin (ds.get v)) : ↑((blockSigmaEquiv (d :: ds)) ⟨v.succ, j⟩) = d + ↑((blockSigmaEquiv ds) ⟨v, j⟩)

The tail-block values of the enumeration.

noncomputable def RS.blockRestrict {k ℓ : ℕ} (ds : List ℕ) (c : MixedColouring k ℓ ds.sum) (v : Fin ds.length) : MixedColouring k ℓ (ds.get v)

The block restriction of a colouring.

Equations

• RS.blockRestrict ds c v j = c ((RS.blockSigmaEquiv ds) ⟨v, j⟩)

theorem RS.blockSigmaEquiv_strictMono (ds : List ℕ) (v : Fin ds.length) : StrictMono fun (j : Fin (ds.get v)) => (blockSigmaEquiv ds) ⟨v, j⟩

The sigma position is strictly monotone in the block offset.