The colour action of the top braiding, base case

The two-strand braid conjugated into the colouring model is the Koszul-signed adjacent swap: coordinate evaluation of the braid on the block structure, one encoding context throughout.

Arity-one evaluations on general pads

Arity-two evaluations on general pads, even component

The braid values, in-file encodings

The even-component coordinate identity

Arity-two evaluations, odd component

The odd braid values and coordinate identity

The top swap on halves

The general even coordinate identity

The general odd coordinate identity and main theorem

theorem RS.toColour_topBraid {k ℓ : ℕ} (n : ℕ) : toColour (n + 2) (topBraid (stdSuperPair k ℓ) n) = colourSwap k ℓ (n + 2) n ⋯

The colour action of the top braiding.