theorem Hex.GraphIso.Nauty.runState_orbits {n k : Nat} (G : Colored n k) : OrbitsOk (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd

The complete search run justifies every orbit pointer by its recorded generators.

theorem Hex.GraphIso.Nauty.runState_colors {n k : Nat} (G : Colored n k) : TraceStab G (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd

Every generator in the completed run stabilizes the initial colour partition.

theorem Hex.GraphIso.Nauty.runState_pairs {n k : Nat} (G : Colored n k) : PairsOk G { g := rowsOf G } (runState n (rowsOf G) (initialPartition G).fst (initialPartition G).snd).snd

Every pair in the final workspace has checked colour-preserving realizers.

theorem Hex.GraphIso.Nauty.runColoredTraced_stab {n k : Nat} (G : Colored n k) {perm : Array Nat} (hp : perm ∈ (runColoredTraced G).autos) : ColorStab G perm

The search's reported generators preserve the ordered colour cells.

theorem Hex.GraphIso.Nauty.canonlab_size {n k : Nat} (G : Colored n k) : (runColored G).canonlab.size = n

The search returns a full canonical labelling.

theorem Hex.GraphIso.Nauty.canonlab_cellsReach {n k : Nat} (G : Colored n k) : CellsReach G (runColored G).canonlab

The search's canonical labelling fills each initial colour cell with its own vertices.

theorem Hex.GraphIso.Nauty.labelColorSorted_canonlab {n k : Nat} (G : Colored n k) : labelColorSorted G (runColored G).canonlab = true

The search's canonical labelling respects the initial colour order.

theorem Hex.GraphIso.Nauty.canonlab_perm_range {n k : Nat} (G : Colored n k) : (runColored G).canonlab.toList.Perm (List.range n)

The search's canonical labelling is a permutation of the vertices.

theorem Hex.GraphIso.Nauty.canong_inv {n k : Nat} (G : Colored n k) : CanongInv { g := rowsOf G } (runColored G).canong (runColored G).canonlab n

Finishing the search fills every canonical row from the installed labelling.

theorem Hex.GraphIso.Nauty.canong_rows {n k : Nat} (G : Colored n k) : List.map (fun (x : Nat) => (runColored G).canong[x]!) (List.range n) = leafRows { g := rowsOf G } (runColored G).canonlab

The returned row array encodes the search's returned labelling.

theorem Hex.GraphIso.Nauty.runTraced_result (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : (runTraced n g lab0 cellEnds).result = run n g lab0 cellEnds

Discarding the trace gives the search's ordinary result.

theorem Hex.GraphIso.Nauty.runColoredTraced_result {n k : Nat} (G : Colored n k) : (runColoredTraced G).result = runColored G

The traced coloured run and ordinary coloured run have the same result.