theorem Hex.GraphIso.Nauty.Sparse.splitSingleton_trace {n : Nat} (G : SparseGraph n) (level split : Nat) (s : RefineSt n) (hp : s.lab.toList.Perm (List.range n)) (hs : s.ptn.size = n) (hend : s.ptn[n - 1]! ≤ level) (hsp : split < n) (hi : Index.Valid n s.lab s.ptn level s.cellstart s.cellend) (hm : Scratch.Marks n s.stamp s.marks) (hv : Scratch.Marks n s.stamp s.vmarks) : have vertex := s.lab[split]!; have r := (have marks := s.marks; have touched := #[]; have hitVertices := s.vmarks; do let __s ← forIn [G.offsets[vertex]!:G.offsets[vertex + 1]!] (marks, touched, hitVertices) fun (e : Nat) (__s : Array Nat × Array Nat × Array Nat) => have marks := __s.fst; have __s := __s.snd; have touched := __s.fst; have hitVertices := __s.snd; have j := (Graph.ofGraph G).neighbor e; have hitVertices := hitVertices.set! j (s.stamp + 1); have k := s.cellstart[j]!; if (k != n && marks[k]! != s.stamp + 1) = true then have marks := marks.set! k (s.stamp + 1); have touched := touched.push k; pure (ForInStep.yield (marks, touched, hitVertices)) else pure (ForInStep.yield (marks, touched, hitVertices)) have marks : Array Nat := __s.fst have __s : Array Nat × Array Nat := __s.snd have touched : Array Nat := __s.fst have hitVertices : Array Nat := __s.snd pure (marks, touched, hitVertices)).run; have touched := sortCells r.snd.fst; have initial := { lab := s.lab, ptn := s.ptn, active := s.active, queue := s.queue, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := r.fst, vmarks := r.snd.snd, stamp := s.stamp + 1, numcells := s.numcells, longcode := s.longcode }.hash touched.size; Binary.Pass level (s.stamp + 1) touched.toList initial (splitSingleton (Graph.ofGraph G) level split s)

The production singleton splitter is its native marking loop followed by the proved touched-cell trace, including its initial touched-count hash.