theorem Hex.GraphIso.Nauty.Sparse.rootLeaves_map {n k : Nat} {G H : Sparse.Colored n k} {p : Perm n} (h : Sparse.IsIso G H p) {leaf : SpecLeaf n} (hm : leaf ∈ rootLeaves G) : SpecLeaf.map p leaf ∈ rootLeaves H

Isomorphic roots have corresponding leaves in the native sparse tree. The colour-bucket correspondence concerns the initializer only; all recursive refinement and target selection in this theorem are sparse operations.

theorem Hex.GraphIso.Nauty.Sparse.canonSpecKey_map {n k : Nat} {G H : Sparse.Colored n k} {p : Perm n} (h : Sparse.IsIso G H p) : canonSpecKey G = canonSpecKey H

Sparse nauty's declarative maximum is invariant under every colour-preserving graph isomorphism. Both inequalities follow from actual tree leaves, without an assumption about the production search.

theorem Hex.GraphIso.Nauty.Sparse.canonSpecKey_iso {n k : Nat} {G H : Sparse.Colored n k} (h : Sparse.Isomorphic G H) : canonSpecKey G = canonSpecKey H