theorem Hex.GraphIso.Nauty.Sparse.Index.Valid.reindex {n level first last : Nat} {oldlab lab ptn oldstarts starts ends : Array Nat} (h : Valid n oldlab ptn level oldstarts ends) (hc : IsCell ptn level first (last - first)) (hs : starts.size = n) (hf : Frame n first (last - 1) oldlab lab oldstarts starts ends ends) (hg : ∀ (q : Nat), first ≤ q → q < last → starts[lab[q]!]! = if last = first + 1 then n else first) : Valid n lab ptn level starts ends

With the partition unchanged, correct indices on one cell and retained exterior entries suffice for complete cache validity.