theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.singleton_cert {n level : Nat} {s : RefineSt n} (h : Valid level s) (G : SparseGraph n) (pos : Nat) (hp : pos < s.queue.size) (hsplit : s.ptn[s.queue[pos]!]! ≤ level) (hinv : CertInv (Graph.context G) level s.toPartition) : have r := { lab := s.lab, ptn := s.ptn, active := s.active.erase s.queue[pos]!, queue := (s.queue.setIfInBounds pos s.queue[s.queue.size - 1]!).pop, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }.hash s.queue[pos]!; CertInv (Graph.context G) level (splitSingleton (Graph.ofGraph G) level s.queue[pos]! r).toPartition

The actual singleton branch preserves the equitability certificate, including swap/pop removal and hashing of the selected splitter.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.nontrivial_cert {n level : Nat} {s : RefineSt n} (h : Valid level s) (G : SparseGraph n) (pos : Nat) (hp : pos < s.queue.size) (hinv : CertInv (Graph.context G) level s.toPartition) : have r := { lab := s.lab, ptn := s.ptn, active := s.active.erase s.queue[pos]!, queue := (s.queue.setIfInBounds pos s.queue[s.queue.size - 1]!).pop, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode }.hash s.queue[pos]!; CertInv (Graph.context G) level (splitNontrivial (Graph.ofGraph G) level s.queue[pos]! r).toPartition

The actual nontrivial branch preserves the equitability certificate, including the exact queue removal and largest-fragment activation choices.