def Hex.GraphIso.Nauty.ColorMap {n k : Nat} (G : Colored n k) (γ : Array Nat) : Prop

A raw permutation array preserves the ordered initial colours.

Equations

• Hex.GraphIso.Nauty.ColorMap G γ = ∀ (v : Fin n), ∃ (hv : γ[↑v]! < n), G.coloring.cells.get ⟨γ[↑v]!, hv⟩ = G.coloring.cells.get v

theorem Hex.GraphIso.Nauty.ColorMap.scatter {n k : Nat} {G : Colored n k} {γ ref cur : Array Nat} (hn : 0 < n) (hrefSize : ref.size = n) (href : CellsReach G ref) (hcur : CellsReach G cur) (hmap : ∀ (i : Nat), i < n → γ[ref[i]!]! = cur[i]!) : ColorMap G γ

Scattering between reached labellings preserves colours because the colour at each position is fixed by the initial ordered partition.

theorem Hex.GraphIso.Nauty.GenTraceOk.colors {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : SearchSt n} (h : GenTraceOk ctx st (ColorMap G)) {γ : Array Nat} (hγ : γ ∈ st.genTrace.toList) : ColorMap G γ

Read colour preservation from the strengthened trace invariant.