theorem Hex.GraphIso.Nauty.Sparse.Graph.context_iso {n : Nat} (G H : SparseGraph n) (σ : Renaming n) (h : RowsMap σ (context G).g (context H).g) (i j : Fin n) : H.adj (σ.toPerm.get i) (σ.toPerm.get j) = G.adj i j

The shared row interpretation of a renaming gives native adjacency preservation by its finite permutation.

theorem Hex.GraphIso.Nauty.Sparse.Ready.automorphism {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hshape : NodeShape n level st.ptn) {tc te a b : Nat} (hc : (tc, te) ∈ cells st.ptn level n) (hne : tc < te) (ha : a ≤ te - tc) (hb : b ≤ te - tc) (hab : a ≠ b) : ∃ (p : Perm n), (∀ (i j : Fin n), G.graph.adj (p.get i) (p.get j) = G.graph.adj i j) ∧ cellsPerm st.ptn level st.lab (Array.map (renamingOf p).toFun st.lab) ∧ st.lab[tc + b]! = (renamingOf p).toFun st.lab[tc + a]!

The automorphism supplied by the cheap shape can be consumed directly by native refinement transport, with the same moved vertex and cell action.