theorem Hex.GraphIso.Nauty.Sparse.Index.Two.valid {n level first cut last : Nat} {lab oldlab ptn oldstarts starts oldends : Array Nat} (h : Two n first cut last last lab starts) (hi : Valid n oldlab ptn level oldstarts oldends) (hc : IsCell ptn level first (last - first)) (hs : ptn.size = n) (hf : first < cut) (hl : cut < last) (hb : last ≤ n) (hframe : Frame n first (last - 1) oldlab lab oldstarts starts oldends oldends) : Valid n lab (ptn.setIfInBounds (cut - 1) level) level starts ((oldends.setIfInBounds first (cut - 1)).setIfInBounds cut (last - 1))

A binary split installs a complete valid cache after its literal partition and endpoint writes. All other cells keep their old cache entries.