theorem Hex.GraphIso.Nauty.Sparse.Graph.row_map {n : Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (vertex : Fin n) : ((ofGraph H).row ↑(p.get vertex)).Perm (List.map (renamingOf p).toFun ((ofGraph G).row ↑vertex))

A native row transports its vertex multiset under an isomorphism. Its stored neighbour order is allowed to change.

theorem Hex.GraphIso.Nauty.Sparse.Graph.cell_row_map {n : Nat} {lab ptn : Array Nat} {level : Nat} {starts ends out other final : Array Nat} (G H : SparseGraph n) (p : Perm n) (hiso : ∀ (u v : Fin n), H.adj (p.get u) (p.get v) = G.adj u v) (vertex : Fin n) (hi : Index.Valid n lab ptn level starts ends) (hj : Index.Valid n out ptn level other final) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : cellsPerm ptn level out (Array.map (renamingOf p).toFun lab)) : (List.map (fun (v : Nat) => other[v]!) ((ofGraph H).row ↑(p.get vertex))).Perm (List.map (fun (v : Nat) => starts[v]!) ((ofGraph G).row ↑vertex))

Mapping each native neighbour to its cached cell preserves the full multiset, for arbitrary admissible caches and orders within the cells.