theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.mem_cell {n level a len v : Nat} {lab ptn starts ends : Array Nat} (h : 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 a len) (hb : a + len ≤ n) (hn : 1 < len) (hv : v < n) : (starts[v]! == a) = (worksetOf n lab a (a + len - 1)).mem v

A native vertex-to-cell lookup tests membership in the corresponding nontrivial cell's vertex set. Singleton sentinels cannot match that start.