theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.cell_mem {lab ptn starts ends : Array Nat} {n level first last v : Nat} (hi : Valid n lab ptn level starts ends) (hp : lab.toList.Perm (List.range n)) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hc : IsCell ptn level first (last - first)) (hn : first + 1 < last) (hb : last ≤ n) (hv : v < n) : v ∈ List.map (fun (q : Nat) => lab[q]!) (List.range' first (last - first)) ↔ starts[v]! = first

A nontrivial cell's vertex list is exactly its cached inverse image.

theorem Hex.GraphIso.Nauty.Sparse.clear_scan (lab before : Array Nat) (n first last : Nat) (hp : lab.toList.Perm (List.range n)) (hs : before.size = n) (hf : first ≤ last) (hb : last ≤ n) : have out := (have hits := before; do let __s ← forIn [first:last] hits fun (q : Nat) (__s : Array Nat) => have hits := __s; have hits := hits.set! lab[q]! 0; pure (ForInStep.yield hits) have hits : Array Nat := __s pure hits).run; Index.Writes n before out (List.map (fun (q : Nat) => lab[q]!) (List.range' first (last - first))) 0

The literal first-touch clearing loop changes precisely its cell's vertices, without requiring any bound on the previous count values.