theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.iter {n : Nat} {G : SparseGraph n} {level : Nat} {s : RefineSt n} (h : Ready G level s) : IterOk (Graph.context G) level s.toPartition

The partition interpretation of a native refined state satisfies the invariants used by the shared cell-stabilizer and pruning proofs.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Ready.automorphism {n : Nat} {G : SparseGraph n} {level : Nat} {s : RefineSt n} (h : Ready G level s) (hshape : NodeShape n level s.ptn) {tc len a b : Nat} (hc : IsCell s.ptn level tc len) (hb : tc + len ≤ n) (hn : 1 < len) (ha : a < len) (hb' : b < len) (hab : a ≠ b) : ∃ (p : Perm n), (∀ (i j : Fin n), G.adj (p.get i) (p.get j) = G.adj i j) ∧ cellsPerm s.ptn level s.lab (Array.map (renamingOf p).toFun s.lab) ∧ s.lab[tc + b]! = (renamingOf p).toFun s.lab[tc + a]!

The small-cell stabilizer theorem applies to a literal cached-refinement node through its proved partition interpretation.