theorem Hex.GraphIso.Nauty.Sparse.Compact.cache {n level first last cut : Nat} {before lab hit out ptn oldstarts starts ends : Array Nat} {p : Nat → Bool} {seen : List Nat} (h : Compact before p first last seen lab hit cut) (hs : seen = List.take (last - first) (List.drop first before.toList)) (hr : Fill lab hit.toList.reverse cut hit.toList.reverse.length out) (hw : Index.Writes n oldstarts starts hit.toList.reverse cut) (hp : before.toList.Perm (List.range n)) (hptn : ptn.size = n) (hi : Index.Valid n before ptn level oldstarts ends) (hc : IsCell ptn level first (last - first)) (hn : first + 1 < last) : let changed := cut ≠ last ∧ cut ≠ first; have middle := if cut = first + 1 then starts.setIfInBounds out[first]! n else starts; Index.Valid n out (if changed then ptn.setIfInBounds (cut - 1) level else ptn) level (if changed then if last = cut + 1 then middle.setIfInBounds out[cut]! n else middle else starts) (if changed then (ends.setIfInBounds first (cut - 1)).setIfInBounds cut (last - 1) else ends)

Compaction, reverse reinsertion, and the singleton splitter's conditional boundary and sentinel writes preserve the complete cell cache. Uniform cells retain their partition; a mixed cell receives exactly the two new endpoints.