theorem Hex.GraphIso.Nauty.Sparse.mark_neighbors {n : Nat} (G : SparseGraph n) (vertex : Fin n) (lab ptn starts ends marks vmarks : Array Nat) (level stamp : Nat) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hi : Index.Valid n lab ptn level starts ends) (hm : Scratch.Marks n stamp marks) (hvm : Scratch.Marks n stamp vmarks) : have r := (have marks := marks; have touched := #[]; have hitVertices := 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 (stamp + 1); have k := starts[j]!; if (k != n && marks[k]! != stamp + 1) = true then have marks := marks.set! k (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; Touched n stamp marks r.fst (sortCells r.snd.fst) (List.map (fun (e : Nat) => starts[(Graph.ofGraph G).neighbor e]!) (List.range' G.offsets[↑vertex]! (G.offsets[↑vertex + 1]! - G.offsets[↑vertex]!))) ∧ (∀ (v : Fin n), r.snd.snd[↑v]! = stamp + 1 ↔ G.adj vertex v = true) ∧ ∀ (a : Nat), a ∈ (sortCells r.snd.fst).toList → IsCell ptn level a (ends[a]! + 1 - a) ∧ a < ends[a]! ∧ ends[a]! < n

Native singleton marking computes adjacency exactly and records only bounded nontrivial cells. The valid graph and cache discharge every loop lookup bound, including graphs with isolated vertices.